Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . 3
⊢
(Cntz‘𝐺) =
(Cntz‘𝐺) |
2 | | eqid 2738 |
. . 3
⊢
(0g‘𝐺) = (0g‘𝐺) |
3 | | eqid 2738 |
. . 3
⊢
(mrCls‘(SubGrp‘𝐺)) = (mrCls‘(SubGrp‘𝐺)) |
4 | | subgrcl 18402 |
. . . 4
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) |
5 | 4 | adantl 485 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝐺 ∈ Grp) |
6 | | snex 5298 |
. . . 4
⊢ {𝐴} ∈ V |
7 | 6 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) → {𝐴} ∈ V) |
8 | | f1osng 6658 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) → {〈𝐴, 𝑆〉}:{𝐴}–1-1-onto→{𝑆}) |
9 | | f1of 6618 |
. . . . 5
⊢
({〈𝐴, 𝑆〉}:{𝐴}–1-1-onto→{𝑆} → {〈𝐴, 𝑆〉}:{𝐴}⟶{𝑆}) |
10 | 8, 9 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) → {〈𝐴, 𝑆〉}:{𝐴}⟶{𝑆}) |
11 | | simpr 488 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝑆 ∈ (SubGrp‘𝐺)) |
12 | 11 | snssd 4697 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) → {𝑆} ⊆ (SubGrp‘𝐺)) |
13 | 10, 12 | fssd 6522 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) → {〈𝐴, 𝑆〉}:{𝐴}⟶(SubGrp‘𝐺)) |
14 | | simpr1 1195 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ {𝐴} ∧ 𝑦 ∈ {𝐴} ∧ 𝑥 ≠ 𝑦)) → 𝑥 ∈ {𝐴}) |
15 | | elsni 4533 |
. . . . . 6
⊢ (𝑥 ∈ {𝐴} → 𝑥 = 𝐴) |
16 | 14, 15 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ {𝐴} ∧ 𝑦 ∈ {𝐴} ∧ 𝑥 ≠ 𝑦)) → 𝑥 = 𝐴) |
17 | | simpr2 1196 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ {𝐴} ∧ 𝑦 ∈ {𝐴} ∧ 𝑥 ≠ 𝑦)) → 𝑦 ∈ {𝐴}) |
18 | | elsni 4533 |
. . . . . 6
⊢ (𝑦 ∈ {𝐴} → 𝑦 = 𝐴) |
19 | 17, 18 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ {𝐴} ∧ 𝑦 ∈ {𝐴} ∧ 𝑥 ≠ 𝑦)) → 𝑦 = 𝐴) |
20 | 16, 19 | eqtr4d 2776 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ {𝐴} ∧ 𝑦 ∈ {𝐴} ∧ 𝑥 ≠ 𝑦)) → 𝑥 = 𝑦) |
21 | | simpr3 1197 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ {𝐴} ∧ 𝑦 ∈ {𝐴} ∧ 𝑥 ≠ 𝑦)) → 𝑥 ≠ 𝑦) |
22 | 20, 21 | pm2.21ddne 3018 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ {𝐴} ∧ 𝑦 ∈ {𝐴} ∧ 𝑥 ≠ 𝑦)) → ({〈𝐴, 𝑆〉}‘𝑥) ⊆ ((Cntz‘𝐺)‘({〈𝐴, 𝑆〉}‘𝑦))) |
23 | 5 | adantr 484 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → 𝐺 ∈ Grp) |
24 | | eqid 2738 |
. . . . . . . . 9
⊢
(Base‘𝐺) =
(Base‘𝐺) |
25 | 24 | subgacs 18431 |
. . . . . . . 8
⊢ (𝐺 ∈ Grp →
(SubGrp‘𝐺) ∈
(ACS‘(Base‘𝐺))) |
26 | | acsmre 17026 |
. . . . . . . 8
⊢
((SubGrp‘𝐺)
∈ (ACS‘(Base‘𝐺)) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺))) |
27 | 23, 25, 26 | 3syl 18 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺))) |
28 | 15 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → 𝑥 = 𝐴) |
29 | 28 | sneqd 4528 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → {𝑥} = {𝐴}) |
30 | 29 | difeq2d 4013 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → ({𝐴} ∖ {𝑥}) = ({𝐴} ∖ {𝐴})) |
31 | | difid 4259 |
. . . . . . . . . . . . 13
⊢ ({𝐴} ∖ {𝐴}) = ∅ |
32 | 30, 31 | eqtrdi 2789 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → ({𝐴} ∖ {𝑥}) = ∅) |
33 | 32 | imaeq2d 5903 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → ({〈𝐴, 𝑆〉} “ ({𝐴} ∖ {𝑥})) = ({〈𝐴, 𝑆〉} “ ∅)) |
34 | | ima0 5919 |
. . . . . . . . . . 11
⊢
({〈𝐴, 𝑆〉} “ ∅) =
∅ |
35 | 33, 34 | eqtrdi 2789 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → ({〈𝐴, 𝑆〉} “ ({𝐴} ∖ {𝑥})) = ∅) |
36 | 35 | unieqd 4810 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → ∪
({〈𝐴, 𝑆〉} “ ({𝐴} ∖ {𝑥})) = ∪
∅) |
37 | | uni0 4826 |
. . . . . . . . 9
⊢ ∪ ∅ = ∅ |
38 | 36, 37 | eqtrdi 2789 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → ∪
({〈𝐴, 𝑆〉} “ ({𝐴} ∖ {𝑥})) = ∅) |
39 | | 0ss 4285 |
. . . . . . . . 9
⊢ ∅
⊆ {(0g‘𝐺)} |
40 | 39 | a1i 11 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → ∅ ⊆
{(0g‘𝐺)}) |
41 | 38, 40 | eqsstrd 3915 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → ∪
({〈𝐴, 𝑆〉} “ ({𝐴} ∖ {𝑥})) ⊆ {(0g‘𝐺)}) |
42 | 2 | 0subg 18422 |
. . . . . . . 8
⊢ (𝐺 ∈ Grp →
{(0g‘𝐺)}
∈ (SubGrp‘𝐺)) |
43 | 23, 42 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → {(0g‘𝐺)} ∈ (SubGrp‘𝐺)) |
44 | 3 | mrcsscl 16994 |
. . . . . . 7
⊢
(((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) ∧ ∪
({〈𝐴, 𝑆〉} “ ({𝐴} ∖ {𝑥})) ⊆ {(0g‘𝐺)} ∧
{(0g‘𝐺)}
∈ (SubGrp‘𝐺))
→ ((mrCls‘(SubGrp‘𝐺))‘∪
({〈𝐴, 𝑆〉} “ ({𝐴} ∖ {𝑥}))) ⊆ {(0g‘𝐺)}) |
45 | 27, 41, 43, 44 | syl3anc 1372 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → ((mrCls‘(SubGrp‘𝐺))‘∪ ({〈𝐴, 𝑆〉} “ ({𝐴} ∖ {𝑥}))) ⊆ {(0g‘𝐺)}) |
46 | 2 | subg0cl 18405 |
. . . . . . . . 9
⊢ (𝑆 ∈ (SubGrp‘𝐺) →
(0g‘𝐺)
∈ 𝑆) |
47 | 46 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → (0g‘𝐺) ∈ 𝑆) |
48 | 15 | fveq2d 6678 |
. . . . . . . . 9
⊢ (𝑥 ∈ {𝐴} → ({〈𝐴, 𝑆〉}‘𝑥) = ({〈𝐴, 𝑆〉}‘𝐴)) |
49 | | fvsng 6952 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ({〈𝐴, 𝑆〉}‘𝐴) = 𝑆) |
50 | 48, 49 | sylan9eqr 2795 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → ({〈𝐴, 𝑆〉}‘𝑥) = 𝑆) |
51 | 47, 50 | eleqtrrd 2836 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → (0g‘𝐺) ∈ ({〈𝐴, 𝑆〉}‘𝑥)) |
52 | 51 | snssd 4697 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → {(0g‘𝐺)} ⊆ ({〈𝐴, 𝑆〉}‘𝑥)) |
53 | 45, 52 | sstrd 3887 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → ((mrCls‘(SubGrp‘𝐺))‘∪ ({〈𝐴, 𝑆〉} “ ({𝐴} ∖ {𝑥}))) ⊆ ({〈𝐴, 𝑆〉}‘𝑥)) |
54 | | sseqin2 4106 |
. . . . 5
⊢
(((mrCls‘(SubGrp‘𝐺))‘∪
({〈𝐴, 𝑆〉} “ ({𝐴} ∖ {𝑥}))) ⊆ ({〈𝐴, 𝑆〉}‘𝑥) ↔ (({〈𝐴, 𝑆〉}‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ ({〈𝐴, 𝑆〉} “ ({𝐴} ∖ {𝑥})))) = ((mrCls‘(SubGrp‘𝐺))‘∪ ({〈𝐴, 𝑆〉} “ ({𝐴} ∖ {𝑥})))) |
55 | 53, 54 | sylib 221 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → (({〈𝐴, 𝑆〉}‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ ({〈𝐴, 𝑆〉} “ ({𝐴} ∖ {𝑥})))) = ((mrCls‘(SubGrp‘𝐺))‘∪ ({〈𝐴, 𝑆〉} “ ({𝐴} ∖ {𝑥})))) |
56 | 55, 45 | eqsstrd 3915 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ {𝐴}) → (({〈𝐴, 𝑆〉}‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ ({〈𝐴, 𝑆〉} “ ({𝐴} ∖ {𝑥})))) ⊆ {(0g‘𝐺)}) |
57 | 1, 2, 3, 5, 7, 13,
22, 56 | dmdprdd 19240 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝐺dom DProd {〈𝐴, 𝑆〉}) |
58 | 3 | dprdspan 19268 |
. . . 4
⊢ (𝐺dom DProd {〈𝐴, 𝑆〉} → (𝐺 DProd {〈𝐴, 𝑆〉}) = ((mrCls‘(SubGrp‘𝐺))‘∪ ran {〈𝐴, 𝑆〉})) |
59 | 57, 58 | syl 17 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (𝐺 DProd {〈𝐴, 𝑆〉}) = ((mrCls‘(SubGrp‘𝐺))‘∪ ran {〈𝐴, 𝑆〉})) |
60 | | rnsnopg 6053 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → ran {〈𝐴, 𝑆〉} = {𝑆}) |
61 | 60 | adantr 484 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ran {〈𝐴, 𝑆〉} = {𝑆}) |
62 | 61 | unieqd 4810 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ∪ ran
{〈𝐴, 𝑆〉} = ∪
{𝑆}) |
63 | | unisng 4817 |
. . . . . . 7
⊢ (𝑆 ∈ (SubGrp‘𝐺) → ∪ {𝑆}
= 𝑆) |
64 | 63 | adantl 485 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ∪
{𝑆} = 𝑆) |
65 | 62, 64 | eqtrd 2773 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ∪ ran
{〈𝐴, 𝑆〉} = 𝑆) |
66 | 65 | fveq2d 6678 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ((mrCls‘(SubGrp‘𝐺))‘∪ ran {〈𝐴, 𝑆〉}) = ((mrCls‘(SubGrp‘𝐺))‘𝑆)) |
67 | 5, 25, 26 | 3syl 18 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺))) |
68 | 3 | mrcid 16987 |
. . . . 5
⊢
(((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ((mrCls‘(SubGrp‘𝐺))‘𝑆) = 𝑆) |
69 | 67, 68 | sylancom 591 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ((mrCls‘(SubGrp‘𝐺))‘𝑆) = 𝑆) |
70 | 66, 69 | eqtrd 2773 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ((mrCls‘(SubGrp‘𝐺))‘∪ ran {〈𝐴, 𝑆〉}) = 𝑆) |
71 | 59, 70 | eqtrd 2773 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (𝐺 DProd {〈𝐴, 𝑆〉}) = 𝑆) |
72 | 57, 71 | jca 515 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (𝐺dom DProd {〈𝐴, 𝑆〉} ∧ (𝐺 DProd {〈𝐴, 𝑆〉}) = 𝑆)) |