Theorem hoadddi 11366

Description: Scalar product distributive law for Hilbert space operators.

Assertion

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

Proof of Theorem hoadddi

Step	Hyp	Ref	Expression
1		homval 11151	. . . . . . 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 1067	. . . . . 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		hoaddcl 11321	. . . . . . . 8 |- ((T:~H-->~H /\ U:~H-->~H) -> (T +op U):~H-->~H)
4	3	anim2i 362	. . . . . . 7 |- ((A e. CC /\ (T:~H-->~H /\ U:~H-->~H)) -> (A e. CC /\ (T +op U):~H-->~H))
5	4	3impb 1063	. . . . . 6 |- ((A e. CC /\ T:~H-->~H /\ U:~H-->~H) -> (A e. CC /\ (T +op U):~H-->~H))
6	2, 5	sylan 497	. . . . 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		hosval 11149	. . . . . . . 8 |- ((T:~H-->~H /\ U:~H-->~H /\ x e. ~H) -> ((T +op U)` x) = ((T` x) +h (U` x)))
8	7	opreq2d 4898	. . . . . . 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 1067	. . . . . 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 1032	. . . . 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		simp1 876	. . . . . . . 8 |- ((A e. CC /\ T:~H-->~H /\ U:~H-->~H) -> A e. CC)
12	11	adantr 425	. . . . . . 7 |- (((A e. CC /\ T:~H-->~H /\ U:~H-->~H) /\ x e. ~H) -> A e. CC)
13		ffvelrn 4787	. . . . . . . 8 |- ((T:~H-->~H /\ x e. ~H) -> (T` x) e. ~H)
14	13	3ad2antl2 1039	. . . . . . 7 |- (((A e. CC /\ T:~H-->~H /\ U:~H-->~H) /\ x e. ~H) -> (T` x) e. ~H)
15		ffvelrn 4787	. . . . . . . 8 |- ((U:~H-->~H /\ x e. ~H) -> (U` x) e. ~H)
16	15	3ad2antl3 1040	. . . . . . 7 |- (((A e. CC /\ T:~H-->~H /\ U:~H-->~H) /\ x e. ~H) -> (U` x) e. ~H)
17		ax-hvdistr1 10510	. . . . . . 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))))
18	12, 14, 16, 17	syl111anc 1100	. . . . . 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		homval 11151	. . . . . . . . 9 |- ((A e. CC /\ T:~H-->~H /\ x e. ~H) -> ((A .op T)` x) = (A .h (T` x)))
20	19	3expa 1067	. . . . . . . 8 |- (((A e. CC /\ T:~H-->~H) /\ x e. ~H) -> ((A .op T)` x) = (A .h (T` x)))
21	20	3adantl3 1034	. . . . . . 7 |- (((A e. CC /\ T:~H-->~H /\ U:~H-->~H) /\ x e. ~H) -> ((A .op T)` x) = (A .h (T` x)))
22		homval 11151	. . . . . . . . 9 |- ((A e. CC /\ U:~H-->~H /\ x e. ~H) -> ((A .op U)` x) = (A .h (U` x)))
23	22	3expa 1067	. . . . . . . 8 |- (((A e. CC /\ U:~H-->~H) /\ x e. ~H) -> ((A .op U)` x) = (A .h (U` x)))
24	23	3adantl2 1033	. . . . . . 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 4900	. . . . . 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 1928	. . . . 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 1929	. . . 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		hosval 11149	. . . . . 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 1067	. . . . 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		homulcl 11322	. . . . . . 7 |- ((A e. CC /\ T:~H-->~H) -> (A .op T):~H-->~H)
31		homulcl 11322	. . . . . . 7 |- ((A e. CC /\ U:~H-->~H) -> (A .op U):~H-->~H)
32	30, 31	anim12i 360	. . . . . 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 1152	. . . . 5 |- ((A e. CC /\ T:~H-->~H /\ U:~H-->~H) -> ((A .op T):~H-->~H /\ (A .op U):~H-->~H))
34	29, 33	sylan 497	. . . 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 1928	. . 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 2176	. 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		homulcl 11322	. . . . 5 |- ((A e. CC /\ (T +op U):~H-->~H) -> (A .op (T +op U)):~H-->~H)
38	37, 3	sylan2 500	. . . 4 |- ((A e. CC /\ (T:~H-->~H /\ U:~H-->~H)) -> (A .op (T +op U)):~H-->~H)
39	38	3impb 1063	. . 3 |- ((A e. CC /\ T:~H-->~H /\ U:~H-->~H) -> (A .op (T +op U)):~H-->~H)
40		hoaddcl 11321	. . . . 5 |- (((A .op T):~H-->~H /\ (A .op U):~H-->~H) -> ((A .op T) +op (A .op U)):~H-->~H)
41	40, 30, 31	syl2an 503	. . . 4 |- (((A e. CC /\ T:~H-->~H) /\ (A e. CC /\ U:~H-->~H)) -> ((A .op T) +op (A .op U)):~H-->~H)
42	41	3impdi 1152	. . 3 |- ((A e. CC /\ T:~H-->~H /\ U:~H-->~H) -> ((A .op T) +op (A .op U)):~H-->~H)
43		hoeq 11323	. . 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))))
44	39, 42, 43	syl11anc 524	. 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) <-> (A .op (T +op U)) = ((A .op T) +op (A .op U))))
45	36, 44	mpbid 212	1 |- ((A e. CC /\ T:~H-->~H /\ U:~H-->~H) -> (A .op (T +op U)) = ((A .op T) +op (A .op U)))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  -->wf 3994  ` cfv 3998  (class class class)co 4884  CCcc 6384  ~Hchil 10420   +h cva 10421   .h csm 10422   +op chos 10439   .op chot 10440

This theorem is referenced by:  hosubdi 11371  honegdi 11372  ho2times 11382  opsqrlem6 11716

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-hilex 10501  ax-hfvadd 10502  ax-hfvmul 10507  ax-hvdistr1 10510

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-fv 4014  df-opr 4886  df-oprab 4887  df-map 5383  df-hosum 11139  df-homul 11140

Copyright terms: Public domain