Theorem hoadddit 9646

Description: Scalar product distributive law for Hilbert space operators.

Assertion

Ref	Expression
hoadddit	|- ((A e. CC /\ T:H~-->H~ /\ U:H~-->H~) -> (A .op (T +op U)) = ((A .op T) +op (A .op U)))

Proof of Theorem hoadddit

Step	Hyp	Ref	Expression
1		homvalt 9435	. . . . . . 7 |- ((A e. CC /\ (T +op U):H~-->H~ /\ x e. H~) -> ((A .op (T +op U))` x) = (A .h ((T +op U)` x)))
2	1	3expa 831	. . . . . 6 |- (((A e. CC /\ (T +op U):H~-->H~) /\ x e. H~) -> ((A .op (T +op U))` x) = (A .h ((T +op U)` x)))
3		hoaddclt 9601	. . . . . . . 8 |- ((T:H~-->H~ /\ U:H~-->H~) -> (T +op U):H~-->H~)
4	3	anim2i 335	. . . . . . 7 |- ((A e. CC /\ (T:H~-->H~ /\ U:H~-->H~)) -> (A e. CC /\ (T +op U):H~-->H~))
5	4	3impb 827	. . . . . 6 |- ((A e. CC /\ T:H~-->H~ /\ U:H~-->H~) -> (A e. CC /\ (T +op U):H~-->H~))
6	2, 5	sylan 448	. . . . 5 |- (((A e. CC /\ T:H~-->H~ /\ U:H~-->H~) /\ x e. H~) -> ((A .op (T +op U))` x) = (A .h ((T +op U)` x)))
7		hosvalt 9433	. . . . . . . 8 |- ((T:H~-->H~ /\ U:H~-->H~ /\ x e. H~) -> ((T +op U)` x) = ((T` x) +h (U` x)))
8	7	opreq2d 3961	. . . . . . 7 |- ((T:H~-->H~ /\ U:H~-->H~ /\ x e. H~) -> (A .h ((T +op U)` x)) = (A .h ((T` x) +h (U` x))))
9	8	3expa 831	. . . . . 6 |- (((T:H~-->H~ /\ U:H~-->H~) /\ x e. H~) -> (A .h ((T +op U)` x)) = (A .h ((T` x) +h (U` x))))
10	9	3adantl1 801	. . . . 5 |- (((A e. CC /\ T:H~-->H~ /\ U:H~-->H~) /\ x e. H~) -> (A .h ((T +op U)` x)) = (A .h ((T` x) +h (U` x))))
11		ax-hvdistr1 8799	. . . . . . 7 |- ((A e. CC /\ (T` x) e. H~ /\ (U` x) e. H~) -> (A .h ((T` x) +h (U` x))) = ((A .h (T` x)) +h (A .h (U` x))))
12		3simp1 786	. . . . . . . 8 |- ((A e. CC /\ T:H~-->H~ /\ U:H~-->H~) -> A e. CC)
13	12	adantr 389	. . . . . . 7 |- (((A e. CC /\ T:H~-->H~ /\ U:H~-->H~) /\ x e. H~) -> A e. CC)
14		ffvelrn 3799	. . . . . . . 8 |- ((T:H~-->H~ /\ x e. H~) -> (T` x) e. H~)
15	14	3ad2antl2 808	. . . . . . 7 |- (((A e. CC /\ T:H~-->H~ /\ U:H~-->H~) /\ x e. H~) -> (T` x) e. H~)
16		ffvelrn 3799	. . . . . . . 8 |- ((U:H~-->H~ /\ x e. H~) -> (U` x) e. H~)
17	16	3ad2antl3 809	. . . . . . 7 |- (((A e. CC /\ T:H~-->H~ /\ U:H~-->H~) /\ x e. H~) -> (U` x) e. H~)
18	11, 13, 15, 17	syl3anc 856	. . . . . 6 |- (((A e. CC /\ T:H~-->H~ /\ U:H~-->H~) /\ x e. H~) -> (A .h ((T` x) +h (U` x))) = ((A .h (T` x)) +h (A .h (U` x))))
19		homvalt 9435	. . . . . . . . 9 |- ((A e. CC /\ T:H~-->H~ /\ x e. H~) -> ((A .op T)` x) = (A .h (T` x)))
20	19	3expa 831	. . . . . . . 8 |- (((A e. CC /\ T:H~-->H~) /\ x e. H~) -> ((A .op T)` x) = (A .h (T` x)))
21	20	3adantl3 803	. . . . . . 7 |- (((A e. CC /\ T:H~-->H~ /\ U:H~-->H~) /\ x e. H~) -> ((A .op T)` x) = (A .h (T` x)))
22		homvalt 9435	. . . . . . . . 9 |- ((A e. CC /\ U:H~-->H~ /\ x e. H~) -> ((A .op U)` x) = (A .h (U` x)))
23	22	3expa 831	. . . . . . . 8 |- (((A e. CC /\ U:H~-->H~) /\ x e. H~) -> ((A .op U)` x) = (A .h (U` x)))
24	23	3adantl2 802	. . . . . . 7 |- (((A e. CC /\ T:H~-->H~ /\ U:H~-->H~) /\ x e. H~) -> ((A .op U)` x) = (A .h (U` x)))
25	21, 24	opreq12d 3963	. . . . . 6 |- (((A e. CC /\ T:H~-->H~ /\ U:H~-->H~) /\ x e. H~) -> (((A .op T)` x) +h ((A .op U)` x)) = ((A .h (T` x)) +h (A .h (U` x))))
26	18, 25	eqtr4d 1502	. . . . 5 |- (((A e. CC /\ T:H~-->H~ /\ U:H~-->H~) /\ x e. H~) -> (A .h ((T` x) +h (U` x))) = (((A .op T)` x) +h ((A .op U)` x)))
27	6, 10, 26	3eqtrd 1503	. . . 4 |- (((A e. CC /\ T:H~-->H~ /\ U:H~-->H~) /\ x e. H~) -> ((A .op (T +op U))` x) = (((A .op T)` x) +h ((A .op U)` x)))
28		hosvalt 9433	. . . . . 6 |- (((A .op T):H~-->H~ /\ (A .op U):H~-->H~ /\ x e. H~) -> (((A .op T) +op (A .op U))` x) = (((A .op T)` x) +h ((A .op U)` x)))
29	28	3expa 831	. . . . 5 |- ((((A .op T):H~-->H~ /\ (A .op U):H~-->H~) /\ x e. H~) -> (((A .op T) +op (A .op U))` x) = (((A .op T)` x) +h ((A .op U)` x)))
30		homulclt 9602	. . . . . . 7 |- ((A e. CC /\ T:H~-->H~) -> (A .op T):H~-->H~)
31		homulclt 9602	. . . . . . 7 |- ((A e. CC /\ U:H~-->H~) -> (A .op U):H~-->H~)
32	30, 31	anim12i 333	. . . . . 6 |- (((A e. CC /\ T:H~-->H~) /\ (A e. CC /\ U:H~-->H~)) -> ((A .op T):H~-->H~ /\ (A .op U):H~-->H~))
33	32	3impdi 877	. . . . 5 |- ((A e. CC /\ T:H~-->H~ /\ U:H~-->H~) -> ((A .op T):H~-->H~ /\ (A .op U):H~-->H~))
34	29, 33	sylan 448	. . . 4 |- (((A e. CC /\ T:H~-->H~ /\ U:H~-->H~) /\ x e. H~) -> (((A .op T) +op (A .op U))` x) = (((A .op T)` x) +h ((A .op U)` x)))
35	27, 34	eqtr4d 1502	. . 3 |- (((A e. CC /\ T:H~-->H~ /\ U:H~-->H~) /\ x e. H~) -> ((A .op (T +op U))` x) = (((A .op T) +op (A .op U))` x))
36	35	r19.21aiva 1706	. 2 |- ((A e. CC /\ T:H~-->H~ /\ U:H~-->H~) -> A.x e. H~ ((A .op (T +op U))` x) = (((A .op T) +op (A .op U))` x))
37		hoeqt 9603	. . 3 |- (((A .op (T +op U)):H~-->H~ /\ ((A .op T) +op (A .op U)):H~-->H~) -> (A.x e. H~ ((A .op (T +op U))` x) = (((A .op T) +op (A .op U))` x) <-> (A .op (T +op U)) = ((A .op T) +op (A .op U))))
38		homulclt 9602	. . . . 5 |- ((A e. CC /\ (T +op U):H~-->H~) -> (A .op (T +op U)):H~-->H~)
39	38, 3	sylan2 451	. . . 4 |- ((A e. CC /\ (T:H~-->H~ /\ U:H~-->H~)) -> (A .op (T +op U)):H~-->H~)
40	39	3impb 827	. . 3 |- ((A e. CC /\ T:H~-->H~ /\ U:H~-->H~) -> (A .op (T +op U)):H~-->H~)
41		hoaddclt 9601	. . . . 5 |- (((A .op T):H~-->H~ /\ (A .op U):H~-->H~) -> ((A .op T) +op (A .op U)):H~-->H~)
42	41, 30, 31	syl2an 454	. . . 4 |- (((A e. CC /\ T:H~-->H~) /\ (A e. CC /\ U:H~-->H~)) -> ((A .op T) +op (A .op U)):H~-->H~)
43	42	3impdi 877	. . 3 |- ((A e. CC /\ T:H~-->H~ /\ U:H~-->H~) -> ((A .op T) +op (A .op U)):H~-->H~)
44	37, 40, 43	sylanc 471	. 2 |- ((A e. CC /\ T:H~-->H~ /\ U:H~-->H~) -> (A.x e. H~ (