Theorem hstel2t 10141

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 10137	. . . 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 792	. . . 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 406	. 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 2085	. . . . . . . 8 |- (x = A -> (x (_ (_|_` y) <-> A (_ (_|_` y)))
6		fveq2 3730	. . . . . . . . . . 11 |- (x = A -> (S` x) = (S` A))
7	6	opreq1d 3981	. . . . . . . . . 10 |- (x = A -> ((S` x) .ih (S` y)) = ((S` A) .ih (S` y)))
8	7	eqeq1d 1486	. . . . . . . . 9 |- (x = A -> (((S` x) .ih (S` y)) = 0 <-> ((S` A) .ih (S` y)) = 0))
9		opreq1 3974	. . . . . . . . . . 11 |- (x = A -> (x vH y) = (A vH y))
10	9	fveq2d 3734	. . . . . . . . . 10 |- (x = A -> (S` (x vH y)) = (S` (A vH y)))
11	6	opreq1d 3981	. . . . . . . . . 10 |- (x = A -> ((S` x) +h (S` y)) = ((S` A) +h (S` y)))
12	10, 11	eqeq12d 1492	. . . . . . . . 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 630	. . . . . . . 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 628	. . . . . . 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 3730	. . . . . . . . 9 |- (y = B -> (_|_` y) = (_|_` B))
16	15	sseq2d 2092	. . . . . . . 8 |- (y = B -> (A (_ (_|_` y) <-> A (_ (_|_` B)))
17		fveq2 3730	. . . . . . . . . . 11 |- (y = B -> (S` y) = (S` B))
18	17	opreq2d 3982	. . . . . . . . . 10 |- (y = B -> ((S` A) .ih (S` y)) = ((S` A) .ih (S` B)))
19	18	eqeq1d 1486	. . . . . . . . 9 |- (y = B -> (((S` A) .ih (S` y)) = 0 <-> ((S` A) .ih (S` B)) = 0))
20		opreq2 3975	. . . . . . . . . . 11 |- (y = B -> (A vH y) = (A vH B))
21	20	fveq2d 3734	. . . . . . . . . 10 |- (y = B -> (S` (A vH y)) = (S` (A vH B)))
22	17	opreq2d 3982	. . . . . . . . . 10 |- (y = B -> ((S` A) +h (S` y)) = ((S` A) +h (S` B)))
23	21, 22	eqeq12d 1492	. . . . . . . . 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 630	. . . . . . . 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 628	. . . . . . 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 1883	. . . . . 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 442	. . 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 394	. 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 777   = wceq 958   e. wcel 960  A.wral 1648   (_ wss 2050  -->wf 3184  ` cfv 3188  (class class class)co 3969  0cc0 5246  1c1 5247  H~chil 8783   +h cva 8784   .ih csp 8788  normhcno 8789  CHcch 8793  _|_cort 8794   vH chj 8797  CHStateschst 8827

This theorem is referenced by:  hstortht 10142  hstosumt 10143

This theorem was proved from axioms:  ax-1