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 A V S SubGrp G G dom DProd A S G DProd A S = S

Proof

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