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

Metamath Proof Explorer

Theorem dmdprdpr

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
Hypotheses dmdprdpr.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
dmdprdpr.0 ⊢ 0 = ( 0g ‘ 𝐺 )
dmdprdpr.s ⊢ ( 𝜑 → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
dmdprdpr.t ⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
Assertion dmdprdpr ( 𝜑 → ( 𝐺 dom DProd { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ↔ ( 𝑆 ⊆ ( 𝑍 ‘ 𝑇 ) ∧ ( 𝑆 ∩ 𝑇 ) = { 0 } ) ) )

Proof

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