Step | Hyp | Ref
| Expression |
1 | | eqidd 2738 |
. 2
⊢ (𝐷 ∈ 𝑉 → (𝐺 ↾s {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ⊆ 𝑋}) = (𝐺 ↾s {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ⊆ 𝑋})) |
2 | | eqidd 2738 |
. 2
⊢ (𝐷 ∈ 𝑉 → (0g‘𝐺) = (0g‘𝐺)) |
3 | | eqidd 2738 |
. 2
⊢ (𝐷 ∈ 𝑉 → (+g‘𝐺) = (+g‘𝐺)) |
4 | | ssrab2 3993 |
. . . 4
⊢ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ⊆ 𝑋} ⊆ 𝐵 |
5 | | symgsssg.b |
. . . 4
⊢ 𝐵 = (Base‘𝐺) |
6 | 4, 5 | sseqtri 3937 |
. . 3
⊢ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ⊆ 𝑋} ⊆ (Base‘𝐺) |
7 | 6 | a1i 11 |
. 2
⊢ (𝐷 ∈ 𝑉 → {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ⊆ 𝑋} ⊆ (Base‘𝐺)) |
8 | | difeq1 4030 |
. . . . 5
⊢ (𝑥 = (0g‘𝐺) → (𝑥 ∖ I ) = ((0g‘𝐺) ∖ I )) |
9 | 8 | dmeqd 5774 |
. . . 4
⊢ (𝑥 = (0g‘𝐺) → dom (𝑥 ∖ I ) = dom
((0g‘𝐺)
∖ I )) |
10 | 9 | sseq1d 3932 |
. . 3
⊢ (𝑥 = (0g‘𝐺) → (dom (𝑥 ∖ I ) ⊆ 𝑋 ↔ dom
((0g‘𝐺)
∖ I ) ⊆ 𝑋)) |
11 | | symgsssg.g |
. . . . 5
⊢ 𝐺 = (SymGrp‘𝐷) |
12 | 11 | symggrp 18792 |
. . . 4
⊢ (𝐷 ∈ 𝑉 → 𝐺 ∈ Grp) |
13 | | eqid 2737 |
. . . . 5
⊢
(0g‘𝐺) = (0g‘𝐺) |
14 | 5, 13 | grpidcl 18395 |
. . . 4
⊢ (𝐺 ∈ Grp →
(0g‘𝐺)
∈ 𝐵) |
15 | 12, 14 | syl 17 |
. . 3
⊢ (𝐷 ∈ 𝑉 → (0g‘𝐺) ∈ 𝐵) |
16 | 11 | symgid 18793 |
. . . . . 6
⊢ (𝐷 ∈ 𝑉 → ( I ↾ 𝐷) = (0g‘𝐺)) |
17 | 16 | difeq1d 4036 |
. . . . 5
⊢ (𝐷 ∈ 𝑉 → (( I ↾ 𝐷) ∖ I ) = ((0g‘𝐺) ∖ I )) |
18 | 17 | dmeqd 5774 |
. . . 4
⊢ (𝐷 ∈ 𝑉 → dom (( I ↾ 𝐷) ∖ I ) = dom
((0g‘𝐺)
∖ I )) |
19 | | resss 5876 |
. . . . . . . 8
⊢ ( I
↾ 𝐷) ⊆
I |
20 | | ssdif0 4278 |
. . . . . . . 8
⊢ (( I
↾ 𝐷) ⊆ I ↔
(( I ↾ 𝐷) ∖ I )
= ∅) |
21 | 19, 20 | mpbi 233 |
. . . . . . 7
⊢ (( I
↾ 𝐷) ∖ I ) =
∅ |
22 | 21 | dmeqi 5773 |
. . . . . 6
⊢ dom (( I
↾ 𝐷) ∖ I ) =
dom ∅ |
23 | | dm0 5789 |
. . . . . 6
⊢ dom
∅ = ∅ |
24 | 22, 23 | eqtri 2765 |
. . . . 5
⊢ dom (( I
↾ 𝐷) ∖ I ) =
∅ |
25 | | 0ss 4311 |
. . . . 5
⊢ ∅
⊆ 𝑋 |
26 | 24, 25 | eqsstri 3935 |
. . . 4
⊢ dom (( I
↾ 𝐷) ∖ I )
⊆ 𝑋 |
27 | 18, 26 | eqsstrrdi 3956 |
. . 3
⊢ (𝐷 ∈ 𝑉 → dom ((0g‘𝐺) ∖ I ) ⊆ 𝑋) |
28 | 10, 15, 27 | elrabd 3604 |
. 2
⊢ (𝐷 ∈ 𝑉 → (0g‘𝐺) ∈ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ⊆ 𝑋}) |
29 | | biid 264 |
. . 3
⊢ (𝐷 ∈ 𝑉 ↔ 𝐷 ∈ 𝑉) |
30 | | difeq1 4030 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑥 ∖ I ) = (𝑦 ∖ I )) |
31 | 30 | dmeqd 5774 |
. . . . 5
⊢ (𝑥 = 𝑦 → dom (𝑥 ∖ I ) = dom (𝑦 ∖ I )) |
32 | 31 | sseq1d 3932 |
. . . 4
⊢ (𝑥 = 𝑦 → (dom (𝑥 ∖ I ) ⊆ 𝑋 ↔ dom (𝑦 ∖ I ) ⊆ 𝑋)) |
33 | 32 | elrab 3602 |
. . 3
⊢ (𝑦 ∈ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ⊆ 𝑋} ↔ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋)) |
34 | | difeq1 4030 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (𝑥 ∖ I ) = (𝑧 ∖ I )) |
35 | 34 | dmeqd 5774 |
. . . . 5
⊢ (𝑥 = 𝑧 → dom (𝑥 ∖ I ) = dom (𝑧 ∖ I )) |
36 | 35 | sseq1d 3932 |
. . . 4
⊢ (𝑥 = 𝑧 → (dom (𝑥 ∖ I ) ⊆ 𝑋 ↔ dom (𝑧 ∖ I ) ⊆ 𝑋)) |
37 | 36 | elrab 3602 |
. . 3
⊢ (𝑧 ∈ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ⊆ 𝑋} ↔ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ⊆ 𝑋)) |
38 | | difeq1 4030 |
. . . . . 6
⊢ (𝑥 = (𝑦(+g‘𝐺)𝑧) → (𝑥 ∖ I ) = ((𝑦(+g‘𝐺)𝑧) ∖ I )) |
39 | 38 | dmeqd 5774 |
. . . . 5
⊢ (𝑥 = (𝑦(+g‘𝐺)𝑧) → dom (𝑥 ∖ I ) = dom ((𝑦(+g‘𝐺)𝑧) ∖ I )) |
40 | 39 | sseq1d 3932 |
. . . 4
⊢ (𝑥 = (𝑦(+g‘𝐺)𝑧) → (dom (𝑥 ∖ I ) ⊆ 𝑋 ↔ dom ((𝑦(+g‘𝐺)𝑧) ∖ I ) ⊆ 𝑋)) |
41 | 12 | 3ad2ant1 1135 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ⊆ 𝑋)) → 𝐺 ∈ Grp) |
42 | | simp2l 1201 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ⊆ 𝑋)) → 𝑦 ∈ 𝐵) |
43 | | simp3l 1203 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ⊆ 𝑋)) → 𝑧 ∈ 𝐵) |
44 | | eqid 2737 |
. . . . . 6
⊢
(+g‘𝐺) = (+g‘𝐺) |
45 | 5, 44 | grpcl 18373 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝑦(+g‘𝐺)𝑧) ∈ 𝐵) |
46 | 41, 42, 43, 45 | syl3anc 1373 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ⊆ 𝑋)) → (𝑦(+g‘𝐺)𝑧) ∈ 𝐵) |
47 | 11, 5, 44 | symgov 18776 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝑦(+g‘𝐺)𝑧) = (𝑦 ∘ 𝑧)) |
48 | 42, 43, 47 | syl2anc 587 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ⊆ 𝑋)) → (𝑦(+g‘𝐺)𝑧) = (𝑦 ∘ 𝑧)) |
49 | 48 | difeq1d 4036 |
. . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ⊆ 𝑋)) → ((𝑦(+g‘𝐺)𝑧) ∖ I ) = ((𝑦 ∘ 𝑧) ∖ I )) |
50 | 49 | dmeqd 5774 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ⊆ 𝑋)) → dom ((𝑦(+g‘𝐺)𝑧) ∖ I ) = dom ((𝑦 ∘ 𝑧) ∖ I )) |
51 | | mvdco 18837 |
. . . . . 6
⊢ dom
((𝑦 ∘ 𝑧) ∖ I ) ⊆ (dom
(𝑦 ∖ I ) ∪ dom
(𝑧 ∖ I
)) |
52 | | simp2r 1202 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ⊆ 𝑋)) → dom (𝑦 ∖ I ) ⊆ 𝑋) |
53 | | simp3r 1204 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ⊆ 𝑋)) → dom (𝑧 ∖ I ) ⊆ 𝑋) |
54 | 52, 53 | unssd 4100 |
. . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ⊆ 𝑋)) → (dom (𝑦 ∖ I ) ∪ dom (𝑧 ∖ I )) ⊆ 𝑋) |
55 | 51, 54 | sstrid 3912 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ⊆ 𝑋)) → dom ((𝑦 ∘ 𝑧) ∖ I ) ⊆ 𝑋) |
56 | 50, 55 | eqsstrd 3939 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ⊆ 𝑋)) → dom ((𝑦(+g‘𝐺)𝑧) ∖ I ) ⊆ 𝑋) |
57 | 40, 46, 56 | elrabd 3604 |
. . 3
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ⊆ 𝑋)) → (𝑦(+g‘𝐺)𝑧) ∈ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ⊆ 𝑋}) |
58 | 29, 33, 37, 57 | syl3anb 1163 |
. 2
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ⊆ 𝑋} ∧ 𝑧 ∈ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ⊆ 𝑋}) → (𝑦(+g‘𝐺)𝑧) ∈ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ⊆ 𝑋}) |
59 | | difeq1 4030 |
. . . . . 6
⊢ (𝑥 = ((invg‘𝐺)‘𝑦) → (𝑥 ∖ I ) = (((invg‘𝐺)‘𝑦) ∖ I )) |
60 | 59 | dmeqd 5774 |
. . . . 5
⊢ (𝑥 = ((invg‘𝐺)‘𝑦) → dom (𝑥 ∖ I ) = dom
(((invg‘𝐺)‘𝑦) ∖ I )) |
61 | 60 | sseq1d 3932 |
. . . 4
⊢ (𝑥 = ((invg‘𝐺)‘𝑦) → (dom (𝑥 ∖ I ) ⊆ 𝑋 ↔ dom (((invg‘𝐺)‘𝑦) ∖ I ) ⊆ 𝑋)) |
62 | | simprl 771 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋)) → 𝑦 ∈ 𝐵) |
63 | | eqid 2737 |
. . . . . 6
⊢
(invg‘𝐺) = (invg‘𝐺) |
64 | 5, 63 | grpinvcl 18415 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ 𝐵) → ((invg‘𝐺)‘𝑦) ∈ 𝐵) |
65 | 12, 62, 64 | syl2an2r 685 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋)) → ((invg‘𝐺)‘𝑦) ∈ 𝐵) |
66 | 11, 5, 63 | symginv 18794 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐵 → ((invg‘𝐺)‘𝑦) = ◡𝑦) |
67 | 66 | ad2antrl 728 |
. . . . . . . 8
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋)) → ((invg‘𝐺)‘𝑦) = ◡𝑦) |
68 | 67 | difeq1d 4036 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋)) → (((invg‘𝐺)‘𝑦) ∖ I ) = (◡𝑦 ∖ I )) |
69 | 68 | dmeqd 5774 |
. . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋)) → dom (((invg‘𝐺)‘𝑦) ∖ I ) = dom (◡𝑦 ∖ I )) |
70 | 11, 5 | symgbasf1o 18767 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐵 → 𝑦:𝐷–1-1-onto→𝐷) |
71 | 70 | ad2antrl 728 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋)) → 𝑦:𝐷–1-1-onto→𝐷) |
72 | | f1omvdcnv 18836 |
. . . . . . 7
⊢ (𝑦:𝐷–1-1-onto→𝐷 → dom (◡𝑦 ∖ I ) = dom (𝑦 ∖ I )) |
73 | 71, 72 | syl 17 |
. . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋)) → dom (◡𝑦 ∖ I ) = dom (𝑦 ∖ I )) |
74 | 69, 73 | eqtrd 2777 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋)) → dom (((invg‘𝐺)‘𝑦) ∖ I ) = dom (𝑦 ∖ I )) |
75 | | simprr 773 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋)) → dom (𝑦 ∖ I ) ⊆ 𝑋) |
76 | 74, 75 | eqsstrd 3939 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋)) → dom (((invg‘𝐺)‘𝑦) ∖ I ) ⊆ 𝑋) |
77 | 61, 65, 76 | elrabd 3604 |
. . 3
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋)) → ((invg‘𝐺)‘𝑦) ∈ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ⊆ 𝑋}) |
78 | 33, 77 | sylan2b 597 |
. 2
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ⊆ 𝑋}) → ((invg‘𝐺)‘𝑦) ∈ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ⊆ 𝑋}) |
79 | 1, 2, 3, 7, 28, 58, 78, 12 | issubgrpd2 18559 |
1
⊢ (𝐷 ∈ 𝑉 → {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ⊆ 𝑋} ∈ (SubGrp‘𝐺)) |