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 { ⟨ 𝐴 , 𝑆 ⟩ } ) = 𝑆 ) )