Step | Hyp | Ref
| Expression |
1 | | eqidd 2623 |
. 2
⊢ (𝐷 ∈ 𝑉 → (𝐺 ↾s {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ⊆ 𝑋}) = (𝐺 ↾s {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ⊆ 𝑋})) |
2 | | eqidd 2623 |
. 2
⊢ (𝐷 ∈ 𝑉 → (0g‘𝐺) = (0g‘𝐺)) |
3 | | eqidd 2623 |
. 2
⊢ (𝐷 ∈ 𝑉 → (+g‘𝐺) = (+g‘𝐺)) |
4 | | ssrab2 3687 |
. . . 4
⊢ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ⊆ 𝑋} ⊆ 𝐵 |
5 | | symgsssg.b |
. . . 4
⊢ 𝐵 = (Base‘𝐺) |
6 | 4, 5 | sseqtri 3637 |
. . 3
⊢ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ⊆ 𝑋} ⊆ (Base‘𝐺) |
7 | 6 | a1i 11 |
. 2
⊢ (𝐷 ∈ 𝑉 → {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ⊆ 𝑋} ⊆ (Base‘𝐺)) |
8 | | symgsssg.g |
. . . . 5
⊢ 𝐺 = (SymGrp‘𝐷) |
9 | 8 | symggrp 17820 |
. . . 4
⊢ (𝐷 ∈ 𝑉 → 𝐺 ∈ Grp) |
10 | | eqid 2622 |
. . . . 5
⊢
(0g‘𝐺) = (0g‘𝐺) |
11 | 5, 10 | grpidcl 17450 |
. . . 4
⊢ (𝐺 ∈ Grp →
(0g‘𝐺)
∈ 𝐵) |
12 | 9, 11 | syl 17 |
. . 3
⊢ (𝐷 ∈ 𝑉 → (0g‘𝐺) ∈ 𝐵) |
13 | 8 | symgid 17821 |
. . . . . 6
⊢ (𝐷 ∈ 𝑉 → ( I ↾ 𝐷) = (0g‘𝐺)) |
14 | 13 | difeq1d 3727 |
. . . . 5
⊢ (𝐷 ∈ 𝑉 → (( I ↾ 𝐷) ∖ I ) = ((0g‘𝐺) ∖ I )) |
15 | 14 | dmeqd 5326 |
. . . 4
⊢ (𝐷 ∈ 𝑉 → dom (( I ↾ 𝐷) ∖ I ) = dom
((0g‘𝐺)
∖ I )) |
16 | | resss 5422 |
. . . . . . . 8
⊢ ( I
↾ 𝐷) ⊆
I |
17 | | ssdif0 3942 |
. . . . . . . 8
⊢ (( I
↾ 𝐷) ⊆ I ↔
(( I ↾ 𝐷) ∖ I )
= ∅) |
18 | 16, 17 | mpbi 220 |
. . . . . . 7
⊢ (( I
↾ 𝐷) ∖ I ) =
∅ |
19 | 18 | dmeqi 5325 |
. . . . . 6
⊢ dom (( I
↾ 𝐷) ∖ I ) =
dom ∅ |
20 | | dm0 5339 |
. . . . . 6
⊢ dom
∅ = ∅ |
21 | 19, 20 | eqtri 2644 |
. . . . 5
⊢ dom (( I
↾ 𝐷) ∖ I ) =
∅ |
22 | | 0ss 3972 |
. . . . 5
⊢ ∅
⊆ 𝑋 |
23 | 21, 22 | eqsstri 3635 |
. . . 4
⊢ dom (( I
↾ 𝐷) ∖ I )
⊆ 𝑋 |
24 | 15, 23 | syl6eqssr 3656 |
. . 3
⊢ (𝐷 ∈ 𝑉 → dom ((0g‘𝐺) ∖ I ) ⊆ 𝑋) |
25 | | difeq1 3721 |
. . . . . 6
⊢ (𝑥 = (0g‘𝐺) → (𝑥 ∖ I ) = ((0g‘𝐺) ∖ I )) |
26 | 25 | dmeqd 5326 |
. . . . 5
⊢ (𝑥 = (0g‘𝐺) → dom (𝑥 ∖ I ) = dom
((0g‘𝐺)
∖ I )) |
27 | 26 | sseq1d 3632 |
. . . 4
⊢ (𝑥 = (0g‘𝐺) → (dom (𝑥 ∖ I ) ⊆ 𝑋 ↔ dom
((0g‘𝐺)
∖ I ) ⊆ 𝑋)) |
28 | 27 | elrab 3363 |
. . 3
⊢
((0g‘𝐺) ∈ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ⊆ 𝑋} ↔ ((0g‘𝐺) ∈ 𝐵 ∧ dom ((0g‘𝐺) ∖ I ) ⊆ 𝑋)) |
29 | 12, 24, 28 | sylanbrc 698 |
. 2
⊢ (𝐷 ∈ 𝑉 → (0g‘𝐺) ∈ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ⊆ 𝑋}) |
30 | | biid 251 |
. . 3
⊢ (𝐷 ∈ 𝑉 ↔ 𝐷 ∈ 𝑉) |
31 | | difeq1 3721 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑥 ∖ I ) = (𝑦 ∖ I )) |
32 | 31 | dmeqd 5326 |
. . . . 5
⊢ (𝑥 = 𝑦 → dom (𝑥 ∖ I ) = dom (𝑦 ∖ I )) |
33 | 32 | sseq1d 3632 |
. . . 4
⊢ (𝑥 = 𝑦 → (dom (𝑥 ∖ I ) ⊆ 𝑋 ↔ dom (𝑦 ∖ I ) ⊆ 𝑋)) |
34 | 33 | elrab 3363 |
. . 3
⊢ (𝑦 ∈ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ⊆ 𝑋} ↔ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋)) |
35 | | difeq1 3721 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (𝑥 ∖ I ) = (𝑧 ∖ I )) |
36 | 35 | dmeqd 5326 |
. . . . 5
⊢ (𝑥 = 𝑧 → dom (𝑥 ∖ I ) = dom (𝑧 ∖ I )) |
37 | 36 | sseq1d 3632 |
. . . 4
⊢ (𝑥 = 𝑧 → (dom (𝑥 ∖ I ) ⊆ 𝑋 ↔ dom (𝑧 ∖ I ) ⊆ 𝑋)) |
38 | 37 | elrab 3363 |
. . 3
⊢ (𝑧 ∈ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ⊆ 𝑋} ↔ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ⊆ 𝑋)) |
39 | 9 | 3ad2ant1 1082 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ⊆ 𝑋)) → 𝐺 ∈ Grp) |
40 | | simp2l 1087 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ⊆ 𝑋)) → 𝑦 ∈ 𝐵) |
41 | | simp3l 1089 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ⊆ 𝑋)) → 𝑧 ∈ 𝐵) |
42 | | eqid 2622 |
. . . . . 6
⊢
(+g‘𝐺) = (+g‘𝐺) |
43 | 5, 42 | grpcl 17430 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝑦(+g‘𝐺)𝑧) ∈ 𝐵) |
44 | 39, 40, 41, 43 | syl3anc 1326 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ⊆ 𝑋)) → (𝑦(+g‘𝐺)𝑧) ∈ 𝐵) |
45 | 8, 5, 42 | symgov 17810 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝑦(+g‘𝐺)𝑧) = (𝑦 ∘ 𝑧)) |
46 | 40, 41, 45 | syl2anc 693 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ⊆ 𝑋)) → (𝑦(+g‘𝐺)𝑧) = (𝑦 ∘ 𝑧)) |
47 | 46 | difeq1d 3727 |
. . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ⊆ 𝑋)) → ((𝑦(+g‘𝐺)𝑧) ∖ I ) = ((𝑦 ∘ 𝑧) ∖ I )) |
48 | 47 | dmeqd 5326 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ⊆ 𝑋)) → dom ((𝑦(+g‘𝐺)𝑧) ∖ I ) = dom ((𝑦 ∘ 𝑧) ∖ I )) |
49 | | mvdco 17865 |
. . . . . 6
⊢ dom
((𝑦 ∘ 𝑧) ∖ I ) ⊆ (dom
(𝑦 ∖ I ) ∪ dom
(𝑧 ∖ I
)) |
50 | | simp2r 1088 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ⊆ 𝑋)) → dom (𝑦 ∖ I ) ⊆ 𝑋) |
51 | | simp3r 1090 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ⊆ 𝑋)) → dom (𝑧 ∖ I ) ⊆ 𝑋) |
52 | 50, 51 | unssd 3789 |
. . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ⊆ 𝑋)) → (dom (𝑦 ∖ I ) ∪ dom (𝑧 ∖ I )) ⊆ 𝑋) |
53 | 49, 52 | syl5ss 3614 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ⊆ 𝑋)) → dom ((𝑦 ∘ 𝑧) ∖ I ) ⊆ 𝑋) |
54 | 48, 53 | eqsstrd 3639 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ⊆ 𝑋)) → dom ((𝑦(+g‘𝐺)𝑧) ∖ I ) ⊆ 𝑋) |
55 | | difeq1 3721 |
. . . . . . 7
⊢ (𝑥 = (𝑦(+g‘𝐺)𝑧) → (𝑥 ∖ I ) = ((𝑦(+g‘𝐺)𝑧) ∖ I )) |
56 | 55 | dmeqd 5326 |
. . . . . 6
⊢ (𝑥 = (𝑦(+g‘𝐺)𝑧) → dom (𝑥 ∖ I ) = dom ((𝑦(+g‘𝐺)𝑧) ∖ I )) |
57 | 56 | sseq1d 3632 |
. . . . 5
⊢ (𝑥 = (𝑦(+g‘𝐺)𝑧) → (dom (𝑥 ∖ I ) ⊆ 𝑋 ↔ dom ((𝑦(+g‘𝐺)𝑧) ∖ I ) ⊆ 𝑋)) |
58 | 57 | elrab 3363 |
. . . 4
⊢ ((𝑦(+g‘𝐺)𝑧) ∈ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ⊆ 𝑋} ↔ ((𝑦(+g‘𝐺)𝑧) ∈ 𝐵 ∧ dom ((𝑦(+g‘𝐺)𝑧) ∖ I ) ⊆ 𝑋)) |
59 | 44, 54, 58 | sylanbrc 698 |
. . 3
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋) ∧ (𝑧 ∈ 𝐵 ∧ dom (𝑧 ∖ I ) ⊆ 𝑋)) → (𝑦(+g‘𝐺)𝑧) ∈ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ⊆ 𝑋}) |
60 | 30, 34, 38, 59 | syl3anb 1369 |
. 2
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ⊆ 𝑋} ∧ 𝑧 ∈ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ⊆ 𝑋}) → (𝑦(+g‘𝐺)𝑧) ∈ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ⊆ 𝑋}) |
61 | 9 | adantr 481 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋)) → 𝐺 ∈ Grp) |
62 | | simprl 794 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋)) → 𝑦 ∈ 𝐵) |
63 | | eqid 2622 |
. . . . . 6
⊢
(invg‘𝐺) = (invg‘𝐺) |
64 | 5, 63 | grpinvcl 17467 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ 𝐵) → ((invg‘𝐺)‘𝑦) ∈ 𝐵) |
65 | 61, 62, 64 | syl2anc 693 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋)) → ((invg‘𝐺)‘𝑦) ∈ 𝐵) |
66 | 8, 5, 63 | symginv 17822 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐵 → ((invg‘𝐺)‘𝑦) = ◡𝑦) |
67 | 66 | ad2antrl 764 |
. . . . . . . 8
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋)) → ((invg‘𝐺)‘𝑦) = ◡𝑦) |
68 | 67 | difeq1d 3727 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋)) → (((invg‘𝐺)‘𝑦) ∖ I ) = (◡𝑦 ∖ I )) |
69 | 68 | dmeqd 5326 |
. . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋)) → dom (((invg‘𝐺)‘𝑦) ∖ I ) = dom (◡𝑦 ∖ I )) |
70 | 8, 5 | symgbasf1o 17803 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐵 → 𝑦:𝐷–1-1-onto→𝐷) |
71 | 70 | ad2antrl 764 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋)) → 𝑦:𝐷–1-1-onto→𝐷) |
72 | | f1omvdcnv 17864 |
. . . . . . 7
⊢ (𝑦:𝐷–1-1-onto→𝐷 → dom (◡𝑦 ∖ I ) = dom (𝑦 ∖ I )) |
73 | 71, 72 | syl 17 |
. . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋)) → dom (◡𝑦 ∖ I ) = dom (𝑦 ∖ I )) |
74 | 69, 73 | eqtrd 2656 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋)) → dom (((invg‘𝐺)‘𝑦) ∖ I ) = dom (𝑦 ∖ I )) |
75 | | simprr 796 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋)) → dom (𝑦 ∖ I ) ⊆ 𝑋) |
76 | 74, 75 | eqsstrd 3639 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋)) → dom (((invg‘𝐺)‘𝑦) ∖ I ) ⊆ 𝑋) |
77 | | difeq1 3721 |
. . . . . . 7
⊢ (𝑥 = ((invg‘𝐺)‘𝑦) → (𝑥 ∖ I ) = (((invg‘𝐺)‘𝑦) ∖ I )) |
78 | 77 | dmeqd 5326 |
. . . . . 6
⊢ (𝑥 = ((invg‘𝐺)‘𝑦) → dom (𝑥 ∖ I ) = dom
(((invg‘𝐺)‘𝑦) ∖ I )) |
79 | 78 | sseq1d 3632 |
. . . . 5
⊢ (𝑥 = ((invg‘𝐺)‘𝑦) → (dom (𝑥 ∖ I ) ⊆ 𝑋 ↔ dom (((invg‘𝐺)‘𝑦) ∖ I ) ⊆ 𝑋)) |
80 | 79 | elrab 3363 |
. . . 4
⊢
(((invg‘𝐺)‘𝑦) ∈ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ⊆ 𝑋} ↔ (((invg‘𝐺)‘𝑦) ∈ 𝐵 ∧ dom (((invg‘𝐺)‘𝑦) ∖ I ) ⊆ 𝑋)) |
81 | 65, 76, 80 | sylanbrc 698 |
. . 3
⊢ ((𝐷 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ dom (𝑦 ∖ I ) ⊆ 𝑋)) → ((invg‘𝐺)‘𝑦) ∈ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ⊆ 𝑋}) |
82 | 34, 81 | sylan2b 492 |
. 2
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑦 ∈ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ⊆ 𝑋}) → ((invg‘𝐺)‘𝑦) ∈ {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ⊆ 𝑋}) |
83 | 1, 2, 3, 7, 29, 60, 82, 9 | issubgrpd2 17610 |
1
⊢ (𝐷 ∈ 𝑉 → {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ⊆ 𝑋} ∈ (SubGrp‘𝐺)) |