Theorem hstel2t 10146

Description: Properties of a Hilbert-space-valued state.

Assertion

Ref	Expression
hstel2t	|- (((S e. CHStates /\ A e. CH) /\ (B e. CH /\ A (_ (_|_` B))) -> (((S` A) .ih (S` B)) = 0 /\ (S` (A vH B)) = ((S` A) +h (S` B))))

Proof of Theorem hstel2t

Step	Hyp	Ref	Expression
1		hstelt 10142	. . . 4 |- (S e. CHStates <-> (S:CH-->H~ /\ (normh` (S` H~)) = 1 /\ A.x e. CH A.y e. CH (x (_ (_|_` y) -> (((S` x) .ih (S` y)) = 0 /\ (S` (x vH y)) = ((S` x) +h (S` y))))))
2		3simp3 790	. . . 4 |- ((S:CH-->H~ /\ (normh` (S` H~)) = 1 /\ A.x e. CH A.y e. CH (x (_ (_|_` y) -> (((S` x) .ih (S` y)) = 0 /\ (S` (x vH y)) = ((S` x) +h (S` y))))) -> A.x e. CH A.y e. CH (x (_ (_|_` y) -> (((S` x) .ih (S` y)) = 0 /\ (S` (x vH y)) = ((S` x) +h (S` y)))))
3	1, 2	sylbi 199	. . 3 |- (S e. CHStates -> A.x e. CH A.y e. CH (x (_ (_|_` y) -> (((S` x) .ih (S` y)) = 0 /\ (S` (x vH y)) = ((S` x) +h (S` y)))))
4	3	ad2antrr 404	. 2 |- (((S e. CHStates /\ A e. CH) /\ (B e. CH /\ A (_ (_|_` B))) -> A.x e. CH A.y e. CH (x (_ (_|_` y) -> (((S` x) .ih (S` y)) = 0 /\ (S` (x vH y)) = ((S` x) +h (S` y)))))
5		sseq1 2082	. . . . . . . 8 |- (x = A -> (x (_ (_|_` y) <-> A (_ (_|_` y)))
6		fveq2 3724	. . . . . . . . . . 11 |- (x = A -> (S` x) = (S` A))
7	6	opreq1d 3975	. . . . . . . . . 10 |- (x = A -> ((S` x) .ih (S` y)) = ((S` A) .ih (S` y)))
8	7	eqeq1d 1483	. . . . . . . . 9 |- (x = A -> (((S` x) .ih (S` y)) = 0 <-> ((S` A) .ih (S` y)) = 0))
9		opreq1 3968	. . . . . . . . . . 11 |- (x = A -> (x vH y) = (A vH y))
10	9	fveq2d 3728	. . . . . . . . . 10 |- (x = A -> (S` (x vH y)) = (S` (A vH y)))
11	6	opreq1d 3975	. . . . . . . . . 10 |- (x = A -> ((S` x) +h (S` y)) = ((S` A) +h (S` y)))
12	10, 11	eqeq12d 1489	. . . . . . . . 9 |- (x = A -> ((S` (x vH y)) = ((S` x) +h (S` y)) <-> (S` (A vH y)) = ((S` A) +h (S` y))))
13	8, 12	anbi12d 628	. . . . . . . 8 |- (x = A -> ((((S` x) .ih (S` y)) = 0 /\ (S` (x vH y)) = ((S` x) +h (S` y))) <-> (((S` A) .ih (S` y)) = 0 /\ (S` (A vH y)) = ((S` A) +h (S` y)))))
14	5, 13	imbi12d 626	. . . . . . 7 |- (x = A -> ((x (_ (_|_` y) -> (((S` x) .ih (S` y)) = 0 /\ (S` (x vH y)) = ((S` x) +h (S` y)))) <-> (A (_ (_|_` y) -> (((S` A) .ih (S` y)) = 0 /\ (S` (A vH y)) = ((S` A) +h (S` y))))))
15		fveq2 3724	. . . . . . . . 9 |- (y = B -> (_|_` y) = (_|_` B))
16	15	sseq2d 2089	. . . . . . . 8 |- (y = B -> (A (_ (_|_` y) <-> A (_ (_|_` B)))
17		fveq2 3724	. . . . . . . . . . 11 |- (y = B -> (S` y) = (S` B))
18	17	opreq2d 3976	. . . . . . . . . 10 |- (y = B -> ((S` A) .ih (S` y)) = ((S` A) .ih (S` B)))
19	18	eqeq1d 1483	. . . . . . . . 9 |- (y = B -> (((S` A) .ih (S` y)) = 0 <-> ((S` A) .ih (S` B)) = 0))
20		opreq2 3969	. . . . . . . . . . 11 |- (y = B -> (A vH y) = (A vH B))
21	20	fveq2d 3728	. . . . . . . . . 10 |- (y = B -> (S` (A vH y)) = (S` (A vH B)))
22	17	opreq2d 3976	. . . . . . . . . 10 |- (y = B -> ((S` A) +h (S` y)) = ((S` A) +h (S` B)))
23	21, 22	eqeq12d 1489	. . . . . . . . 9 |- (y = B -> ((S` (A vH y)) = ((S` A) +h (S` y)) <-> (S` (A vH B)) = ((S` A) +h (S` B))))
24	19, 23	anbi12d 628	. . . . . . . 8 |- (y = B -> ((((S` A) .ih (S` y)) = 0 /\ (S` (A vH y)) = ((S` A) +h (S` y))) <-> (((S` A) .ih (S` B)) = 0 /\ (S` (A vH B)) = ((S` A) +h (S` B)))))
25	16, 24	imbi12d 626	. . . . . . 7 |- (y = B -> ((A (_ (_|_` y) -> (((S` A) .ih (S` y)) = 0 /\ (S` (A vH y)) = ((S` A) +h (S` y)))) <-> (A (_ (_|_` B) -> (((S` A) .ih (S` B)) = 0 /\ (S` (A vH B)) = ((S` A) +h (S` B))))))
26	14, 25	rcla42v 1880	. . . . . 6 |- ((A e. CH /\ B e. CH) -> (A.x e. CH A.y e. CH (x (_ (_|_` y) -> (((S` x) .ih (S` y)) = 0 /\ (S` (x vH y)) = ((S` x) +h (S` y)))) -> (A (_ (_|_` B) -> (((S` A) .ih (S` B)) = 0 /\ (S` (A vH B)) = ((S` A) +h (S` B))))))
27	26	com23 32	. . . . 5 |- ((A e. CH /\ B e. CH) -> (A (_ (_|_` B) -> (A.x e. CH A.y e. CH (x (_ (_|_` y) -> (((S` x) .ih (S` y)) = 0 /\ (S` (x vH y)) = ((S` x) +h (S` y)))) -> (((S` A) .ih (S` B)) = 0 /\ (S` (A vH B)) = ((S` A) +h (S` B))))))
28	27	imp 350	. . . 4 |- (((A e. CH /\ B e. CH) /\ A (_ (_|_` B)) -> (A.x e. CH A.y e. CH (x (_ (_|_` y) -> (((S` x) .ih (S` y)) = 0 /\ (S` (x vH y)) = ((S` x) +h (S` y)))) -> (((S` A) .ih (S` B)) = 0 /\ (S` (A vH B)) = ((S` A) +h (S` B)))))
29	28	anasss 440	. . 3 |- ((A e. CH /\ (B e. CH /\ A (_ (_|_` B))) -> (A.x e. CH A.y e. CH (x (_ (_|_` y) -> (((S` x) .ih (S` y)) = 0 /\ (S` (x vH y)) = ((S` x) +h (S` y)))) -> (((S` A) .ih (S` B)) = 0 /\ (S` (A vH B)) = ((S` A) +h (S` B)))))
30	29	adantll 392	. 2 |- (((S e. CHStates /\ A e. CH) /\ (B e. CH /\ A (_ (_|_` B))) -> (A.x e. CH A.y e. CH (x (_ (_|_` y) -> (((S` x) .ih (S` y)) = 0 /\ (S` (x vH y)) = ((S` x) +h (S` y)))) -> (((S` A) .ih (S` B)) = 0 /\ (S` (A vH B)) = ((S` A) +h (S` B)))))
31	4, 30	mpd 26	1 |- (((S e. CHStates /\ A e. CH) /\ (B e. CH /\ A (_ (_|_` B))) -> (((S` A) .ih (S` B)) = 0 /\ (S` (A vH B)) = ((S` A) +h (S` B))))

Syntax hints:   -> wi 3   /\ wa 223   /\ w3a 775   = wceq 956   e. wcel 958  A.wral 1645   (_ wss 2047  -->wf 3178  ` cfv 3182  (class class class)co 3963  0cc0 5234  1c1 5235  H~chil 8788   +h cva 8789   .ih csp 8793  normhcno 8794  CHcch 8798  _|_cort 8799   vH chj 8802  CHStateschst 8832

This theorem is referenced by:  hstortht 10147  hstosumt 10148

This theorem was proved from axioms:  ax-1