Proof of Theorem fvcofneq
Step | Hyp | Ref
| Expression |
1 | | simpl 472 |
. . . 4
⊢ ((𝐺 Fn 𝐴 ∧ 𝐾 Fn 𝐵) → 𝐺 Fn 𝐴) |
2 | | elin 3758 |
. . . . . 6
⊢ (𝑋 ∈ (𝐴 ∩ 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵)) |
3 | | simpl 472 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → 𝑋 ∈ 𝐴) |
4 | 2, 3 | sylbi 206 |
. . . . 5
⊢ (𝑋 ∈ (𝐴 ∩ 𝐵) → 𝑋 ∈ 𝐴) |
5 | 4 | 3ad2ant1 1075 |
. . . 4
⊢ ((𝑋 ∈ (𝐴 ∩ 𝐵) ∧ (𝐺‘𝑋) = (𝐾‘𝑋) ∧ ∀𝑥 ∈ (ran 𝐺 ∩ ran 𝐾)(𝐹‘𝑥) = (𝐻‘𝑥)) → 𝑋 ∈ 𝐴) |
6 | | fvco2 6183 |
. . . 4
⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘ 𝐺)‘𝑋) = (𝐹‘(𝐺‘𝑋))) |
7 | 1, 5, 6 | syl2an 493 |
. . 3
⊢ (((𝐺 Fn 𝐴 ∧ 𝐾 Fn 𝐵) ∧ (𝑋 ∈ (𝐴 ∩ 𝐵) ∧ (𝐺‘𝑋) = (𝐾‘𝑋) ∧ ∀𝑥 ∈ (ran 𝐺 ∩ ran 𝐾)(𝐹‘𝑥) = (𝐻‘𝑥))) → ((𝐹 ∘ 𝐺)‘𝑋) = (𝐹‘(𝐺‘𝑋))) |
8 | | simpr 476 |
. . . . 5
⊢ ((𝐺 Fn 𝐴 ∧ 𝐾 Fn 𝐵) → 𝐾 Fn 𝐵) |
9 | | simpr 476 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → 𝑋 ∈ 𝐵) |
10 | 2, 9 | sylbi 206 |
. . . . . 6
⊢ (𝑋 ∈ (𝐴 ∩ 𝐵) → 𝑋 ∈ 𝐵) |
11 | 10 | 3ad2ant1 1075 |
. . . . 5
⊢ ((𝑋 ∈ (𝐴 ∩ 𝐵) ∧ (𝐺‘𝑋) = (𝐾‘𝑋) ∧ ∀𝑥 ∈ (ran 𝐺 ∩ ran 𝐾)(𝐹‘𝑥) = (𝐻‘𝑥)) → 𝑋 ∈ 𝐵) |
12 | | fvco2 6183 |
. . . . 5
⊢ ((𝐾 Fn 𝐵 ∧ 𝑋 ∈ 𝐵) → ((𝐻 ∘ 𝐾)‘𝑋) = (𝐻‘(𝐾‘𝑋))) |
13 | 8, 11, 12 | syl2an 493 |
. . . 4
⊢ (((𝐺 Fn 𝐴 ∧ 𝐾 Fn 𝐵) ∧ (𝑋 ∈ (𝐴 ∩ 𝐵) ∧ (𝐺‘𝑋) = (𝐾‘𝑋) ∧ ∀𝑥 ∈ (ran 𝐺 ∩ ran 𝐾)(𝐹‘𝑥) = (𝐻‘𝑥))) → ((𝐻 ∘ 𝐾)‘𝑋) = (𝐻‘(𝐾‘𝑋))) |
14 | | fveq2 6103 |
. . . . . . 7
⊢ ((𝐾‘𝑋) = (𝐺‘𝑋) → (𝐻‘(𝐾‘𝑋)) = (𝐻‘(𝐺‘𝑋))) |
15 | 14 | eqcoms 2618 |
. . . . . 6
⊢ ((𝐺‘𝑋) = (𝐾‘𝑋) → (𝐻‘(𝐾‘𝑋)) = (𝐻‘(𝐺‘𝑋))) |
16 | 15 | 3ad2ant2 1076 |
. . . . 5
⊢ ((𝑋 ∈ (𝐴 ∩ 𝐵) ∧ (𝐺‘𝑋) = (𝐾‘𝑋) ∧ ∀𝑥 ∈ (ran 𝐺 ∩ ran 𝐾)(𝐹‘𝑥) = (𝐻‘𝑥)) → (𝐻‘(𝐾‘𝑋)) = (𝐻‘(𝐺‘𝑋))) |
17 | 16 | adantl 481 |
. . . 4
⊢ (((𝐺 Fn 𝐴 ∧ 𝐾 Fn 𝐵) ∧ (𝑋 ∈ (𝐴 ∩ 𝐵) ∧ (𝐺‘𝑋) = (𝐾‘𝑋) ∧ ∀𝑥 ∈ (ran 𝐺 ∩ ran 𝐾)(𝐹‘𝑥) = (𝐻‘𝑥))) → (𝐻‘(𝐾‘𝑋)) = (𝐻‘(𝐺‘𝑋))) |
18 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝐺 Fn 𝐴 → 𝐺 Fn 𝐴) |
19 | | fnfvelrn 6264 |
. . . . . . . . . . . 12
⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝐺‘𝑋) ∈ ran 𝐺) |
20 | 18, 4, 19 | syl2anr 494 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ (𝐴 ∩ 𝐵) ∧ 𝐺 Fn 𝐴) → (𝐺‘𝑋) ∈ ran 𝐺) |
21 | 20 | ex 449 |
. . . . . . . . . 10
⊢ (𝑋 ∈ (𝐴 ∩ 𝐵) → (𝐺 Fn 𝐴 → (𝐺‘𝑋) ∈ ran 𝐺)) |
22 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝐾 Fn 𝐵 → 𝐾 Fn 𝐵) |
23 | | fnfvelrn 6264 |
. . . . . . . . . . . 12
⊢ ((𝐾 Fn 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝐾‘𝑋) ∈ ran 𝐾) |
24 | 22, 10, 23 | syl2anr 494 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ (𝐴 ∩ 𝐵) ∧ 𝐾 Fn 𝐵) → (𝐾‘𝑋) ∈ ran 𝐾) |
25 | 24 | ex 449 |
. . . . . . . . . 10
⊢ (𝑋 ∈ (𝐴 ∩ 𝐵) → (𝐾 Fn 𝐵 → (𝐾‘𝑋) ∈ ran 𝐾)) |
26 | 21, 25 | anim12d 584 |
. . . . . . . . 9
⊢ (𝑋 ∈ (𝐴 ∩ 𝐵) → ((𝐺 Fn 𝐴 ∧ 𝐾 Fn 𝐵) → ((𝐺‘𝑋) ∈ ran 𝐺 ∧ (𝐾‘𝑋) ∈ ran 𝐾))) |
27 | | eleq1 2676 |
. . . . . . . . . . . 12
⊢ ((𝐾‘𝑋) = (𝐺‘𝑋) → ((𝐾‘𝑋) ∈ ran 𝐾 ↔ (𝐺‘𝑋) ∈ ran 𝐾)) |
28 | 27 | eqcoms 2618 |
. . . . . . . . . . 11
⊢ ((𝐺‘𝑋) = (𝐾‘𝑋) → ((𝐾‘𝑋) ∈ ran 𝐾 ↔ (𝐺‘𝑋) ∈ ran 𝐾)) |
29 | 28 | anbi2d 736 |
. . . . . . . . . 10
⊢ ((𝐺‘𝑋) = (𝐾‘𝑋) → (((𝐺‘𝑋) ∈ ran 𝐺 ∧ (𝐾‘𝑋) ∈ ran 𝐾) ↔ ((𝐺‘𝑋) ∈ ran 𝐺 ∧ (𝐺‘𝑋) ∈ ran 𝐾))) |
30 | | elin 3758 |
. . . . . . . . . . 11
⊢ ((𝐺‘𝑋) ∈ (ran 𝐺 ∩ ran 𝐾) ↔ ((𝐺‘𝑋) ∈ ran 𝐺 ∧ (𝐺‘𝑋) ∈ ran 𝐾)) |
31 | 30 | biimpri 217 |
. . . . . . . . . 10
⊢ (((𝐺‘𝑋) ∈ ran 𝐺 ∧ (𝐺‘𝑋) ∈ ran 𝐾) → (𝐺‘𝑋) ∈ (ran 𝐺 ∩ ran 𝐾)) |
32 | 29, 31 | syl6bi 242 |
. . . . . . . . 9
⊢ ((𝐺‘𝑋) = (𝐾‘𝑋) → (((𝐺‘𝑋) ∈ ran 𝐺 ∧ (𝐾‘𝑋) ∈ ran 𝐾) → (𝐺‘𝑋) ∈ (ran 𝐺 ∩ ran 𝐾))) |
33 | 26, 32 | sylan9 687 |
. . . . . . . 8
⊢ ((𝑋 ∈ (𝐴 ∩ 𝐵) ∧ (𝐺‘𝑋) = (𝐾‘𝑋)) → ((𝐺 Fn 𝐴 ∧ 𝐾 Fn 𝐵) → (𝐺‘𝑋) ∈ (ran 𝐺 ∩ ran 𝐾))) |
34 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝐺‘𝑋) → (𝐹‘𝑥) = (𝐹‘(𝐺‘𝑋))) |
35 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝐺‘𝑋) → (𝐻‘𝑥) = (𝐻‘(𝐺‘𝑋))) |
36 | 34, 35 | eqeq12d 2625 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝐺‘𝑋) → ((𝐹‘𝑥) = (𝐻‘𝑥) ↔ (𝐹‘(𝐺‘𝑋)) = (𝐻‘(𝐺‘𝑋)))) |
37 | 36 | rspcva 3280 |
. . . . . . . . . 10
⊢ (((𝐺‘𝑋) ∈ (ran 𝐺 ∩ ran 𝐾) ∧ ∀𝑥 ∈ (ran 𝐺 ∩ ran 𝐾)(𝐹‘𝑥) = (𝐻‘𝑥)) → (𝐹‘(𝐺‘𝑋)) = (𝐻‘(𝐺‘𝑋))) |
38 | 37 | eqcomd 2616 |
. . . . . . . . 9
⊢ (((𝐺‘𝑋) ∈ (ran 𝐺 ∩ ran 𝐾) ∧ ∀𝑥 ∈ (ran 𝐺 ∩ ran 𝐾)(𝐹‘𝑥) = (𝐻‘𝑥)) → (𝐻‘(𝐺‘𝑋)) = (𝐹‘(𝐺‘𝑋))) |
39 | 38 | ex 449 |
. . . . . . . 8
⊢ ((𝐺‘𝑋) ∈ (ran 𝐺 ∩ ran 𝐾) → (∀𝑥 ∈ (ran 𝐺 ∩ ran 𝐾)(𝐹‘𝑥) = (𝐻‘𝑥) → (𝐻‘(𝐺‘𝑋)) = (𝐹‘(𝐺‘𝑋)))) |
40 | 33, 39 | syl6 34 |
. . . . . . 7
⊢ ((𝑋 ∈ (𝐴 ∩ 𝐵) ∧ (𝐺‘𝑋) = (𝐾‘𝑋)) → ((𝐺 Fn 𝐴 ∧ 𝐾 Fn 𝐵) → (∀𝑥 ∈ (ran 𝐺 ∩ ran 𝐾)(𝐹‘𝑥) = (𝐻‘𝑥) → (𝐻‘(𝐺‘𝑋)) = (𝐹‘(𝐺‘𝑋))))) |
41 | 40 | com23 84 |
. . . . . 6
⊢ ((𝑋 ∈ (𝐴 ∩ 𝐵) ∧ (𝐺‘𝑋) = (𝐾‘𝑋)) → (∀𝑥 ∈ (ran 𝐺 ∩ ran 𝐾)(𝐹‘𝑥) = (𝐻‘𝑥) → ((𝐺 Fn 𝐴 ∧ 𝐾 Fn 𝐵) → (𝐻‘(𝐺‘𝑋)) = (𝐹‘(𝐺‘𝑋))))) |
42 | 41 | 3impia 1253 |
. . . . 5
⊢ ((𝑋 ∈ (𝐴 ∩ 𝐵) ∧ (𝐺‘𝑋) = (𝐾‘𝑋) ∧ ∀𝑥 ∈ (ran 𝐺 ∩ ran 𝐾)(𝐹‘𝑥) = (𝐻‘𝑥)) → ((𝐺 Fn 𝐴 ∧ 𝐾 Fn 𝐵) → (𝐻‘(𝐺‘𝑋)) = (𝐹‘(𝐺‘𝑋)))) |
43 | 42 | impcom 445 |
. . . 4
⊢ (((𝐺 Fn 𝐴 ∧ 𝐾 Fn 𝐵) ∧ (𝑋 ∈ (𝐴 ∩ 𝐵) ∧ (𝐺‘𝑋) = (𝐾‘𝑋) ∧ ∀𝑥 ∈ (ran 𝐺 ∩ ran 𝐾)(𝐹‘𝑥) = (𝐻‘𝑥))) → (𝐻‘(𝐺‘𝑋)) = (𝐹‘(𝐺‘𝑋))) |
44 | 13, 17, 43 | 3eqtrrd 2649 |
. . 3
⊢ (((𝐺 Fn 𝐴 ∧ 𝐾 Fn 𝐵) ∧ (𝑋 ∈ (𝐴 ∩ 𝐵) ∧ (𝐺‘𝑋) = (𝐾‘𝑋) ∧ ∀𝑥 ∈ (ran 𝐺 ∩ ran 𝐾)(𝐹‘𝑥) = (𝐻‘𝑥))) → (𝐹‘(𝐺‘𝑋)) = ((𝐻 ∘ 𝐾)‘𝑋)) |
45 | 7, 44 | eqtrd 2644 |
. 2
⊢ (((𝐺 Fn 𝐴 ∧ 𝐾 Fn 𝐵) ∧ (𝑋 ∈ (𝐴 ∩ 𝐵) ∧ (𝐺‘𝑋) = (𝐾‘𝑋) ∧ ∀𝑥 ∈ (ran 𝐺 ∩ ran 𝐾)(𝐹‘𝑥) = (𝐻‘𝑥))) → ((𝐹 ∘ 𝐺)‘𝑋) = ((𝐻 ∘ 𝐾)‘𝑋)) |
46 | 45 | ex 449 |
1
⊢ ((𝐺 Fn 𝐴 ∧ 𝐾 Fn 𝐵) → ((𝑋 ∈ (𝐴 ∩ 𝐵) ∧ (𝐺‘𝑋) = (𝐾‘𝑋) ∧ ∀𝑥 ∈ (ran 𝐺 ∩ ran 𝐾)(𝐹‘𝑥) = (𝐻‘𝑥)) → ((𝐹 ∘ 𝐺)‘𝑋) = ((𝐻 ∘ 𝐾)‘𝑋))) |