# 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 ( ( 𝐴𝑉𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝐺 dom DProd { ⟨ 𝐴 , 𝑆 ⟩ } ∧ ( 𝐺 DProd { ⟨ 𝐴 , 𝑆 ⟩ } ) = 𝑆 ) )

### Proof

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