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		1oelpr	⊢ 1o ∈ { ∅ , 1o }
38	37 14	eleqtrri	⊢ 1o ∈ 2o
39		fnressn	⊢ ( ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } Fn 2o ∧ 1o ∈ 2o ) → ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ↾ { 1o } ) = { ⟨ 1o , ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ‘ 1o ) ⟩ } )
40	21 38 39	sylancl	⊢ ( 𝜑 → ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ↾ { 1o } ) = { ⟨ 1o , ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ‘ 1o ) ⟩ } )
41		fvpr1o	⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ‘ 1o ) = 𝑇 )
42	4 41	syl	⊢ ( 𝜑 → ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ‘ 1o ) = 𝑇 )
43	42	opeq2d	⊢ ( 𝜑 → ⟨ 1o , ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ‘ 1o ) ⟩ = ⟨ 1o , 𝑇 ⟩ )
44	43	sneqd	⊢ ( 𝜑 → { ⟨ 1o , ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ‘ 1o ) ⟩ } = { ⟨ 1o , 𝑇 ⟩ } )
45	40 44	eqtrd	⊢ ( 𝜑 → ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ↾ { 1o } ) = { ⟨ 1o , 𝑇 ⟩ } )
46	45	oveq2d	⊢ ( 𝜑 → ( 𝐺 DProd ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ↾ { 1o } ) ) = ( 𝐺 DProd { ⟨ 1o , 𝑇 ⟩ } ) )
47		1on	⊢ 1o ∈ On
48		dprdsn	⊢ ( ( 1o ∈ On ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝐺 dom DProd { ⟨ 1o , 𝑇 ⟩ } ∧ ( 𝐺 DProd { ⟨ 1o , 𝑇 ⟩ } ) = 𝑇 ) )
49	47 4 48	sylancr	⊢ ( 𝜑 → ( 𝐺 dom DProd { ⟨ 1o , 𝑇 ⟩ } ∧ ( 𝐺 DProd { ⟨ 1o , 𝑇 ⟩ } ) = 𝑇 ) )
50	49	simprd	⊢ ( 𝜑 → ( 𝐺 DProd { ⟨ 1o , 𝑇 ⟩ } ) = 𝑇 )
51	46 50	eqtrd	⊢ ( 𝜑 → ( 𝐺 DProd ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ↾ { 1o } ) ) = 𝑇 )
52	36 51	oveq12d	⊢ ( 𝜑 → ( ( 𝐺 DProd ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ↾ { ∅ } ) ) ⊕ ( 𝐺 DProd ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ↾ { 1o } ) ) ) = ( 𝑆 ⊕ 𝑇 ) )
53	20 52	eqtrd	⊢ ( 𝜑 → ( 𝐺 DProd { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑇 ⟩ } ) = ( 𝑆 ⊕ 𝑇 ) )