# Metamath Proof Explorer

## Theorem dprdsn

Description: A singleton family is an internal direct product, the product of which is the given subgroup. (Contributed by Mario Carneiro, 25-Apr-2016)

Ref Expression
Assertion dprdsn ${⊢}\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\to \left({G}\mathrm{dom}\mathrm{DProd}\left\{⟨{A},{S}⟩\right\}\wedge {G}\mathrm{DProd}\left\{⟨{A},{S}⟩\right\}={S}\right)$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}\mathrm{Cntz}\left({G}\right)=\mathrm{Cntz}\left({G}\right)$
2 eqid ${⊢}{0}_{{G}}={0}_{{G}}$
3 eqid ${⊢}\mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)=\mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)$
4 subgrcl ${⊢}{S}\in \mathrm{SubGrp}\left({G}\right)\to {G}\in \mathrm{Grp}$
5 4 adantl ${⊢}\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\to {G}\in \mathrm{Grp}$
6 snex ${⊢}\left\{{A}\right\}\in \mathrm{V}$
7 6 a1i ${⊢}\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\to \left\{{A}\right\}\in \mathrm{V}$
8 f1osng ${⊢}\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\to \left\{⟨{A},{S}⟩\right\}:\left\{{A}\right\}\underset{1-1 onto}{⟶}\left\{{S}\right\}$
9 f1of ${⊢}\left\{⟨{A},{S}⟩\right\}:\left\{{A}\right\}\underset{1-1 onto}{⟶}\left\{{S}\right\}\to \left\{⟨{A},{S}⟩\right\}:\left\{{A}\right\}⟶\left\{{S}\right\}$
10 8 9 syl ${⊢}\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\to \left\{⟨{A},{S}⟩\right\}:\left\{{A}\right\}⟶\left\{{S}\right\}$
11 simpr ${⊢}\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\to {S}\in \mathrm{SubGrp}\left({G}\right)$
12 11 snssd ${⊢}\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\to \left\{{S}\right\}\subseteq \mathrm{SubGrp}\left({G}\right)$
13 10 12 fssd ${⊢}\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\to \left\{⟨{A},{S}⟩\right\}:\left\{{A}\right\}⟶\mathrm{SubGrp}\left({G}\right)$
14 simpr1 ${⊢}\left(\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge \left({x}\in \left\{{A}\right\}\wedge {y}\in \left\{{A}\right\}\wedge {x}\ne {y}\right)\right)\to {x}\in \left\{{A}\right\}$
15 elsni ${⊢}{x}\in \left\{{A}\right\}\to {x}={A}$
16 14 15 syl ${⊢}\left(\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge \left({x}\in \left\{{A}\right\}\wedge {y}\in \left\{{A}\right\}\wedge {x}\ne {y}\right)\right)\to {x}={A}$
17 simpr2 ${⊢}\left(\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge \left({x}\in \left\{{A}\right\}\wedge {y}\in \left\{{A}\right\}\wedge {x}\ne {y}\right)\right)\to {y}\in \left\{{A}\right\}$
18 elsni ${⊢}{y}\in \left\{{A}\right\}\to {y}={A}$
19 17 18 syl ${⊢}\left(\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge \left({x}\in \left\{{A}\right\}\wedge {y}\in \left\{{A}\right\}\wedge {x}\ne {y}\right)\right)\to {y}={A}$
20 16 19 eqtr4d ${⊢}\left(\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge \left({x}\in \left\{{A}\right\}\wedge {y}\in \left\{{A}\right\}\wedge {x}\ne {y}\right)\right)\to {x}={y}$
21 simpr3 ${⊢}\left(\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge \left({x}\in \left\{{A}\right\}\wedge {y}\in \left\{{A}\right\}\wedge {x}\ne {y}\right)\right)\to {x}\ne {y}$
22 20 21 pm2.21ddne ${⊢}\left(\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge \left({x}\in \left\{{A}\right\}\wedge {y}\in \left\{{A}\right\}\wedge {x}\ne {y}\right)\right)\to \left\{⟨{A},{S}⟩\right\}\left({x}\right)\subseteq \mathrm{Cntz}\left({G}\right)\left(\left\{⟨{A},{S}⟩\right\}\left({y}\right)\right)$
23 5 adantr ${⊢}\left(\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge {x}\in \left\{{A}\right\}\right)\to {G}\in \mathrm{Grp}$
24 eqid ${⊢}{\mathrm{Base}}_{{G}}={\mathrm{Base}}_{{G}}$
25 24 subgacs ${⊢}{G}\in \mathrm{Grp}\to \mathrm{SubGrp}\left({G}\right)\in \mathrm{ACS}\left({\mathrm{Base}}_{{G}}\right)$
26 acsmre ${⊢}\mathrm{SubGrp}\left({G}\right)\in \mathrm{ACS}\left({\mathrm{Base}}_{{G}}\right)\to \mathrm{SubGrp}\left({G}\right)\in \mathrm{Moore}\left({\mathrm{Base}}_{{G}}\right)$
27 23 25 26 3syl ${⊢}\left(\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge {x}\in \left\{{A}\right\}\right)\to \mathrm{SubGrp}\left({G}\right)\in \mathrm{Moore}\left({\mathrm{Base}}_{{G}}\right)$
28 15 adantl ${⊢}\left(\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge {x}\in \left\{{A}\right\}\right)\to {x}={A}$
29 28 sneqd ${⊢}\left(\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge {x}\in \left\{{A}\right\}\right)\to \left\{{x}\right\}=\left\{{A}\right\}$
30 29 difeq2d ${⊢}\left(\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge {x}\in \left\{{A}\right\}\right)\to \left\{{A}\right\}\setminus \left\{{x}\right\}=\left\{{A}\right\}\setminus \left\{{A}\right\}$
31 difid ${⊢}\left\{{A}\right\}\setminus \left\{{A}\right\}=\varnothing$
32 30 31 syl6eq ${⊢}\left(\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge {x}\in \left\{{A}\right\}\right)\to \left\{{A}\right\}\setminus \left\{{x}\right\}=\varnothing$
33 32 imaeq2d ${⊢}\left(\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge {x}\in \left\{{A}\right\}\right)\to \left\{⟨{A},{S}⟩\right\}\left[\left\{{A}\right\}\setminus \left\{{x}\right\}\right]=\left\{⟨{A},{S}⟩\right\}\left[\varnothing \right]$
34 ima0 ${⊢}\left\{⟨{A},{S}⟩\right\}\left[\varnothing \right]=\varnothing$
35 33 34 syl6eq ${⊢}\left(\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge {x}\in \left\{{A}\right\}\right)\to \left\{⟨{A},{S}⟩\right\}\left[\left\{{A}\right\}\setminus \left\{{x}\right\}\right]=\varnothing$
36 35 unieqd ${⊢}\left(\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge {x}\in \left\{{A}\right\}\right)\to \bigcup \left\{⟨{A},{S}⟩\right\}\left[\left\{{A}\right\}\setminus \left\{{x}\right\}\right]=\bigcup \varnothing$
37 uni0 ${⊢}\bigcup \varnothing =\varnothing$
38 36 37 syl6eq ${⊢}\left(\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge {x}\in \left\{{A}\right\}\right)\to \bigcup \left\{⟨{A},{S}⟩\right\}\left[\left\{{A}\right\}\setminus \left\{{x}\right\}\right]=\varnothing$
39 0ss ${⊢}\varnothing \subseteq \left\{{0}_{{G}}\right\}$
40 39 a1i ${⊢}\left(\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge {x}\in \left\{{A}\right\}\right)\to \varnothing \subseteq \left\{{0}_{{G}}\right\}$
41 38 40 eqsstrd ${⊢}\left(\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge {x}\in \left\{{A}\right\}\right)\to \bigcup \left\{⟨{A},{S}⟩\right\}\left[\left\{{A}\right\}\setminus \left\{{x}\right\}\right]\subseteq \left\{{0}_{{G}}\right\}$
42 2 0subg ${⊢}{G}\in \mathrm{Grp}\to \left\{{0}_{{G}}\right\}\in \mathrm{SubGrp}\left({G}\right)$
43 23 42 syl ${⊢}\left(\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge {x}\in \left\{{A}\right\}\right)\to \left\{{0}_{{G}}\right\}\in \mathrm{SubGrp}\left({G}\right)$
44 3 mrcsscl ${⊢}\left(\mathrm{SubGrp}\left({G}\right)\in \mathrm{Moore}\left({\mathrm{Base}}_{{G}}\right)\wedge \bigcup \left\{⟨{A},{S}⟩\right\}\left[\left\{{A}\right\}\setminus \left\{{x}\right\}\right]\subseteq \left\{{0}_{{G}}\right\}\wedge \left\{{0}_{{G}}\right\}\in \mathrm{SubGrp}\left({G}\right)\right)\to \mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left(\bigcup \left\{⟨{A},{S}⟩\right\}\left[\left\{{A}\right\}\setminus \left\{{x}\right\}\right]\right)\subseteq \left\{{0}_{{G}}\right\}$
45 27 41 43 44 syl3anc ${⊢}\left(\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge {x}\in \left\{{A}\right\}\right)\to \mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left(\bigcup \left\{⟨{A},{S}⟩\right\}\left[\left\{{A}\right\}\setminus \left\{{x}\right\}\right]\right)\subseteq \left\{{0}_{{G}}\right\}$
46 2 subg0cl ${⊢}{S}\in \mathrm{SubGrp}\left({G}\right)\to {0}_{{G}}\in {S}$
47 46 ad2antlr ${⊢}\left(\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge {x}\in \left\{{A}\right\}\right)\to {0}_{{G}}\in {S}$
48 15 fveq2d ${⊢}{x}\in \left\{{A}\right\}\to \left\{⟨{A},{S}⟩\right\}\left({x}\right)=\left\{⟨{A},{S}⟩\right\}\left({A}\right)$
49 fvsng ${⊢}\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\to \left\{⟨{A},{S}⟩\right\}\left({A}\right)={S}$
50 48 49 sylan9eqr ${⊢}\left(\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge {x}\in \left\{{A}\right\}\right)\to \left\{⟨{A},{S}⟩\right\}\left({x}\right)={S}$
51 47 50 eleqtrrd ${⊢}\left(\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge {x}\in \left\{{A}\right\}\right)\to {0}_{{G}}\in \left\{⟨{A},{S}⟩\right\}\left({x}\right)$
52 51 snssd ${⊢}\left(\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge {x}\in \left\{{A}\right\}\right)\to \left\{{0}_{{G}}\right\}\subseteq \left\{⟨{A},{S}⟩\right\}\left({x}\right)$
53 45 52 sstrd ${⊢}\left(\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge {x}\in \left\{{A}\right\}\right)\to \mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left(\bigcup \left\{⟨{A},{S}⟩\right\}\left[\left\{{A}\right\}\setminus \left\{{x}\right\}\right]\right)\subseteq \left\{⟨{A},{S}⟩\right\}\left({x}\right)$
54 sseqin2 ${⊢}\mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left(\bigcup \left\{⟨{A},{S}⟩\right\}\left[\left\{{A}\right\}\setminus \left\{{x}\right\}\right]\right)\subseteq \left\{⟨{A},{S}⟩\right\}\left({x}\right)↔\left\{⟨{A},{S}⟩\right\}\left({x}\right)\cap \mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left(\bigcup \left\{⟨{A},{S}⟩\right\}\left[\left\{{A}\right\}\setminus \left\{{x}\right\}\right]\right)=\mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left(\bigcup \left\{⟨{A},{S}⟩\right\}\left[\left\{{A}\right\}\setminus \left\{{x}\right\}\right]\right)$
55 53 54 sylib ${⊢}\left(\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge {x}\in \left\{{A}\right\}\right)\to \left\{⟨{A},{S}⟩\right\}\left({x}\right)\cap \mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left(\bigcup \left\{⟨{A},{S}⟩\right\}\left[\left\{{A}\right\}\setminus \left\{{x}\right\}\right]\right)=\mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left(\bigcup \left\{⟨{A},{S}⟩\right\}\left[\left\{{A}\right\}\setminus \left\{{x}\right\}\right]\right)$
56 55 45 eqsstrd ${⊢}\left(\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\wedge {x}\in \left\{{A}\right\}\right)\to \left\{⟨{A},{S}⟩\right\}\left({x}\right)\cap \mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left(\bigcup \left\{⟨{A},{S}⟩\right\}\left[\left\{{A}\right\}\setminus \left\{{x}\right\}\right]\right)\subseteq \left\{{0}_{{G}}\right\}$
57 1 2 3 5 7 13 22 56 dmdprdd ${⊢}\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\to {G}\mathrm{dom}\mathrm{DProd}\left\{⟨{A},{S}⟩\right\}$
58 3 dprdspan ${⊢}{G}\mathrm{dom}\mathrm{DProd}\left\{⟨{A},{S}⟩\right\}\to {G}\mathrm{DProd}\left\{⟨{A},{S}⟩\right\}=\mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left(\bigcup \mathrm{ran}\left\{⟨{A},{S}⟩\right\}\right)$
59 57 58 syl ${⊢}\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\to {G}\mathrm{DProd}\left\{⟨{A},{S}⟩\right\}=\mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left(\bigcup \mathrm{ran}\left\{⟨{A},{S}⟩\right\}\right)$
60 rnsnopg ${⊢}{A}\in {V}\to \mathrm{ran}\left\{⟨{A},{S}⟩\right\}=\left\{{S}\right\}$
61 60 adantr ${⊢}\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\to \mathrm{ran}\left\{⟨{A},{S}⟩\right\}=\left\{{S}\right\}$
62 61 unieqd ${⊢}\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\to \bigcup \mathrm{ran}\left\{⟨{A},{S}⟩\right\}=\bigcup \left\{{S}\right\}$
63 unisng ${⊢}{S}\in \mathrm{SubGrp}\left({G}\right)\to \bigcup \left\{{S}\right\}={S}$
64 63 adantl ${⊢}\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\to \bigcup \left\{{S}\right\}={S}$
65 62 64 eqtrd ${⊢}\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\to \bigcup \mathrm{ran}\left\{⟨{A},{S}⟩\right\}={S}$
66 65 fveq2d ${⊢}\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\to \mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left(\bigcup \mathrm{ran}\left\{⟨{A},{S}⟩\right\}\right)=\mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left({S}\right)$
67 5 25 26 3syl ${⊢}\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\to \mathrm{SubGrp}\left({G}\right)\in \mathrm{Moore}\left({\mathrm{Base}}_{{G}}\right)$
68 3 mrcid ${⊢}\left(\mathrm{SubGrp}\left({G}\right)\in \mathrm{Moore}\left({\mathrm{Base}}_{{G}}\right)\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\to \mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left({S}\right)={S}$
69 67 68 sylancom ${⊢}\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\to \mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left({S}\right)={S}$
70 66 69 eqtrd ${⊢}\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\to \mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)\left(\bigcup \mathrm{ran}\left\{⟨{A},{S}⟩\right\}\right)={S}$
71 59 70 eqtrd ${⊢}\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\to {G}\mathrm{DProd}\left\{⟨{A},{S}⟩\right\}={S}$
72 57 71 jca ${⊢}\left({A}\in {V}\wedge {S}\in \mathrm{SubGrp}\left({G}\right)\right)\to \left({G}\mathrm{dom}\mathrm{DProd}\left\{⟨{A},{S}⟩\right\}\wedge {G}\mathrm{DProd}\left\{⟨{A},{S}⟩\right\}={S}\right)$