Step | Hyp | Ref
| Expression |
1 | | eqidd 2779 |
. 2
⊢ (𝐷 ∈ 𝑉 → (𝐺 ↾s {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ∈ Fin}) = (𝐺 ↾s {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ∈ Fin})) |
2 | | eqidd 2779 |
. 2
⊢ (𝐷 ∈ 𝑉 → (0g‘𝐺) = (0g‘𝐺)) |
3 | | eqidd 2779 |
. 2
⊢ (𝐷 ∈ 𝑉 → (+g‘𝐺) = (+g‘𝐺)) |
4 | | ssrab2 3908 |
. . . 4
⊢ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ∈ Fin} ⊆ 𝐵 |
5 | | symgsssg.b |
. . . 4
⊢ 𝐵 = (Base‘𝐺) |
6 | 4, 5 | sseqtri 3856 |
. . 3
⊢ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ∈ Fin} ⊆
(Base‘𝐺) |
7 | 6 | a1i 11 |
. 2
⊢ (𝐷 ∈ 𝑉 → {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ∈ Fin} ⊆
(Base‘𝐺)) |
8 | | symgsssg.g |
. . . . 5
⊢ 𝐺 = (SymGrp‘𝐷) |
9 | 8 | symggrp 18203 |
. . . 4
⊢ (𝐷 ∈ 𝑉 → 𝐺 ∈ Grp) |
10 | | eqid 2778 |
. . . . 5
⊢
(0g‘𝐺) = (0g‘𝐺) |
11 | 5, 10 | grpidcl 17837 |
. . . 4
⊢ (𝐺 ∈ Grp →
(0g‘𝐺)
∈ 𝐵) |
12 | 9, 11 | syl 17 |
. . 3
⊢ (𝐷 ∈ 𝑉 → (0g‘𝐺) ∈ 𝐵) |
13 | 8 | symgid 18204 |
. . . . . 6
⊢ (𝐷 ∈ 𝑉 → ( I ↾ 𝐷) = (0g‘𝐺)) |
14 | 13 | difeq1d 3950 |
. . . . 5
⊢ (𝐷 ∈ 𝑉 → (( I ↾ 𝐷) ∖ I ) = ((0g‘𝐺) ∖ I )) |
15 | 14 | dmeqd 5571 |
. . . 4
⊢ (𝐷 ∈ 𝑉 → dom (( I ↾ 𝐷) ∖ I ) = dom
((0g‘𝐺)
∖ I )) |
16 | | resss 5671 |
. . . . . . . 8
⊢ ( I
↾ 𝐷) ⊆
I |
17 | | ssdif0 4172 |
. . . . . . . 8
⊢ (( I
↾ 𝐷) ⊆ I ↔
(( I ↾ 𝐷) ∖ I )
= ∅) |
18 | 16, 17 | mpbi 222 |
. . . . . . 7
⊢ (( I
↾ 𝐷) ∖ I ) =
∅ |
19 | 18 | dmeqi 5570 |
. . . . . 6
⊢ dom (( I
↾ 𝐷) ∖ I ) =
dom ∅ |
20 | | dm0 5584 |
. . . . . 6
⊢ dom
∅ = ∅ |
21 | 19, 20 | eqtri 2802 |
. . . . 5
⊢ dom (( I
↾ 𝐷) ∖ I ) =
∅ |
22 | | 0fin 8476 |
. . . . 5
⊢ ∅
∈ Fin |
23 | 21, 22 | eqeltri 2855 |
. . . 4
⊢ dom (( I
↾ 𝐷) ∖ I )
∈ Fin |
24 | 15, 23 | syl6eqelr 2868 |
. . 3
⊢ (𝐷 ∈ 𝑉 → dom ((0g‘𝐺) ∖ I ) ∈
Fin) |
25 | | difeq1 3944 |
. . . . . 6
⊢ (𝑥 = (0g‘𝐺) → (𝑥 ∖ I ) = ((0g‘𝐺) ∖ I )) |
26 | 25 | dmeqd 5571 |
. . . . 5
⊢ (𝑥 = (0g‘𝐺) → dom (𝑥 ∖ I ) = dom
((0g‘𝐺)
∖ I )) |
27 | 26 | eleq1d 2844 |
. . . 4
⊢ (𝑥 = (0g‘𝐺) → (dom (𝑥 ∖ I ) ∈ Fin ↔
dom ((0g‘𝐺) ∖ I ) ∈ Fin)) |
28 | 27 | elrab 3572 |
. . 3
⊢
((0g‘𝐺) ∈ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ∈ Fin} ↔
((0g‘𝐺)
∈ 𝐵 ∧ dom
((0g‘𝐺)
∖ I ) ∈ Fin)) |
29 | 12, 24, 28 | sylanbrc 578 |
. 2
⊢ (𝐷 ∈ 𝑉 → (0g‘𝐺) ∈ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ∈ Fin}) |
30 | | biid 253 |
. . 3
⊢ (𝐷 ∈ 𝑉 ↔ 𝐷 ∈ 𝑉) |
31 | | difeq1 3944 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑥 ∖ I ) = (𝑦 ∖ I )) |
32 | 31 | dmeqd 5571 |
. . . . 5
⊢ (𝑥 = 𝑦 → dom (𝑥 ∖ I ) = dom (𝑦 ∖ I )) |
33 | 32 | eleq1d 2844 |
. . . 4
⊢ (𝑥 = 𝑦 → (dom (𝑥 ∖ I ) ∈ Fin ↔ dom (𝑦 ∖ I ) ∈
Fin)) |
34 | 33 | elrab 3572 |
. . 3
⊢ (𝑦 ∈ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ∈ Fin} ↔ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ∈ Fin)) |
35 | | difeq1 3944 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (𝑥 ∖ I ) = (𝑧 ∖ I )) |
36 | 35 | dmeqd 5571 |
. . . . 5
⊢ (𝑥 = 𝑧 → dom (𝑥 ∖ I ) = dom (𝑧 ∖ I )) |
37 | 36 | eleq1d 2844 |
. . . 4
⊢ (𝑥 = 𝑧 → (dom (𝑥 ∖ I ) ∈ Fin ↔ dom (𝑧 ∖ I ) ∈
Fin)) |
38 | 37 | elrab 3572 |
. . 3
⊢ (𝑧 ∈ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ∈ Fin} ↔ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ∈ Fin)) |
39 | 9 | 3ad2ant1 1124 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ∈ Fin) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ∈ Fin)) → 𝐺 ∈ Grp) |
40 | | simp2l 1213 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ∈ Fin) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ∈ Fin)) → 𝑦 ∈ 𝐵) |
41 | | simp3l 1215 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ∈ Fin) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ∈ Fin)) → 𝑧 ∈ 𝐵) |
42 | | eqid 2778 |
. . . . . 6
⊢
(+g‘𝐺) = (+g‘𝐺) |
43 | 5, 42 | grpcl 17817 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝑦(+g‘𝐺)𝑧) ∈ 𝐵) |
44 | 39, 40, 41, 43 | syl3anc 1439 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ∈ Fin) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ∈ Fin)) → (𝑦(+g‘𝐺)𝑧) ∈ 𝐵) |
45 | 8, 5, 42 | symgov 18193 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝑦(+g‘𝐺)𝑧) = (𝑦 ∘ 𝑧)) |
46 | 40, 41, 45 | syl2anc 579 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ∈ Fin) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ∈ Fin)) → (𝑦(+g‘𝐺)𝑧) = (𝑦 ∘ 𝑧)) |
47 | 46 | difeq1d 3950 |
. . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ∈ Fin) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ∈ Fin)) → ((𝑦(+g‘𝐺)𝑧) ∖ I ) = ((𝑦 ∘ 𝑧) ∖ I )) |
48 | 47 | dmeqd 5571 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ∈ Fin) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ∈ Fin)) → dom ((𝑦(+g‘𝐺)𝑧) ∖ I ) = dom ((𝑦 ∘ 𝑧) ∖ I )) |
49 | | simp2r 1214 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ∈ Fin) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ∈ Fin)) → dom (𝑦 ∖ I ) ∈
Fin) |
50 | | simp3r 1216 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ∈ Fin) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ∈ Fin)) → dom (𝑧 ∖ I ) ∈
Fin) |
51 | | unfi 8515 |
. . . . . . 7
⊢ ((dom
(𝑦 ∖ I ) ∈ Fin
∧ dom (𝑧 ∖ I )
∈ Fin) → (dom (𝑦
∖ I ) ∪ dom (𝑧
∖ I )) ∈ Fin) |
52 | 49, 50, 51 | syl2anc 579 |
. . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ∈ Fin) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ∈ Fin)) → (dom (𝑦 ∖ I ) ∪ dom (𝑧 ∖ I )) ∈
Fin) |
53 | | mvdco 18248 |
. . . . . 6
⊢ dom
((𝑦 ∘ 𝑧) ∖ I ) ⊆ (dom
(𝑦 ∖ I ) ∪ dom
(𝑧 ∖ I
)) |
54 | | ssfi 8468 |
. . . . . 6
⊢ (((dom
(𝑦 ∖ I ) ∪ dom
(𝑧 ∖ I )) ∈ Fin
∧ dom ((𝑦 ∘ 𝑧) ∖ I ) ⊆ (dom
(𝑦 ∖ I ) ∪ dom
(𝑧 ∖ I ))) → dom
((𝑦 ∘ 𝑧) ∖ I ) ∈
Fin) |
55 | 52, 53, 54 | sylancl 580 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ∈ Fin) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ∈ Fin)) → dom ((𝑦 ∘ 𝑧) ∖ I ) ∈ Fin) |
56 | 48, 55 | eqeltrd 2859 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ∈ Fin) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ∈ Fin)) → dom ((𝑦(+g‘𝐺)𝑧) ∖ I ) ∈ Fin) |
57 | | difeq1 3944 |
. . . . . . 7
⊢ (𝑥 = (𝑦(+g‘𝐺)𝑧) → (𝑥 ∖ I ) = ((𝑦(+g‘𝐺)𝑧) ∖ I )) |
58 | 57 | dmeqd 5571 |
. . . . . 6
⊢ (𝑥 = (𝑦(+g‘𝐺)𝑧) → dom (𝑥 ∖ I ) = dom ((𝑦(+g‘𝐺)𝑧) ∖ I )) |
59 | 58 | eleq1d 2844 |
. . . . 5
⊢ (𝑥 = (𝑦(+g‘𝐺)𝑧) → (dom (𝑥 ∖ I ) ∈ Fin ↔ dom ((𝑦(+g‘𝐺)𝑧) ∖ I ) ∈ Fin)) |
60 | 59 | elrab 3572 |
. . . 4
⊢ ((𝑦(+g‘𝐺)𝑧) ∈ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ∈ Fin} ↔ ((𝑦(+g‘𝐺)𝑧) ∈ 𝐵 ∧ dom ((𝑦(+g‘𝐺)𝑧) ∖ I ) ∈ Fin)) |
61 | 44, 56, 60 | sylanbrc 578 |
. . 3
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ∈ Fin) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ∈ Fin)) → (𝑦(+g‘𝐺)𝑧) ∈ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ∈ Fin}) |
62 | 30, 34, 38, 61 | syl3anb 1161 |
. 2
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ∈ Fin} ∧ 𝑧 ∈ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ∈ Fin}) → (𝑦(+g‘𝐺)𝑧) ∈ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ∈ Fin}) |
63 | 9 | adantr 474 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ∈ Fin)) → 𝐺 ∈ Grp) |
64 | | simprl 761 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ∈ Fin)) → 𝑦 ∈ 𝐵) |
65 | | eqid 2778 |
. . . . . 6
⊢
(invg‘𝐺) = (invg‘𝐺) |
66 | 5, 65 | grpinvcl 17854 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ 𝐵) → ((invg‘𝐺)‘𝑦) ∈ 𝐵) |
67 | 63, 64, 66 | syl2anc 579 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ∈ Fin)) →
((invg‘𝐺)‘𝑦) ∈ 𝐵) |
68 | 8, 5, 65 | symginv 18205 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐵 → ((invg‘𝐺)‘𝑦) = ◡𝑦) |
69 | 68 | ad2antrl 718 |
. . . . . . . 8
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ∈ Fin)) →
((invg‘𝐺)‘𝑦) = ◡𝑦) |
70 | 69 | difeq1d 3950 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ∈ Fin)) →
(((invg‘𝐺)‘𝑦) ∖ I ) = (◡𝑦 ∖ I )) |
71 | 70 | dmeqd 5571 |
. . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ∈ Fin)) → dom
(((invg‘𝐺)‘𝑦) ∖ I ) = dom (◡𝑦 ∖ I )) |
72 | 8, 5 | symgbasf1o 18186 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐵 → 𝑦:𝐷–1-1-onto→𝐷) |
73 | 72 | ad2antrl 718 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ∈ Fin)) → 𝑦:𝐷–1-1-onto→𝐷) |
74 | | f1omvdcnv 18247 |
. . . . . . 7
⊢ (𝑦:𝐷–1-1-onto→𝐷 → dom (◡𝑦 ∖ I ) = dom (𝑦 ∖ I )) |
75 | 73, 74 | syl 17 |
. . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ∈ Fin)) → dom (◡𝑦 ∖ I ) = dom (𝑦 ∖ I )) |
76 | 71, 75 | eqtrd 2814 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ∈ Fin)) → dom
(((invg‘𝐺)‘𝑦) ∖ I ) = dom (𝑦 ∖ I )) |
77 | | simprr 763 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ∈ Fin)) → dom (𝑦 ∖ I ) ∈
Fin) |
78 | 76, 77 | eqeltrd 2859 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ∈ Fin)) → dom
(((invg‘𝐺)‘𝑦) ∖ I ) ∈ Fin) |
79 | | difeq1 3944 |
. . . . . . 7
⊢ (𝑥 = ((invg‘𝐺)‘𝑦) → (𝑥 ∖ I ) = (((invg‘𝐺)‘𝑦) ∖ I )) |
80 | 79 | dmeqd 5571 |
. . . . . 6
⊢ (𝑥 = ((invg‘𝐺)‘𝑦) → dom (𝑥 ∖ I ) = dom
(((invg‘𝐺)‘𝑦) ∖ I )) |
81 | 80 | eleq1d 2844 |
. . . . 5
⊢ (𝑥 = ((invg‘𝐺)‘𝑦) → (dom (𝑥 ∖ I ) ∈ Fin ↔ dom
(((invg‘𝐺)‘𝑦) ∖ I ) ∈ Fin)) |
82 | 81 | elrab 3572 |
. . . 4
⊢
(((invg‘𝐺)‘𝑦) ∈ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ∈ Fin} ↔
(((invg‘𝐺)‘𝑦) ∈ 𝐵 ∧ dom (((invg‘𝐺)‘𝑦) ∖ I ) ∈ Fin)) |
83 | 67, 78, 82 | sylanbrc 578 |
. . 3
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ∈ Fin)) →
((invg‘𝐺)‘𝑦) ∈ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ∈ Fin}) |
84 | 34, 83 | sylan2b 587 |
. 2
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ∈ Fin}) →
((invg‘𝐺)‘𝑦) ∈ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ∈ Fin}) |
85 | 1, 2, 3, 7, 29, 62, 84, 9 | issubgrpd2 17994 |
1
⊢ (𝐷 ∈ 𝑉 → {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ∈ Fin} ∈
(SubGrp‘𝐺)) |