Theorem homulass 29579

Description: Scalar product associative law for Hilbert space operators. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.)

Assertion

Ref	Expression
homulass	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) → ((𝐴 · 𝐵) ·op 𝑇) = (𝐴 ·op (𝐵 ·op 𝑇)))

Proof of Theorem homulass

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		mulcl 10621	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
2		homval 29518	. . . . . . . . 9 ⊢ (((𝐴 · 𝐵) ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑥 ∈ ℋ) → (((𝐴 · 𝐵) ·op 𝑇)‘𝑥) = ((𝐴 · 𝐵) ·ℎ (𝑇‘𝑥)))
3	1, 2	syl3an1 1159	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑥 ∈ ℋ) → (((𝐴 · 𝐵) ·op 𝑇)‘𝑥) = ((𝐴 · 𝐵) ·ℎ (𝑇‘𝑥)))
4	3	3expia 1117	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑇: ℋ⟶ ℋ) → (𝑥 ∈ ℋ → (((𝐴 · 𝐵) ·op 𝑇)‘𝑥) = ((𝐴 · 𝐵) ·ℎ (𝑇‘𝑥))))
5	4	3impa 1106	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) → (𝑥 ∈ ℋ → (((𝐴 · 𝐵) ·op 𝑇)‘𝑥) = ((𝐴 · 𝐵) ·ℎ (𝑇‘𝑥))))
6	5	imp 409	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧ 𝑥 ∈ ℋ) → (((𝐴 · 𝐵) ·op 𝑇)‘𝑥) = ((𝐴 · 𝐵) ·ℎ (𝑇‘𝑥)))
7		homval 29518	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑥 ∈ ℋ) → ((𝐵 ·op 𝑇)‘𝑥) = (𝐵 ·ℎ (𝑇‘𝑥)))
8	7	oveq2d 7172	. . . . . . . 8 ⊢ ((𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑥 ∈ ℋ) → (𝐴 ·ℎ ((𝐵 ·op 𝑇)‘𝑥)) = (𝐴 ·ℎ (𝐵 ·ℎ (𝑇‘𝑥))))
9	8	3expa 1114	. . . . . . 7 ⊢ (((𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧ 𝑥 ∈ ℋ) → (𝐴 ·ℎ ((𝐵 ·op 𝑇)‘𝑥)) = (𝐴 ·ℎ (𝐵 ·ℎ (𝑇‘𝑥))))
10	9	3adantl1 1162	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧ 𝑥 ∈ ℋ) → (𝐴 ·ℎ ((𝐵 ·op 𝑇)‘𝑥)) = (𝐴 ·ℎ (𝐵 ·ℎ (𝑇‘𝑥))))
11		ffvelrn 6849	. . . . . . . . . 10 ⊢ ((𝑇: ℋ⟶ ℋ ∧ 𝑥 ∈ ℋ) → (𝑇‘𝑥) ∈ ℋ)
12		ax-hvmulass 28784	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝑇‘𝑥) ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ (𝑇‘𝑥)) = (𝐴 ·ℎ (𝐵 ·ℎ (𝑇‘𝑥))))
13	11, 12	syl3an3 1161	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝑇: ℋ⟶ ℋ ∧ 𝑥 ∈ ℋ)) → ((𝐴 · 𝐵) ·ℎ (𝑇‘𝑥)) = (𝐴 ·ℎ (𝐵 ·ℎ (𝑇‘𝑥))))
14	13	3expa 1114	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑇: ℋ⟶ ℋ ∧ 𝑥 ∈ ℋ)) → ((𝐴 · 𝐵) ·ℎ (𝑇‘𝑥)) = (𝐴 ·ℎ (𝐵 ·ℎ (𝑇‘𝑥))))
15	14	exp43 439	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (𝐵 ∈ ℂ → (𝑇: ℋ⟶ ℋ → (𝑥 ∈ ℋ → ((𝐴 · 𝐵) ·ℎ (𝑇‘𝑥)) = (𝐴 ·ℎ (𝐵 ·ℎ (𝑇‘𝑥)))))))
16	15	3imp1 1343	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧ 𝑥 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ (𝑇‘𝑥)) = (𝐴 ·ℎ (𝐵 ·ℎ (𝑇‘𝑥))))
17	10, 16	eqtr4d 2859	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧ 𝑥 ∈ ℋ) → (𝐴 ·ℎ ((𝐵 ·op 𝑇)‘𝑥)) = ((𝐴 · 𝐵) ·ℎ (𝑇‘𝑥)))
18	6, 17	eqtr4d 2859	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧ 𝑥 ∈ ℋ) → (((𝐴 · 𝐵) ·op 𝑇)‘𝑥) = (𝐴 ·ℎ ((𝐵 ·op 𝑇)‘𝑥)))
19		homulcl 29536	. . . . . . . 8 ⊢ ((𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) → (𝐵 ·op 𝑇): ℋ⟶ ℋ)
20		homval 29518	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ·op 𝑇): ℋ⟶ ℋ ∧ 𝑥 ∈ ℋ) → ((𝐴 ·op (𝐵 ·op 𝑇))‘𝑥) = (𝐴 ·ℎ ((𝐵 ·op 𝑇)‘𝑥)))
21	19, 20	syl3an2 1160	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧ 𝑥 ∈ ℋ) → ((𝐴 ·op (𝐵 ·op 𝑇))‘𝑥) = (𝐴 ·ℎ ((𝐵 ·op 𝑇)‘𝑥)))
22	21	3expia 1117	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ)) → (𝑥 ∈ ℋ → ((𝐴 ·op (𝐵 ·op 𝑇))‘𝑥) = (𝐴 ·ℎ ((𝐵 ·op 𝑇)‘𝑥))))
23	22	3impb 1111	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) → (𝑥 ∈ ℋ → ((𝐴 ·op (𝐵 ·op 𝑇))‘𝑥) = (𝐴 ·ℎ ((𝐵 ·op 𝑇)‘𝑥))))
24	23	imp 409	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧ 𝑥 ∈ ℋ) → ((𝐴 ·op (𝐵 ·op 𝑇))‘𝑥) = (𝐴 ·ℎ ((𝐵 ·op 𝑇)‘𝑥)))
25	18, 24	eqtr4d 2859	. . 3 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧ 𝑥 ∈ ℋ) → (((𝐴 · 𝐵) ·op 𝑇)‘𝑥) = ((𝐴 ·op (𝐵 ·op 𝑇))‘𝑥))
26	25	ralrimiva 3182	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) → ∀𝑥 ∈ ℋ (((𝐴 · 𝐵) ·op 𝑇)‘𝑥) = ((𝐴 ·op (𝐵 ·op 𝑇))‘𝑥))
27		homulcl 29536	. . . 4 ⊢ (((𝐴 · 𝐵) ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) → ((𝐴 · 𝐵) ·op 𝑇): ℋ⟶ ℋ)
28	1, 27	stoic3 1777	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) → ((𝐴 · 𝐵) ·op 𝑇): ℋ⟶ ℋ)
29		homulcl 29536	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ·op 𝑇): ℋ⟶ ℋ) → (𝐴 ·op (𝐵 ·op 𝑇)): ℋ⟶ ℋ)
30	19, 29	sylan2 594	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ)) → (𝐴 ·op (𝐵 ·op 𝑇)): ℋ⟶ ℋ)
31	30	3impb 1111	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) → (𝐴 ·op (𝐵 ·op 𝑇)): ℋ⟶ ℋ)
32		hoeq 29537	. . 3 ⊢ ((((𝐴 · 𝐵) ·op 𝑇): ℋ⟶ ℋ ∧ (𝐴 ·op (𝐵 ·op 𝑇)): ℋ⟶ ℋ) → (∀𝑥 ∈ ℋ (((𝐴 · 𝐵) ·op 𝑇)‘𝑥) = ((𝐴 ·op (𝐵 ·op 𝑇))‘𝑥) ↔ ((𝐴 · 𝐵) ·op 𝑇) = (𝐴 ·op (𝐵 ·op 𝑇))))
33	28, 31, 32	syl2anc 586	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) → (∀𝑥 ∈ ℋ (((𝐴 · 𝐵) ·op 𝑇)‘𝑥) = ((𝐴 ·op (𝐵 ·op 𝑇))‘𝑥) ↔ ((𝐴 · 𝐵) ·op 𝑇) = (𝐴 ·op (𝐵 ·op 𝑇))))
34	26, 33	mpbid 234	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) → ((𝐴 · 𝐵) ·op 𝑇) = (𝐴 ·op (𝐵 ·op 𝑇)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114  ∀wral 3138  ⟶wf 6351  ‘cfv 6355  (class class class)co 7156  ℂcc 10535   · cmul 10542   ℋchba 28696   ·_ℎ csm 28698   ·_op chot 28716

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-rep 5190  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-mulcl 10599  ax-hilex 28776  ax-hfvmul 28782  ax-hvmulass 28784

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-ov 7159  df-oprab 7160  df-mpo 7161  df-map 8408  df-homul 29508

This theorem is referenced by:  homul12  29582  honegneg  29583  leopmul  29911  nmopleid  29916  opsqrlem1  29917  opsqrlem6  29922