Step | Hyp | Ref
| Expression |
1 | | mulcl 10955 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ) |
2 | | homval 30103 |
. . . . . . . . 9
⊢ (((𝐴 · 𝐵) ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑥 ∈ ℋ) → (((𝐴 · 𝐵) ·op 𝑇)‘𝑥) = ((𝐴 · 𝐵) ·ℎ (𝑇‘𝑥))) |
3 | 1, 2 | syl3an1 1162 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑇: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) →
(((𝐴 · 𝐵) ·op
𝑇)‘𝑥) = ((𝐴 · 𝐵) ·ℎ (𝑇‘𝑥))) |
4 | 3 | 3expia 1120 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑇: ℋ⟶ ℋ)
→ (𝑥 ∈ ℋ
→ (((𝐴 · 𝐵) ·op
𝑇)‘𝑥) = ((𝐴 · 𝐵) ·ℎ (𝑇‘𝑥)))) |
5 | 4 | 3impa 1109 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ)
→ (𝑥 ∈ ℋ
→ (((𝐴 · 𝐵) ·op
𝑇)‘𝑥) = ((𝐴 · 𝐵) ·ℎ (𝑇‘𝑥)))) |
6 | 5 | imp 407 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
𝑥 ∈ ℋ) →
(((𝐴 · 𝐵) ·op
𝑇)‘𝑥) = ((𝐴 · 𝐵) ·ℎ (𝑇‘𝑥))) |
7 | | homval 30103 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) →
((𝐵
·op 𝑇)‘𝑥) = (𝐵 ·ℎ (𝑇‘𝑥))) |
8 | 7 | oveq2d 7291 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) →
(𝐴
·ℎ ((𝐵 ·op 𝑇)‘𝑥)) = (𝐴 ·ℎ (𝐵
·ℎ (𝑇‘𝑥)))) |
9 | 8 | 3expa 1117 |
. . . . . . 7
⊢ (((𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
𝑥 ∈ ℋ) →
(𝐴
·ℎ ((𝐵 ·op 𝑇)‘𝑥)) = (𝐴 ·ℎ (𝐵
·ℎ (𝑇‘𝑥)))) |
10 | 9 | 3adantl1 1165 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
𝑥 ∈ ℋ) →
(𝐴
·ℎ ((𝐵 ·op 𝑇)‘𝑥)) = (𝐴 ·ℎ (𝐵
·ℎ (𝑇‘𝑥)))) |
11 | | ffvelrn 6959 |
. . . . . . . . . 10
⊢ ((𝑇: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) →
(𝑇‘𝑥) ∈ ℋ) |
12 | | ax-hvmulass 29369 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝑇‘𝑥) ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ (𝑇‘𝑥)) = (𝐴 ·ℎ (𝐵
·ℎ (𝑇‘𝑥)))) |
13 | 11, 12 | syl3an3 1164 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝑇: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ)) →
((𝐴 · 𝐵)
·ℎ (𝑇‘𝑥)) = (𝐴 ·ℎ (𝐵
·ℎ (𝑇‘𝑥)))) |
14 | 13 | 3expa 1117 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝑇: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ)) →
((𝐴 · 𝐵)
·ℎ (𝑇‘𝑥)) = (𝐴 ·ℎ (𝐵
·ℎ (𝑇‘𝑥)))) |
15 | 14 | exp43 437 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (𝐵 ∈ ℂ → (𝑇: ℋ⟶ ℋ →
(𝑥 ∈ ℋ →
((𝐴 · 𝐵)
·ℎ (𝑇‘𝑥)) = (𝐴 ·ℎ (𝐵
·ℎ (𝑇‘𝑥))))))) |
16 | 15 | 3imp1 1346 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
𝑥 ∈ ℋ) →
((𝐴 · 𝐵)
·ℎ (𝑇‘𝑥)) = (𝐴 ·ℎ (𝐵
·ℎ (𝑇‘𝑥)))) |
17 | 10, 16 | eqtr4d 2781 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
𝑥 ∈ ℋ) →
(𝐴
·ℎ ((𝐵 ·op 𝑇)‘𝑥)) = ((𝐴 · 𝐵) ·ℎ (𝑇‘𝑥))) |
18 | 6, 17 | eqtr4d 2781 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
𝑥 ∈ ℋ) →
(((𝐴 · 𝐵) ·op
𝑇)‘𝑥) = (𝐴 ·ℎ ((𝐵 ·op
𝑇)‘𝑥))) |
19 | | homulcl 30121 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ)
→ (𝐵
·op 𝑇): ℋ⟶ ℋ) |
20 | | homval 30103 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ·op
𝑇): ℋ⟶ ℋ
∧ 𝑥 ∈ ℋ)
→ ((𝐴
·op (𝐵 ·op 𝑇))‘𝑥) = (𝐴 ·ℎ ((𝐵 ·op
𝑇)‘𝑥))) |
21 | 19, 20 | syl3an2 1163 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
𝑥 ∈ ℋ) →
((𝐴
·op (𝐵 ·op 𝑇))‘𝑥) = (𝐴 ·ℎ ((𝐵 ·op
𝑇)‘𝑥))) |
22 | 21 | 3expia 1120 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ))
→ (𝑥 ∈ ℋ
→ ((𝐴
·op (𝐵 ·op 𝑇))‘𝑥) = (𝐴 ·ℎ ((𝐵 ·op
𝑇)‘𝑥)))) |
23 | 22 | 3impb 1114 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ)
→ (𝑥 ∈ ℋ
→ ((𝐴
·op (𝐵 ·op 𝑇))‘𝑥) = (𝐴 ·ℎ ((𝐵 ·op
𝑇)‘𝑥)))) |
24 | 23 | imp 407 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
𝑥 ∈ ℋ) →
((𝐴
·op (𝐵 ·op 𝑇))‘𝑥) = (𝐴 ·ℎ ((𝐵 ·op
𝑇)‘𝑥))) |
25 | 18, 24 | eqtr4d 2781 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
𝑥 ∈ ℋ) →
(((𝐴 · 𝐵) ·op
𝑇)‘𝑥) = ((𝐴 ·op (𝐵 ·op
𝑇))‘𝑥)) |
26 | 25 | ralrimiva 3103 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ)
→ ∀𝑥 ∈
ℋ (((𝐴 · 𝐵) ·op
𝑇)‘𝑥) = ((𝐴 ·op (𝐵 ·op
𝑇))‘𝑥)) |
27 | | homulcl 30121 |
. . . 4
⊢ (((𝐴 · 𝐵) ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) → ((𝐴 · 𝐵) ·op 𝑇): ℋ⟶
ℋ) |
28 | 1, 27 | stoic3 1779 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ)
→ ((𝐴 · 𝐵) ·op
𝑇): ℋ⟶
ℋ) |
29 | | homulcl 30121 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ·op
𝑇): ℋ⟶
ℋ) → (𝐴
·op (𝐵 ·op 𝑇)): ℋ⟶
ℋ) |
30 | 19, 29 | sylan2 593 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ))
→ (𝐴
·op (𝐵 ·op 𝑇)): ℋ⟶
ℋ) |
31 | 30 | 3impb 1114 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ)
→ (𝐴
·op (𝐵 ·op 𝑇)): ℋ⟶
ℋ) |
32 | | hoeq 30122 |
. . 3
⊢ ((((𝐴 · 𝐵) ·op 𝑇): ℋ⟶ ℋ ∧
(𝐴
·op (𝐵 ·op 𝑇)): ℋ⟶ ℋ)
→ (∀𝑥 ∈
ℋ (((𝐴 · 𝐵) ·op
𝑇)‘𝑥) = ((𝐴 ·op (𝐵 ·op
𝑇))‘𝑥) ↔ ((𝐴 · 𝐵) ·op 𝑇) = (𝐴 ·op (𝐵 ·op
𝑇)))) |
33 | 28, 31, 32 | syl2anc 584 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ)
→ (∀𝑥 ∈
ℋ (((𝐴 · 𝐵) ·op
𝑇)‘𝑥) = ((𝐴 ·op (𝐵 ·op
𝑇))‘𝑥) ↔ ((𝐴 · 𝐵) ·op 𝑇) = (𝐴 ·op (𝐵 ·op
𝑇)))) |
34 | 26, 33 | mpbid 231 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ)
→ ((𝐴 · 𝐵) ·op
𝑇) = (𝐴 ·op (𝐵 ·op
𝑇))) |