This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dprdpr

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

Ref Expression
Hypotheses dmdprdpr.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
dmdprdpr.0 ⊢ 0 = ( 0g ‘ 𝐺 )
dmdprdpr.s ⊢ ( 𝜑 → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
dmdprdpr.t ⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
dprdpr.s ⊢ ⊕ = ( LSSum ‘ 𝐺 )
dprdpr.1 ⊢ ( 𝜑 → 𝑆 ⊆ ( 𝑍 ‘ 𝑇 ) )
dprdpr.2 ⊢ ( 𝜑 → ( 𝑆 ∩ 𝑇 ) = { 0 } )
Assertion dprdpr ( 𝜑 → ( 𝐺 DProd { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ) = ( 𝑆 ⊕ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 dmdprdpr.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
2 dmdprdpr.0 ⊢ 0 = ( 0g ‘ 𝐺 )
3 dmdprdpr.s ⊢ ( 𝜑 → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
4 dmdprdpr.t ⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
5 dprdpr.s ⊢ ⊕ = ( LSSum ‘ 𝐺 )
6 dprdpr.1 ⊢ ( 𝜑 → 𝑆 ⊆ ( 𝑍 ‘ 𝑇 ) )
7 dprdpr.2 ⊢ ( 𝜑 → ( 𝑆 ∩ 𝑇 ) = { 0 } )
8 xpscf ⊢ ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } : 2o ⟶ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ) )
9 3 4 8 sylanbrc ⊢ ( 𝜑 → { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } : 2o ⟶ ( SubGrp ‘ 𝐺 ) )
10 1n0 ⊢ 1o ≠ ∅
11 10 necomi ⊢ ∅ ≠ 1o
12 disjsn2 ⊢ ( ∅ ≠ 1o → ( { ∅ } ∩ { 1o } ) = ∅ )
13 11 12 mp1i ⊢ ( 𝜑 → ( { ∅ } ∩ { 1o } ) = ∅ )
14 df2o3 ⊢ 2o = { ∅ , 1o }
15 df-pr ⊢ { ∅ , 1o } = ( { ∅ } ∪ { 1o } )
16 14 15 eqtri ⊢ 2o = ( { ∅ } ∪ { 1o } )
17 16 a1i ⊢ ( 𝜑 → 2o = ( { ∅ } ∪ { 1o } ) )
18 1 2 3 4 dmdprdpr ⊢ ( 𝜑 → ( 𝐺 dom DProd { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ↔ ( 𝑆 ⊆ ( 𝑍 ‘ 𝑇 ) ∧ ( 𝑆 ∩ 𝑇 ) = { 0 } ) ) )
19 6 7 18 mpbir2and ⊢ ( 𝜑 → 𝐺 dom DProd { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } )
20 9 13 17 5 19 dprdsplit ⊢ ( 𝜑 → ( 𝐺 DProd { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ) = ( ( 𝐺 DProd ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ↾ { ∅ } ) ) ⊕ ( 𝐺 DProd ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ↾ { 1o } ) ) ) )
21 9 ffnd ⊢ ( 𝜑 → { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } Fn 2o )
22 0ex ⊢ ∅ ∈ V
23 22 prid1 ⊢ ∅ ∈ { ∅ , 1o }
24 23 14 eleqtrri ⊢ ∅ ∈ 2o
25 fnressn ⊢ ( ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } Fn 2o ∧ ∅ ∈ 2o ) → ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ↾ { ∅ } ) = { ⟨ ∅ , ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ‘ ∅ ) ⟩ } )
26 21 24 25 sylancl ⊢ ( 𝜑 → ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ↾ { ∅ } ) = { ⟨ ∅ , ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ‘ ∅ ) ⟩ } )
27 fvpr0o ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ‘ ∅ ) = 𝑆 )
28 3 27 syl ⊢ ( 𝜑 → ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ‘ ∅ ) = 𝑆 )
29 28 opeq2d ⊢ ( 𝜑 → ⟨ ∅ , ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ‘ ∅ ) ⟩ = ⟨ ∅ , 𝑆 ⟩ )
30 29 sneqd ⊢ ( 𝜑 → { ⟨ ∅ , ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ‘ ∅ ) ⟩ } = { ⟨ ∅ , 𝑆 ⟩ } )
31 26 30 eqtrd ⊢ ( 𝜑 → ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ↾ { ∅ } ) = { ⟨ ∅ , 𝑆 ⟩ } )
32 31 oveq2d ⊢ ( 𝜑 → ( 𝐺 DProd ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ↾ { ∅ } ) ) = ( 𝐺 DProd { ⟨ ∅ , 𝑆 ⟩ } ) )
33 dprdsn ⊢ ( ( ∅ ∈ V ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝐺 dom DProd { ⟨ ∅ , 𝑆 ⟩ } ∧ ( 𝐺 DProd { ⟨ ∅ , 𝑆 ⟩ } ) = 𝑆 ) )
34 22 3 33 sylancr ⊢ ( 𝜑 → ( 𝐺 dom DProd { ⟨ ∅ , 𝑆 ⟩ } ∧ ( 𝐺 DProd { ⟨ ∅ , 𝑆 ⟩ } ) = 𝑆 ) )
35 34 simprd ⊢ ( 𝜑 → ( 𝐺 DProd { ⟨ ∅ , 𝑆 ⟩ } ) = 𝑆 )
36 32 35 eqtrd ⊢ ( 𝜑 → ( 𝐺 DProd ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ↾ { ∅ } ) ) = 𝑆 )
37 1oex ⊢ 1o ∈ V
38 37 prid2 ⊢ 1o ∈ { ∅ , 1o }
39 38 14 eleqtrri ⊢ 1o ∈ 2o
40 fnressn ⊢ ( ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } Fn 2o ∧ 1o ∈ 2o ) → ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ↾ { 1o } ) = { ⟨ 1o , ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ‘ 1o ) ⟩ } )
41 21 39 40 sylancl ⊢ ( 𝜑 → ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ↾ { 1o } ) = { ⟨ 1o , ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ‘ 1o ) ⟩ } )
42 fvpr1o ⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ‘ 1o ) = 𝑇 )
43 4 42 syl ⊢ ( 𝜑 → ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ‘ 1o ) = 𝑇 )
44 43 opeq2d ⊢ ( 𝜑 → ⟨ 1o , ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ‘ 1o ) ⟩ = ⟨ 1o , 𝑇 ⟩ )
45 44 sneqd ⊢ ( 𝜑 → { ⟨ 1o , ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ‘ 1o ) ⟩ } = { ⟨ 1o , 𝑇 ⟩ } )
46 41 45 eqtrd ⊢ ( 𝜑 → ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ↾ { 1o } ) = { ⟨ 1o , 𝑇 ⟩ } )
47 46 oveq2d ⊢ ( 𝜑 → ( 𝐺 DProd ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ↾ { 1o } ) ) = ( 𝐺 DProd { ⟨ 1o , 𝑇 ⟩ } ) )
48 1on ⊢ 1o ∈ On
49 dprdsn ⊢ ( ( 1o ∈ On ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝐺 dom DProd { ⟨ 1o , 𝑇 ⟩ } ∧ ( 𝐺 DProd { ⟨ 1o , 𝑇 ⟩ } ) = 𝑇 ) )
50 48 4 49 sylancr ⊢ ( 𝜑 → ( 𝐺 dom DProd { ⟨ 1o , 𝑇 ⟩ } ∧ ( 𝐺 DProd { ⟨ 1o , 𝑇 ⟩ } ) = 𝑇 ) )
51 50 simprd ⊢ ( 𝜑 → ( 𝐺 DProd { ⟨ 1o , 𝑇 ⟩ } ) = 𝑇 )
52 47 51 eqtrd ⊢ ( 𝜑 → ( 𝐺 DProd ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ↾ { 1o } ) ) = 𝑇 )
53 36 52 oveq12d ⊢ ( 𝜑 → ( ( 𝐺 DProd ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ↾ { ∅ } ) ) ⊕ ( 𝐺 DProd ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ↾ { 1o } ) ) ) = ( 𝑆 ⊕ 𝑇 ) )
54 20 53 eqtrd ⊢ ( 𝜑 → ( 𝐺 DProd { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ) = ( 𝑆 ⊕ 𝑇 ) )