| Step | Hyp | Ref
| Expression |
| 1 | | coof.f |
. . . . 5
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
| 2 | 1 | ffvelcdmda 7104 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵) |
| 3 | | coof.g |
. . . . 5
⊢ (𝜑 → 𝐺:𝐴⟶𝐵) |
| 4 | 3 | ffvelcdmda 7104 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ∈ 𝐵) |
| 5 | | coof.2 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → (𝐻‘(𝑏𝑅𝑐)) = ((𝐻‘𝑏)𝑆(𝐻‘𝑐))) |
| 6 | 5 | ralrimivva 3202 |
. . . . 5
⊢ (𝜑 → ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 (𝐻‘(𝑏𝑅𝑐)) = ((𝐻‘𝑏)𝑆(𝐻‘𝑐))) |
| 7 | 6 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 (𝐻‘(𝑏𝑅𝑐)) = ((𝐻‘𝑏)𝑆(𝐻‘𝑐))) |
| 8 | | fvoveq1 7454 |
. . . . . 6
⊢ (𝑏 = (𝐹‘𝑥) → (𝐻‘(𝑏𝑅𝑐)) = (𝐻‘((𝐹‘𝑥)𝑅𝑐))) |
| 9 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑏 = (𝐹‘𝑥) → (𝐻‘𝑏) = (𝐻‘(𝐹‘𝑥))) |
| 10 | 9 | oveq1d 7446 |
. . . . . 6
⊢ (𝑏 = (𝐹‘𝑥) → ((𝐻‘𝑏)𝑆(𝐻‘𝑐)) = ((𝐻‘(𝐹‘𝑥))𝑆(𝐻‘𝑐))) |
| 11 | 8, 10 | eqeq12d 2753 |
. . . . 5
⊢ (𝑏 = (𝐹‘𝑥) → ((𝐻‘(𝑏𝑅𝑐)) = ((𝐻‘𝑏)𝑆(𝐻‘𝑐)) ↔ (𝐻‘((𝐹‘𝑥)𝑅𝑐)) = ((𝐻‘(𝐹‘𝑥))𝑆(𝐻‘𝑐)))) |
| 12 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑐 = (𝐺‘𝑥) → ((𝐹‘𝑥)𝑅𝑐) = ((𝐹‘𝑥)𝑅(𝐺‘𝑥))) |
| 13 | 12 | fveq2d 6910 |
. . . . . 6
⊢ (𝑐 = (𝐺‘𝑥) → (𝐻‘((𝐹‘𝑥)𝑅𝑐)) = (𝐻‘((𝐹‘𝑥)𝑅(𝐺‘𝑥)))) |
| 14 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑐 = (𝐺‘𝑥) → (𝐻‘𝑐) = (𝐻‘(𝐺‘𝑥))) |
| 15 | 14 | oveq2d 7447 |
. . . . . 6
⊢ (𝑐 = (𝐺‘𝑥) → ((𝐻‘(𝐹‘𝑥))𝑆(𝐻‘𝑐)) = ((𝐻‘(𝐹‘𝑥))𝑆(𝐻‘(𝐺‘𝑥)))) |
| 16 | 13, 15 | eqeq12d 2753 |
. . . . 5
⊢ (𝑐 = (𝐺‘𝑥) → ((𝐻‘((𝐹‘𝑥)𝑅𝑐)) = ((𝐻‘(𝐹‘𝑥))𝑆(𝐻‘𝑐)) ↔ (𝐻‘((𝐹‘𝑥)𝑅(𝐺‘𝑥))) = ((𝐻‘(𝐹‘𝑥))𝑆(𝐻‘(𝐺‘𝑥))))) |
| 17 | 11, 16 | rspc2va 3634 |
. . . 4
⊢ ((((𝐹‘𝑥) ∈ 𝐵 ∧ (𝐺‘𝑥) ∈ 𝐵) ∧ ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 (𝐻‘(𝑏𝑅𝑐)) = ((𝐻‘𝑏)𝑆(𝐻‘𝑐))) → (𝐻‘((𝐹‘𝑥)𝑅(𝐺‘𝑥))) = ((𝐻‘(𝐹‘𝑥))𝑆(𝐻‘(𝐺‘𝑥)))) |
| 18 | 2, 4, 7, 17 | syl21anc 838 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐻‘((𝐹‘𝑥)𝑅(𝐺‘𝑥))) = ((𝐻‘(𝐹‘𝑥))𝑆(𝐻‘(𝐺‘𝑥)))) |
| 19 | 18 | mpteq2dva 5242 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐻‘((𝐹‘𝑥)𝑅(𝐺‘𝑥)))) = (𝑥 ∈ 𝐴 ↦ ((𝐻‘(𝐹‘𝑥))𝑆(𝐻‘(𝐺‘𝑥))))) |
| 20 | 1 | ffnd 6737 |
. . . . 5
⊢ (𝜑 → 𝐹 Fn 𝐴) |
| 21 | 3 | ffnd 6737 |
. . . . 5
⊢ (𝜑 → 𝐺 Fn 𝐴) |
| 22 | | coof.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 23 | | inidm 4227 |
. . . . 5
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
| 24 | | eqidd 2738 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐹‘𝑥)) |
| 25 | | eqidd 2738 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = (𝐺‘𝑥)) |
| 26 | 20, 21, 22, 22, 23, 24, 25 | offval 7706 |
. . . 4
⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ 𝐴 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))) |
| 27 | 26 | coeq2d 5873 |
. . 3
⊢ (𝜑 → (𝐻 ∘ (𝐹 ∘f 𝑅𝐺)) = (𝐻 ∘ (𝑥 ∈ 𝐴 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))))) |
| 28 | | coof.h |
. . . . 5
⊢ (𝜑 → 𝐻 Fn 𝐵) |
| 29 | | dffn3 6748 |
. . . . 5
⊢ (𝐻 Fn 𝐵 ↔ 𝐻:𝐵⟶ran 𝐻) |
| 30 | 28, 29 | sylib 218 |
. . . 4
⊢ (𝜑 → 𝐻:𝐵⟶ran 𝐻) |
| 31 | 2, 4 | jca 511 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) ∈ 𝐵 ∧ (𝐺‘𝑥) ∈ 𝐵)) |
| 32 | | coof.1 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → (𝑏𝑅𝑐) ∈ 𝐵) |
| 33 | 32 | caovclg 7625 |
. . . . 5
⊢ ((𝜑 ∧ ((𝐹‘𝑥) ∈ 𝐵 ∧ (𝐺‘𝑥) ∈ 𝐵)) → ((𝐹‘𝑥)𝑅(𝐺‘𝑥)) ∈ 𝐵) |
| 34 | 31, 33 | syldan 591 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥)𝑅(𝐺‘𝑥)) ∈ 𝐵) |
| 35 | 30, 34 | cofmpt 7152 |
. . 3
⊢ (𝜑 → (𝐻 ∘ (𝑥 ∈ 𝐴 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))) = (𝑥 ∈ 𝐴 ↦ (𝐻‘((𝐹‘𝑥)𝑅(𝐺‘𝑥))))) |
| 36 | 27, 35 | eqtrd 2777 |
. 2
⊢ (𝜑 → (𝐻 ∘ (𝐹 ∘f 𝑅𝐺)) = (𝑥 ∈ 𝐴 ↦ (𝐻‘((𝐹‘𝑥)𝑅(𝐺‘𝑥))))) |
| 37 | | fnfco 6773 |
. . . 4
⊢ ((𝐻 Fn 𝐵 ∧ 𝐹:𝐴⟶𝐵) → (𝐻 ∘ 𝐹) Fn 𝐴) |
| 38 | 28, 1, 37 | syl2anc 584 |
. . 3
⊢ (𝜑 → (𝐻 ∘ 𝐹) Fn 𝐴) |
| 39 | | fnfco 6773 |
. . . 4
⊢ ((𝐻 Fn 𝐵 ∧ 𝐺:𝐴⟶𝐵) → (𝐻 ∘ 𝐺) Fn 𝐴) |
| 40 | 28, 3, 39 | syl2anc 584 |
. . 3
⊢ (𝜑 → (𝐻 ∘ 𝐺) Fn 𝐴) |
| 41 | | fvco2 7006 |
. . . 4
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐻 ∘ 𝐹)‘𝑥) = (𝐻‘(𝐹‘𝑥))) |
| 42 | 20, 41 | sylan 580 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐻 ∘ 𝐹)‘𝑥) = (𝐻‘(𝐹‘𝑥))) |
| 43 | | fvco2 7006 |
. . . 4
⊢ ((𝐺 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐻 ∘ 𝐺)‘𝑥) = (𝐻‘(𝐺‘𝑥))) |
| 44 | 21, 43 | sylan 580 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐻 ∘ 𝐺)‘𝑥) = (𝐻‘(𝐺‘𝑥))) |
| 45 | 38, 40, 22, 22, 23, 42, 44 | offval 7706 |
. 2
⊢ (𝜑 → ((𝐻 ∘ 𝐹) ∘f 𝑆(𝐻 ∘ 𝐺)) = (𝑥 ∈ 𝐴 ↦ ((𝐻‘(𝐹‘𝑥))𝑆(𝐻‘(𝐺‘𝑥))))) |
| 46 | 19, 36, 45 | 3eqtr4d 2787 |
1
⊢ (𝜑 → (𝐻 ∘ (𝐹 ∘f 𝑅𝐺)) = ((𝐻 ∘ 𝐹) ∘f 𝑆(𝐻 ∘ 𝐺))) |