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 } ) ) )