Proof of Theorem fvcosymgeq
Step | Hyp | Ref
| Expression |
1 | | gsmsymgrfix.s |
. . . . . . 7
⊢ 𝑆 = (SymGrp‘𝑁) |
2 | | gsmsymgrfix.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑆) |
3 | 1, 2 | symgbasf 17804 |
. . . . . 6
⊢ (𝐺 ∈ 𝐵 → 𝐺:𝑁⟶𝑁) |
4 | | ffn 6045 |
. . . . . 6
⊢ (𝐺:𝑁⟶𝑁 → 𝐺 Fn 𝑁) |
5 | 3, 4 | syl 17 |
. . . . 5
⊢ (𝐺 ∈ 𝐵 → 𝐺 Fn 𝑁) |
6 | | gsmsymgreq.z |
. . . . . . 7
⊢ 𝑍 = (SymGrp‘𝑀) |
7 | | gsmsymgreq.p |
. . . . . . 7
⊢ 𝑃 = (Base‘𝑍) |
8 | 6, 7 | symgbasf 17804 |
. . . . . 6
⊢ (𝐾 ∈ 𝑃 → 𝐾:𝑀⟶𝑀) |
9 | | ffn 6045 |
. . . . . 6
⊢ (𝐾:𝑀⟶𝑀 → 𝐾 Fn 𝑀) |
10 | 8, 9 | syl 17 |
. . . . 5
⊢ (𝐾 ∈ 𝑃 → 𝐾 Fn 𝑀) |
11 | 5, 10 | anim12i 590 |
. . . 4
⊢ ((𝐺 ∈ 𝐵 ∧ 𝐾 ∈ 𝑃) → (𝐺 Fn 𝑁 ∧ 𝐾 Fn 𝑀)) |
12 | 11 | adantr 481 |
. . 3
⊢ (((𝐺 ∈ 𝐵 ∧ 𝐾 ∈ 𝑃) ∧ (𝑋 ∈ 𝐼 ∧ (𝐺‘𝑋) = (𝐾‘𝑋) ∧ ∀𝑛 ∈ 𝐼 (𝐹‘𝑛) = (𝐻‘𝑛))) → (𝐺 Fn 𝑁 ∧ 𝐾 Fn 𝑀)) |
13 | | gsmsymgreq.i |
. . . . . . . 8
⊢ 𝐼 = (𝑁 ∩ 𝑀) |
14 | 13 | eleq2i 2693 |
. . . . . . 7
⊢ (𝑋 ∈ 𝐼 ↔ 𝑋 ∈ (𝑁 ∩ 𝑀)) |
15 | 14 | biimpi 206 |
. . . . . 6
⊢ (𝑋 ∈ 𝐼 → 𝑋 ∈ (𝑁 ∩ 𝑀)) |
16 | 15 | 3ad2ant1 1082 |
. . . . 5
⊢ ((𝑋 ∈ 𝐼 ∧ (𝐺‘𝑋) = (𝐾‘𝑋) ∧ ∀𝑛 ∈ 𝐼 (𝐹‘𝑛) = (𝐻‘𝑛)) → 𝑋 ∈ (𝑁 ∩ 𝑀)) |
17 | 16 | adantl 482 |
. . . 4
⊢ (((𝐺 ∈ 𝐵 ∧ 𝐾 ∈ 𝑃) ∧ (𝑋 ∈ 𝐼 ∧ (𝐺‘𝑋) = (𝐾‘𝑋) ∧ ∀𝑛 ∈ 𝐼 (𝐹‘𝑛) = (𝐻‘𝑛))) → 𝑋 ∈ (𝑁 ∩ 𝑀)) |
18 | | simpr2 1068 |
. . . 4
⊢ (((𝐺 ∈ 𝐵 ∧ 𝐾 ∈ 𝑃) ∧ (𝑋 ∈ 𝐼 ∧ (𝐺‘𝑋) = (𝐾‘𝑋) ∧ ∀𝑛 ∈ 𝐼 (𝐹‘𝑛) = (𝐻‘𝑛))) → (𝐺‘𝑋) = (𝐾‘𝑋)) |
19 | 1, 2 | symgbasf1o 17803 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ 𝐵 → 𝐺:𝑁–1-1-onto→𝑁) |
20 | | dff1o5 6146 |
. . . . . . . . . . . 12
⊢ (𝐺:𝑁–1-1-onto→𝑁 ↔ (𝐺:𝑁–1-1→𝑁 ∧ ran 𝐺 = 𝑁)) |
21 | | eqcom 2629 |
. . . . . . . . . . . . . 14
⊢ (ran
𝐺 = 𝑁 ↔ 𝑁 = ran 𝐺) |
22 | 21 | biimpi 206 |
. . . . . . . . . . . . 13
⊢ (ran
𝐺 = 𝑁 → 𝑁 = ran 𝐺) |
23 | 22 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝐺:𝑁–1-1→𝑁 ∧ ran 𝐺 = 𝑁) → 𝑁 = ran 𝐺) |
24 | 20, 23 | sylbi 207 |
. . . . . . . . . . 11
⊢ (𝐺:𝑁–1-1-onto→𝑁 → 𝑁 = ran 𝐺) |
25 | 19, 24 | syl 17 |
. . . . . . . . . 10
⊢ (𝐺 ∈ 𝐵 → 𝑁 = ran 𝐺) |
26 | 6, 7 | symgbasf1o 17803 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ 𝑃 → 𝐾:𝑀–1-1-onto→𝑀) |
27 | | dff1o5 6146 |
. . . . . . . . . . . 12
⊢ (𝐾:𝑀–1-1-onto→𝑀 ↔ (𝐾:𝑀–1-1→𝑀 ∧ ran 𝐾 = 𝑀)) |
28 | | eqcom 2629 |
. . . . . . . . . . . . . 14
⊢ (ran
𝐾 = 𝑀 ↔ 𝑀 = ran 𝐾) |
29 | 28 | biimpi 206 |
. . . . . . . . . . . . 13
⊢ (ran
𝐾 = 𝑀 → 𝑀 = ran 𝐾) |
30 | 29 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝐾:𝑀–1-1→𝑀 ∧ ran 𝐾 = 𝑀) → 𝑀 = ran 𝐾) |
31 | 27, 30 | sylbi 207 |
. . . . . . . . . . 11
⊢ (𝐾:𝑀–1-1-onto→𝑀 → 𝑀 = ran 𝐾) |
32 | 26, 31 | syl 17 |
. . . . . . . . . 10
⊢ (𝐾 ∈ 𝑃 → 𝑀 = ran 𝐾) |
33 | 25, 32 | ineqan12d 3816 |
. . . . . . . . 9
⊢ ((𝐺 ∈ 𝐵 ∧ 𝐾 ∈ 𝑃) → (𝑁 ∩ 𝑀) = (ran 𝐺 ∩ ran 𝐾)) |
34 | 13, 33 | syl5eq 2668 |
. . . . . . . 8
⊢ ((𝐺 ∈ 𝐵 ∧ 𝐾 ∈ 𝑃) → 𝐼 = (ran 𝐺 ∩ ran 𝐾)) |
35 | 34 | raleqdv 3144 |
. . . . . . 7
⊢ ((𝐺 ∈ 𝐵 ∧ 𝐾 ∈ 𝑃) → (∀𝑛 ∈ 𝐼 (𝐹‘𝑛) = (𝐻‘𝑛) ↔ ∀𝑛 ∈ (ran 𝐺 ∩ ran 𝐾)(𝐹‘𝑛) = (𝐻‘𝑛))) |
36 | 35 | biimpcd 239 |
. . . . . 6
⊢
(∀𝑛 ∈
𝐼 (𝐹‘𝑛) = (𝐻‘𝑛) → ((𝐺 ∈ 𝐵 ∧ 𝐾 ∈ 𝑃) → ∀𝑛 ∈ (ran 𝐺 ∩ ran 𝐾)(𝐹‘𝑛) = (𝐻‘𝑛))) |
37 | 36 | 3ad2ant3 1084 |
. . . . 5
⊢ ((𝑋 ∈ 𝐼 ∧ (𝐺‘𝑋) = (𝐾‘𝑋) ∧ ∀𝑛 ∈ 𝐼 (𝐹‘𝑛) = (𝐻‘𝑛)) → ((𝐺 ∈ 𝐵 ∧ 𝐾 ∈ 𝑃) → ∀𝑛 ∈ (ran 𝐺 ∩ ran 𝐾)(𝐹‘𝑛) = (𝐻‘𝑛))) |
38 | 37 | impcom 446 |
. . . 4
⊢ (((𝐺 ∈ 𝐵 ∧ 𝐾 ∈ 𝑃) ∧ (𝑋 ∈ 𝐼 ∧ (𝐺‘𝑋) = (𝐾‘𝑋) ∧ ∀𝑛 ∈ 𝐼 (𝐹‘𝑛) = (𝐻‘𝑛))) → ∀𝑛 ∈ (ran 𝐺 ∩ ran 𝐾)(𝐹‘𝑛) = (𝐻‘𝑛)) |
39 | 17, 18, 38 | 3jca 1242 |
. . 3
⊢ (((𝐺 ∈ 𝐵 ∧ 𝐾 ∈ 𝑃) ∧ (𝑋 ∈ 𝐼 ∧ (𝐺‘𝑋) = (𝐾‘𝑋) ∧ ∀𝑛 ∈ 𝐼 (𝐹‘𝑛) = (𝐻‘𝑛))) → (𝑋 ∈ (𝑁 ∩ 𝑀) ∧ (𝐺‘𝑋) = (𝐾‘𝑋) ∧ ∀𝑛 ∈ (ran 𝐺 ∩ ran 𝐾)(𝐹‘𝑛) = (𝐻‘𝑛))) |
40 | | fvcofneq 6367 |
. . 3
⊢ ((𝐺 Fn 𝑁 ∧ 𝐾 Fn 𝑀) → ((𝑋 ∈ (𝑁 ∩ 𝑀) ∧ (𝐺‘𝑋) = (𝐾‘𝑋) ∧ ∀𝑛 ∈ (ran 𝐺 ∩ ran 𝐾)(𝐹‘𝑛) = (𝐻‘𝑛)) → ((𝐹 ∘ 𝐺)‘𝑋) = ((𝐻 ∘ 𝐾)‘𝑋))) |
41 | 12, 39, 40 | sylc 65 |
. 2
⊢ (((𝐺 ∈ 𝐵 ∧ 𝐾 ∈ 𝑃) ∧ (𝑋 ∈ 𝐼 ∧ (𝐺‘𝑋) = (𝐾‘𝑋) ∧ ∀𝑛 ∈ 𝐼 (𝐹‘𝑛) = (𝐻‘𝑛))) → ((𝐹 ∘ 𝐺)‘𝑋) = ((𝐻 ∘ 𝐾)‘𝑋)) |
42 | 41 | ex 450 |
1
⊢ ((𝐺 ∈ 𝐵 ∧ 𝐾 ∈ 𝑃) → ((𝑋 ∈ 𝐼 ∧ (𝐺‘𝑋) = (𝐾‘𝑋) ∧ ∀𝑛 ∈ 𝐼 (𝐹‘𝑛) = (𝐻‘𝑛)) → ((𝐹 ∘ 𝐺)‘𝑋) = ((𝐻 ∘ 𝐾)‘𝑋))) |