Step | Hyp | Ref
| Expression |
1 | | simpl1 1192 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
→ 𝐴 ∈
ℂ) |
2 | | ffvelrn 6862 |
. . . . . . 7
⊢ ((𝑇: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) →
(𝑇‘𝑥) ∈ ℋ) |
3 | 2 | 3ad2antl2 1187 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
→ (𝑇‘𝑥) ∈
ℋ) |
4 | | ffvelrn 6862 |
. . . . . . 7
⊢ ((𝑈: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) →
(𝑈‘𝑥) ∈ ℋ) |
5 | 4 | 3ad2antl3 1188 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
→ (𝑈‘𝑥) ∈
ℋ) |
6 | | ax-hvdistr1 28946 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ (𝑇‘𝑥) ∈ ℋ ∧ (𝑈‘𝑥) ∈ ℋ) → (𝐴 ·ℎ ((𝑇‘𝑥) +ℎ (𝑈‘𝑥))) = ((𝐴 ·ℎ (𝑇‘𝑥)) +ℎ (𝐴 ·ℎ (𝑈‘𝑥)))) |
7 | 1, 3, 5, 6 | syl3anc 1372 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
→ (𝐴
·ℎ ((𝑇‘𝑥) +ℎ (𝑈‘𝑥))) = ((𝐴 ·ℎ (𝑇‘𝑥)) +ℎ (𝐴 ·ℎ (𝑈‘𝑥)))) |
8 | | hosval 29678 |
. . . . . . . 8
⊢ ((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ
∧ 𝑥 ∈ ℋ)
→ ((𝑇 +op
𝑈)‘𝑥) = ((𝑇‘𝑥) +ℎ (𝑈‘𝑥))) |
9 | 8 | oveq2d 7189 |
. . . . . . 7
⊢ ((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ
∧ 𝑥 ∈ ℋ)
→ (𝐴
·ℎ ((𝑇 +op 𝑈)‘𝑥)) = (𝐴 ·ℎ ((𝑇‘𝑥) +ℎ (𝑈‘𝑥)))) |
10 | 9 | 3expa 1119 |
. . . . . 6
⊢ (((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
→ (𝐴
·ℎ ((𝑇 +op 𝑈)‘𝑥)) = (𝐴 ·ℎ ((𝑇‘𝑥) +ℎ (𝑈‘𝑥)))) |
11 | 10 | 3adantl1 1167 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
→ (𝐴
·ℎ ((𝑇 +op 𝑈)‘𝑥)) = (𝐴 ·ℎ ((𝑇‘𝑥) +ℎ (𝑈‘𝑥)))) |
12 | | homval 29679 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) →
((𝐴
·op 𝑇)‘𝑥) = (𝐴 ·ℎ (𝑇‘𝑥))) |
13 | 12 | 3expa 1119 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
𝑥 ∈ ℋ) →
((𝐴
·op 𝑇)‘𝑥) = (𝐴 ·ℎ (𝑇‘𝑥))) |
14 | 13 | 3adantl3 1169 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
→ ((𝐴
·op 𝑇)‘𝑥) = (𝐴 ·ℎ (𝑇‘𝑥))) |
15 | | homval 29679 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑈: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) →
((𝐴
·op 𝑈)‘𝑥) = (𝐴 ·ℎ (𝑈‘𝑥))) |
16 | 15 | 3expa 1119 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑈: ℋ⟶ ℋ) ∧
𝑥 ∈ ℋ) →
((𝐴
·op 𝑈)‘𝑥) = (𝐴 ·ℎ (𝑈‘𝑥))) |
17 | 16 | 3adantl2 1168 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
→ ((𝐴
·op 𝑈)‘𝑥) = (𝐴 ·ℎ (𝑈‘𝑥))) |
18 | 14, 17 | oveq12d 7191 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
→ (((𝐴
·op 𝑇)‘𝑥) +ℎ ((𝐴 ·op 𝑈)‘𝑥)) = ((𝐴 ·ℎ (𝑇‘𝑥)) +ℎ (𝐴 ·ℎ (𝑈‘𝑥)))) |
19 | 7, 11, 18 | 3eqtr4d 2784 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
→ (𝐴
·ℎ ((𝑇 +op 𝑈)‘𝑥)) = (((𝐴 ·op 𝑇)‘𝑥) +ℎ ((𝐴 ·op 𝑈)‘𝑥))) |
20 | | hoaddcl 29696 |
. . . . . . 7
⊢ ((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
→ (𝑇 +op
𝑈): ℋ⟶
ℋ) |
21 | 20 | anim2i 620 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ (𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶
ℋ)) → (𝐴 ∈
ℂ ∧ (𝑇
+op 𝑈):
ℋ⟶ ℋ)) |
22 | 21 | 3impb 1116 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
→ (𝐴 ∈ ℂ
∧ (𝑇 +op
𝑈): ℋ⟶
ℋ)) |
23 | | homval 29679 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ (𝑇 +op 𝑈): ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) →
((𝐴
·op (𝑇 +op 𝑈))‘𝑥) = (𝐴 ·ℎ ((𝑇 +op 𝑈)‘𝑥))) |
24 | 23 | 3expa 1119 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ (𝑇 +op 𝑈): ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
→ ((𝐴
·op (𝑇 +op 𝑈))‘𝑥) = (𝐴 ·ℎ ((𝑇 +op 𝑈)‘𝑥))) |
25 | 22, 24 | sylan 583 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
→ ((𝐴
·op (𝑇 +op 𝑈))‘𝑥) = (𝐴 ·ℎ ((𝑇 +op 𝑈)‘𝑥))) |
26 | | homulcl 29697 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ)
→ (𝐴
·op 𝑇): ℋ⟶ ℋ) |
27 | | homulcl 29697 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑈: ℋ⟶ ℋ)
→ (𝐴
·op 𝑈): ℋ⟶ ℋ) |
28 | 26, 27 | anim12i 616 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
(𝐴 ∈ ℂ ∧
𝑈: ℋ⟶
ℋ)) → ((𝐴
·op 𝑇): ℋ⟶ ℋ ∧ (𝐴 ·op
𝑈): ℋ⟶
ℋ)) |
29 | 28 | 3impdi 1351 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
→ ((𝐴
·op 𝑇): ℋ⟶ ℋ ∧ (𝐴 ·op
𝑈): ℋ⟶
ℋ)) |
30 | | hosval 29678 |
. . . . . 6
⊢ (((𝐴 ·op
𝑇): ℋ⟶ ℋ
∧ (𝐴
·op 𝑈): ℋ⟶ ℋ ∧ 𝑥 ∈ ℋ) → (((𝐴 ·op
𝑇) +op (𝐴 ·op
𝑈))‘𝑥) = (((𝐴 ·op 𝑇)‘𝑥) +ℎ ((𝐴 ·op 𝑈)‘𝑥))) |
31 | 30 | 3expa 1119 |
. . . . 5
⊢ ((((𝐴 ·op
𝑇): ℋ⟶ ℋ
∧ (𝐴
·op 𝑈): ℋ⟶ ℋ) ∧ 𝑥 ∈ ℋ) → (((𝐴 ·op
𝑇) +op (𝐴 ·op
𝑈))‘𝑥) = (((𝐴 ·op 𝑇)‘𝑥) +ℎ ((𝐴 ·op 𝑈)‘𝑥))) |
32 | 29, 31 | sylan 583 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
→ (((𝐴
·op 𝑇) +op (𝐴 ·op 𝑈))‘𝑥) = (((𝐴 ·op 𝑇)‘𝑥) +ℎ ((𝐴 ·op 𝑈)‘𝑥))) |
33 | 19, 25, 32 | 3eqtr4d 2784 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
→ ((𝐴
·op (𝑇 +op 𝑈))‘𝑥) = (((𝐴 ·op 𝑇) +op (𝐴 ·op
𝑈))‘𝑥)) |
34 | 33 | ralrimiva 3097 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
→ ∀𝑥 ∈
ℋ ((𝐴
·op (𝑇 +op 𝑈))‘𝑥) = (((𝐴 ·op 𝑇) +op (𝐴 ·op
𝑈))‘𝑥)) |
35 | | homulcl 29697 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ (𝑇 +op 𝑈): ℋ⟶ ℋ)
→ (𝐴
·op (𝑇 +op 𝑈)): ℋ⟶
ℋ) |
36 | 20, 35 | sylan2 596 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ (𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶
ℋ)) → (𝐴
·op (𝑇 +op 𝑈)): ℋ⟶
ℋ) |
37 | 36 | 3impb 1116 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
→ (𝐴
·op (𝑇 +op 𝑈)): ℋ⟶
ℋ) |
38 | | hoaddcl 29696 |
. . . . 5
⊢ (((𝐴 ·op
𝑇): ℋ⟶ ℋ
∧ (𝐴
·op 𝑈): ℋ⟶ ℋ) → ((𝐴 ·op
𝑇) +op (𝐴 ·op
𝑈)): ℋ⟶
ℋ) |
39 | 26, 27, 38 | syl2an 599 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
(𝐴 ∈ ℂ ∧
𝑈: ℋ⟶
ℋ)) → ((𝐴
·op 𝑇) +op (𝐴 ·op 𝑈)): ℋ⟶
ℋ) |
40 | 39 | 3impdi 1351 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
→ ((𝐴
·op 𝑇) +op (𝐴 ·op 𝑈)): ℋ⟶
ℋ) |
41 | | hoeq 29698 |
. . 3
⊢ (((𝐴 ·op
(𝑇 +op 𝑈)): ℋ⟶ ℋ
∧ ((𝐴
·op 𝑇) +op (𝐴 ·op 𝑈)): ℋ⟶ ℋ)
→ (∀𝑥 ∈
ℋ ((𝐴
·op (𝑇 +op 𝑈))‘𝑥) = (((𝐴 ·op 𝑇) +op (𝐴 ·op
𝑈))‘𝑥) ↔ (𝐴 ·op (𝑇 +op 𝑈)) = ((𝐴 ·op 𝑇) +op (𝐴 ·op
𝑈)))) |
42 | 37, 40, 41 | syl2anc 587 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
→ (∀𝑥 ∈
ℋ ((𝐴
·op (𝑇 +op 𝑈))‘𝑥) = (((𝐴 ·op 𝑇) +op (𝐴 ·op
𝑈))‘𝑥) ↔ (𝐴 ·op (𝑇 +op 𝑈)) = ((𝐴 ·op 𝑇) +op (𝐴 ·op
𝑈)))) |
43 | 34, 42 | mpbid 235 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
→ (𝐴
·op (𝑇 +op 𝑈)) = ((𝐴 ·op 𝑇) +op (𝐴 ·op
𝑈))) |