Step | Hyp | Ref
| Expression |
1 | | fvco3 6810 |
. . . . . 6
⊢ ((𝑈: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) →
(((𝐴
·op 𝑇) ∘ 𝑈)‘𝑥) = ((𝐴 ·op 𝑇)‘(𝑈‘𝑥))) |
2 | 1 | 3ad2antl3 1189 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
→ (((𝐴
·op 𝑇) ∘ 𝑈)‘𝑥) = ((𝐴 ·op 𝑇)‘(𝑈‘𝑥))) |
3 | | fvco3 6810 |
. . . . . . . 8
⊢ ((𝑈: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) →
((𝑇 ∘ 𝑈)‘𝑥) = (𝑇‘(𝑈‘𝑥))) |
4 | 3 | 3ad2antl3 1189 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
→ ((𝑇 ∘ 𝑈)‘𝑥) = (𝑇‘(𝑈‘𝑥))) |
5 | 4 | oveq2d 7229 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
→ (𝐴
·ℎ ((𝑇 ∘ 𝑈)‘𝑥)) = (𝐴 ·ℎ (𝑇‘(𝑈‘𝑥)))) |
6 | | ffvelrn 6902 |
. . . . . . . . . 10
⊢ ((𝑈: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) →
(𝑈‘𝑥) ∈ ℋ) |
7 | | homval 29822 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
(𝑈‘𝑥) ∈ ℋ) → ((𝐴 ·op 𝑇)‘(𝑈‘𝑥)) = (𝐴 ·ℎ (𝑇‘(𝑈‘𝑥)))) |
8 | 6, 7 | syl3an3 1167 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
(𝑈: ℋ⟶ ℋ
∧ 𝑥 ∈ ℋ))
→ ((𝐴
·op 𝑇)‘(𝑈‘𝑥)) = (𝐴 ·ℎ (𝑇‘(𝑈‘𝑥)))) |
9 | 8 | 3expa 1120 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) ∧
(𝑈: ℋ⟶ ℋ
∧ 𝑥 ∈ ℋ))
→ ((𝐴
·op 𝑇)‘(𝑈‘𝑥)) = (𝐴 ·ℎ (𝑇‘(𝑈‘𝑥)))) |
10 | 9 | exp43 440 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (𝑇: ℋ⟶ ℋ →
(𝑈: ℋ⟶ ℋ
→ (𝑥 ∈ ℋ
→ ((𝐴
·op 𝑇)‘(𝑈‘𝑥)) = (𝐴 ·ℎ (𝑇‘(𝑈‘𝑥))))))) |
11 | 10 | 3imp1 1349 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
→ ((𝐴
·op 𝑇)‘(𝑈‘𝑥)) = (𝐴 ·ℎ (𝑇‘(𝑈‘𝑥)))) |
12 | 5, 11 | eqtr4d 2780 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
→ (𝐴
·ℎ ((𝑇 ∘ 𝑈)‘𝑥)) = ((𝐴 ·op 𝑇)‘(𝑈‘𝑥))) |
13 | 2, 12 | eqtr4d 2780 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
→ (((𝐴
·op 𝑇) ∘ 𝑈)‘𝑥) = (𝐴 ·ℎ ((𝑇 ∘ 𝑈)‘𝑥))) |
14 | | fco 6569 |
. . . . . . . 8
⊢ ((𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
→ (𝑇 ∘ 𝑈): ℋ⟶
ℋ) |
15 | | homval 29822 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ (𝑇 ∘ 𝑈): ℋ⟶ ℋ ∧ 𝑥 ∈ ℋ) → ((𝐴 ·op
(𝑇 ∘ 𝑈))‘𝑥) = (𝐴 ·ℎ ((𝑇 ∘ 𝑈)‘𝑥))) |
16 | 14, 15 | syl3an2 1166 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ (𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
→ ((𝐴
·op (𝑇 ∘ 𝑈))‘𝑥) = (𝐴 ·ℎ ((𝑇 ∘ 𝑈)‘𝑥))) |
17 | 16 | 3expia 1123 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ (𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶
ℋ)) → (𝑥 ∈
ℋ → ((𝐴
·op (𝑇 ∘ 𝑈))‘𝑥) = (𝐴 ·ℎ ((𝑇 ∘ 𝑈)‘𝑥)))) |
18 | 17 | 3impb 1117 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
→ (𝑥 ∈ ℋ
→ ((𝐴
·op (𝑇 ∘ 𝑈))‘𝑥) = (𝐴 ·ℎ ((𝑇 ∘ 𝑈)‘𝑥)))) |
19 | 18 | imp 410 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
→ ((𝐴
·op (𝑇 ∘ 𝑈))‘𝑥) = (𝐴 ·ℎ ((𝑇 ∘ 𝑈)‘𝑥))) |
20 | 13, 19 | eqtr4d 2780 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
∧ 𝑥 ∈ ℋ)
→ (((𝐴
·op 𝑇) ∘ 𝑈)‘𝑥) = ((𝐴 ·op (𝑇 ∘ 𝑈))‘𝑥)) |
21 | 20 | ralrimiva 3105 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
→ ∀𝑥 ∈
ℋ (((𝐴
·op 𝑇) ∘ 𝑈)‘𝑥) = ((𝐴 ·op (𝑇 ∘ 𝑈))‘𝑥)) |
22 | | homulcl 29840 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ)
→ (𝐴
·op 𝑇): ℋ⟶ ℋ) |
23 | | fco 6569 |
. . . 4
⊢ (((𝐴 ·op
𝑇): ℋ⟶ ℋ
∧ 𝑈: ℋ⟶
ℋ) → ((𝐴
·op 𝑇) ∘ 𝑈): ℋ⟶ ℋ) |
24 | 22, 23 | stoic3 1784 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
→ ((𝐴
·op 𝑇) ∘ 𝑈): ℋ⟶ ℋ) |
25 | | homulcl 29840 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ (𝑇 ∘ 𝑈): ℋ⟶ ℋ) → (𝐴 ·op
(𝑇 ∘ 𝑈)): ℋ⟶
ℋ) |
26 | 14, 25 | sylan2 596 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ (𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶
ℋ)) → (𝐴
·op (𝑇 ∘ 𝑈)): ℋ⟶
ℋ) |
27 | 26 | 3impb 1117 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
→ (𝐴
·op (𝑇 ∘ 𝑈)): ℋ⟶
ℋ) |
28 | | hoeq 29841 |
. . 3
⊢ ((((𝐴 ·op
𝑇) ∘ 𝑈): ℋ⟶ ℋ ∧
(𝐴
·op (𝑇 ∘ 𝑈)): ℋ⟶ ℋ) →
(∀𝑥 ∈ ℋ
(((𝐴
·op 𝑇) ∘ 𝑈)‘𝑥) = ((𝐴 ·op (𝑇 ∘ 𝑈))‘𝑥) ↔ ((𝐴 ·op 𝑇) ∘ 𝑈) = (𝐴 ·op (𝑇 ∘ 𝑈)))) |
29 | 24, 27, 28 | syl2anc 587 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
→ (∀𝑥 ∈
ℋ (((𝐴
·op 𝑇) ∘ 𝑈)‘𝑥) = ((𝐴 ·op (𝑇 ∘ 𝑈))‘𝑥) ↔ ((𝐴 ·op 𝑇) ∘ 𝑈) = (𝐴 ·op (𝑇 ∘ 𝑈)))) |
30 | 21, 29 | mpbid 235 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑈: ℋ⟶ ℋ)
→ ((𝐴
·op 𝑇) ∘ 𝑈) = (𝐴 ·op (𝑇 ∘ 𝑈))) |