Theorem hoadddit 9669

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 9458	. . . . . . 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 832	. . . . . 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 9624	. . . . . . . 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 828	. . . . . 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 9456	. . . . . . . 8 |- ((T:H~-->H~ /\ U:H~-->H~ /\ x e. H~) -> ((T +op U)` x) = ((T` x) +h (U` x)))
8	7	opreq2d 3967	. . . . . . 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 832	. . . . . 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 802	. . . . 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 8817	. . . . . . 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 787	. . . . . . . 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 3805	. . . . . . . 8 |- ((T:H~-->H~ /\ x e. H~) -> (T` x) e. H~)
15	14	3ad2antl2 809	. . . . . . 7 |- (((A e. CC /\ T:H~-->H~ /\ U:H~-->H~) /\ x e. H~) -> (T` x) e. H~)
16		ffvelrn 3805	. . . . . . . 8 |- ((U:H~-->H~ /\ x e. H~) -> (U` x) e. H~)
17	16	3ad2antl3 810	. . . . . . 7 |- (((A e. CC /\ T:H~-->H~ /\ U:H~-->H~) /\ x e. H~) -> (U` x) e. H~)
18	11, 13, 15, 17	syl3anc 857	. . . . . 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 9458	. . . . . . . . 9 |- ((A e. CC /\ T:H~-->H~ /\ x e. H~) -> ((A .op T)` x) = (A .h (T` x)))
20	19	3expa 832	. . . . . . . 8 |- (((A e. CC /\ T:H~-->H~) /\ x e. H~) -> ((A .op T)` x) = (A .h (T` x)))
21	20	3adantl3 804	. . . . . . 7 |- (((A e. CC /\ T:H~-->H~ /\ U:H~-->H~) /\ x e. H~) -> ((A .op T)` x) = (A .h (T` x)))
22		homvalt 9458	. . . . . . . . 9 |- ((A e. CC /\ U:H~-->H~ /\ x e. H~) -> ((A .op U)` x) = (A .h (U` x)))
23	22	3expa 832	. . . . . . . 8 |- (((A e. CC /\ U:H~-->H~) /\ x e. H~) -> ((A .op U)` x) = (A .h (U` x)))
24	23	3adantl2 803	. . . . . . 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 3969	. . . . . 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 1507	. . . . 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 1508	. . . 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 9456	. . . . . 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 832	. . . . 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 9625	. . . . . . 7 |- ((A e. CC /\ T:H~-->H~) -> (A .op T):H~-->H~)
31		homulclt 9625	. . . . . . 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 878	. . . . 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 1507	. . 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 1711	. 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 9626	. . 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 9625	. . . . 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 828	. . 3 |- ((A e. CC /\ T:H~-->H~ /\ U:H~-->H~) -> (A .op (T +op U)):H~-->H~)
41		hoaddclt 9624	. . . . 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 878	. . 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~ (