| Step | Hyp | Ref
| Expression |
| 1 | | addcl 11237 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) |
| 2 | 1 | anim1i 615 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝑇: ℋ⟶ ℋ)
→ ((𝐴 + 𝐵) ∈ ℂ ∧ 𝑇: ℋ⟶
ℋ)) |
| 3 | 2 | 3impa 1110 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ)
→ ((𝐴 + 𝐵) ∈ ℂ ∧ 𝑇: ℋ⟶
ℋ)) |
| 4 | | homval 31760 |
. . . . . . 7
⊢ (((𝐴 + 𝐵) ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧ 𝑥 ∈ ℋ) → (((𝐴 + 𝐵) ·op 𝑇)‘𝑥) = ((𝐴 + 𝐵) ·ℎ (𝑇‘𝑥))) |
| 5 | 4 | 3expa 1119 |
. . . . . 6
⊢ ((((𝐴 + 𝐵) ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧ 𝑥 ∈ ℋ) → (((𝐴 + 𝐵) ·op 𝑇)‘𝑥) = ((𝐴 + 𝐵) ·ℎ (𝑇‘𝑥))) |
| 6 | 3, 5 | sylan 580 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
𝑥 ∈ ℋ) →
(((𝐴 + 𝐵) ·op 𝑇)‘𝑥) = ((𝐴 + 𝐵) ·ℎ (𝑇‘𝑥))) |
| 7 | | homval 31760 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) →
((𝐴
·op 𝑇)‘𝑥) = (𝐴 ·ℎ (𝑇‘𝑥))) |
| 8 | 7 | 3expa 1119 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
𝑥 ∈ ℋ) →
((𝐴
·op 𝑇)‘𝑥) = (𝐴 ·ℎ (𝑇‘𝑥))) |
| 9 | 8 | 3adantl2 1168 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
𝑥 ∈ ℋ) →
((𝐴
·op 𝑇)‘𝑥) = (𝐴 ·ℎ (𝑇‘𝑥))) |
| 10 | | homval 31760 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) →
((𝐵
·op 𝑇)‘𝑥) = (𝐵 ·ℎ (𝑇‘𝑥))) |
| 11 | 10 | 3expa 1119 |
. . . . . . . 8
⊢ (((𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
𝑥 ∈ ℋ) →
((𝐵
·op 𝑇)‘𝑥) = (𝐵 ·ℎ (𝑇‘𝑥))) |
| 12 | 11 | 3adantl1 1167 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
𝑥 ∈ ℋ) →
((𝐵
·op 𝑇)‘𝑥) = (𝐵 ·ℎ (𝑇‘𝑥))) |
| 13 | 9, 12 | oveq12d 7449 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
𝑥 ∈ ℋ) →
(((𝐴
·op 𝑇)‘𝑥) +ℎ ((𝐵 ·op 𝑇)‘𝑥)) = ((𝐴 ·ℎ (𝑇‘𝑥)) +ℎ (𝐵 ·ℎ (𝑇‘𝑥)))) |
| 14 | | ffvelcdm 7101 |
. . . . . . . . . 10
⊢ ((𝑇: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) →
(𝑇‘𝑥) ∈ ℋ) |
| 15 | | ax-hvdistr2 31028 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝑇‘𝑥) ∈ ℋ) → ((𝐴 + 𝐵) ·ℎ (𝑇‘𝑥)) = ((𝐴 ·ℎ (𝑇‘𝑥)) +ℎ (𝐵 ·ℎ (𝑇‘𝑥)))) |
| 16 | 14, 15 | syl3an3 1166 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝑇: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ)) →
((𝐴 + 𝐵) ·ℎ (𝑇‘𝑥)) = ((𝐴 ·ℎ (𝑇‘𝑥)) +ℎ (𝐵 ·ℎ (𝑇‘𝑥)))) |
| 17 | 16 | 3exp 1120 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (𝐵 ∈ ℂ → ((𝑇: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) →
((𝐴 + 𝐵) ·ℎ (𝑇‘𝑥)) = ((𝐴 ·ℎ (𝑇‘𝑥)) +ℎ (𝐵 ·ℎ (𝑇‘𝑥)))))) |
| 18 | 17 | exp4a 431 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (𝐵 ∈ ℂ → (𝑇: ℋ⟶ ℋ →
(𝑥 ∈ ℋ →
((𝐴 + 𝐵) ·ℎ (𝑇‘𝑥)) = ((𝐴 ·ℎ (𝑇‘𝑥)) +ℎ (𝐵 ·ℎ (𝑇‘𝑥))))))) |
| 19 | 18 | 3imp1 1348 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
𝑥 ∈ ℋ) →
((𝐴 + 𝐵) ·ℎ (𝑇‘𝑥)) = ((𝐴 ·ℎ (𝑇‘𝑥)) +ℎ (𝐵 ·ℎ (𝑇‘𝑥)))) |
| 20 | 13, 19 | eqtr4d 2780 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
𝑥 ∈ ℋ) →
(((𝐴
·op 𝑇)‘𝑥) +ℎ ((𝐵 ·op 𝑇)‘𝑥)) = ((𝐴 + 𝐵) ·ℎ (𝑇‘𝑥))) |
| 21 | 6, 20 | eqtr4d 2780 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
𝑥 ∈ ℋ) →
(((𝐴 + 𝐵) ·op 𝑇)‘𝑥) = (((𝐴 ·op 𝑇)‘𝑥) +ℎ ((𝐵 ·op 𝑇)‘𝑥))) |
| 22 | | homulcl 31778 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ)
→ (𝐴
·op 𝑇): ℋ⟶ ℋ) |
| 23 | | homulcl 31778 |
. . . . . . 7
⊢ ((𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ)
→ (𝐵
·op 𝑇): ℋ⟶ ℋ) |
| 24 | 22, 23 | anim12i 613 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
(𝐵 ∈ ℂ ∧
𝑇: ℋ⟶
ℋ)) → ((𝐴
·op 𝑇): ℋ⟶ ℋ ∧ (𝐵 ·op
𝑇): ℋ⟶
ℋ)) |
| 25 | 24 | 3impdir 1352 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ)
→ ((𝐴
·op 𝑇): ℋ⟶ ℋ ∧ (𝐵 ·op
𝑇): ℋ⟶
ℋ)) |
| 26 | | hosval 31759 |
. . . . . 6
⊢ (((𝐴 ·op
𝑇): ℋ⟶ ℋ
∧ (𝐵
·op 𝑇): ℋ⟶ ℋ ∧ 𝑥 ∈ ℋ) → (((𝐴 ·op
𝑇) +op (𝐵 ·op
𝑇))‘𝑥) = (((𝐴 ·op 𝑇)‘𝑥) +ℎ ((𝐵 ·op 𝑇)‘𝑥))) |
| 27 | 26 | 3expa 1119 |
. . . . 5
⊢ ((((𝐴 ·op
𝑇): ℋ⟶ ℋ
∧ (𝐵
·op 𝑇): ℋ⟶ ℋ) ∧ 𝑥 ∈ ℋ) → (((𝐴 ·op
𝑇) +op (𝐵 ·op
𝑇))‘𝑥) = (((𝐴 ·op 𝑇)‘𝑥) +ℎ ((𝐵 ·op 𝑇)‘𝑥))) |
| 28 | 25, 27 | sylan 580 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
𝑥 ∈ ℋ) →
(((𝐴
·op 𝑇) +op (𝐵 ·op 𝑇))‘𝑥) = (((𝐴 ·op 𝑇)‘𝑥) +ℎ ((𝐵 ·op 𝑇)‘𝑥))) |
| 29 | 21, 28 | eqtr4d 2780 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
𝑥 ∈ ℋ) →
(((𝐴 + 𝐵) ·op 𝑇)‘𝑥) = (((𝐴 ·op 𝑇) +op (𝐵 ·op
𝑇))‘𝑥)) |
| 30 | 29 | ralrimiva 3146 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ)
→ ∀𝑥 ∈
ℋ (((𝐴 + 𝐵) ·op
𝑇)‘𝑥) = (((𝐴 ·op 𝑇) +op (𝐵 ·op
𝑇))‘𝑥)) |
| 31 | | homulcl 31778 |
. . . 4
⊢ (((𝐴 + 𝐵) ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) → ((𝐴 + 𝐵) ·op 𝑇): ℋ⟶
ℋ) |
| 32 | 1, 31 | stoic3 1776 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ)
→ ((𝐴 + 𝐵) ·op
𝑇): ℋ⟶
ℋ) |
| 33 | | hoaddcl 31777 |
. . . . 5
⊢ (((𝐴 ·op
𝑇): ℋ⟶ ℋ
∧ (𝐵
·op 𝑇): ℋ⟶ ℋ) → ((𝐴 ·op
𝑇) +op (𝐵 ·op
𝑇)): ℋ⟶
ℋ) |
| 34 | 22, 23, 33 | syl2an 596 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
(𝐵 ∈ ℂ ∧
𝑇: ℋ⟶
ℋ)) → ((𝐴
·op 𝑇) +op (𝐵 ·op 𝑇)): ℋ⟶
ℋ) |
| 35 | 34 | 3impdir 1352 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ)
→ ((𝐴
·op 𝑇) +op (𝐵 ·op 𝑇)): ℋ⟶
ℋ) |
| 36 | | hoeq 31779 |
. . 3
⊢ ((((𝐴 + 𝐵) ·op 𝑇): ℋ⟶ ℋ ∧
((𝐴
·op 𝑇) +op (𝐵 ·op 𝑇)): ℋ⟶ ℋ)
→ (∀𝑥 ∈
ℋ (((𝐴 + 𝐵) ·op
𝑇)‘𝑥) = (((𝐴 ·op 𝑇) +op (𝐵 ·op
𝑇))‘𝑥) ↔ ((𝐴 + 𝐵) ·op 𝑇) = ((𝐴 ·op 𝑇) +op (𝐵 ·op
𝑇)))) |
| 37 | 32, 35, 36 | syl2anc 584 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ)
→ (∀𝑥 ∈
ℋ (((𝐴 + 𝐵) ·op
𝑇)‘𝑥) = (((𝐴 ·op 𝑇) +op (𝐵 ·op
𝑇))‘𝑥) ↔ ((𝐴 + 𝐵) ·op 𝑇) = ((𝐴 ·op 𝑇) +op (𝐵 ·op
𝑇)))) |
| 38 | 30, 37 | mpbid 232 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ)
→ ((𝐴 + 𝐵) ·op
𝑇) = ((𝐴 ·op 𝑇) +op (𝐵 ·op
𝑇))) |