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	\|- Z = ( Cntz ` G )
	dmdprdpr.0	\|- .0. = ( 0g ` G )
	dmdprdpr.s	\|- ( ph -> S e. ( SubGrp ` G ) )
	dmdprdpr.t	\|- ( ph -> T e. ( SubGrp ` G ) )
	dprdpr.s	\|- .(+) = ( LSSum ` G )
	dprdpr.1	\|- ( ph -> S C_ ( Z ` T ) )
	dprdpr.2	\|- ( ph -> ( S i^i T ) = { .0. } )
Assertion	dprdpr	\|- ( ph -> ( G DProd { <. (/) , S >. , <. 1o , T >. } ) = ( S .(+) T ) )

Proof

Step	Hyp	Ref	Expression
1		dmdprdpr.z	\|- Z = ( Cntz ` G )
2		dmdprdpr.0	\|- .0. = ( 0g ` G )
3		dmdprdpr.s	\|- ( ph -> S e. ( SubGrp ` G ) )
4		dmdprdpr.t	\|- ( ph -> T e. ( SubGrp ` G ) )
5		dprdpr.s	\|- .(+) = ( LSSum ` G )
6		dprdpr.1	\|- ( ph -> S C_ ( Z ` T ) )
7		dprdpr.2	\|- ( ph -> ( S i^i T ) = { .0. } )
8		xpscf	\|- ( { <. (/) , S >. , <. 1o , T >. } : 2o --> ( SubGrp ` G ) <-> ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) ) )
9	3 4 8	sylanbrc	\|- ( ph -> { <. (/) , S >. , <. 1o , T >. } : 2o --> ( SubGrp ` G ) )
10		1n0	\|- 1o =/= (/)
11	10	necomi	\|- (/) =/= 1o
12		disjsn2	\|- ( (/) =/= 1o -> ( { (/) } i^i { 1o } ) = (/) )
13	11 12	mp1i	\|- ( ph -> ( { (/) } i^i { 1o } ) = (/) )
14		df2o3	\|- 2o = { (/) , 1o }
15		df-pr	\|- { (/) , 1o } = ( { (/) } u. { 1o } )
16	14 15	eqtri	\|- 2o = ( { (/) } u. { 1o } )
17	16	a1i	\|- ( ph -> 2o = ( { (/) } u. { 1o } ) )
18	1 2 3 4	dmdprdpr	\|- ( ph -> ( G dom DProd { <. (/) , S >. , <. 1o , T >. } <-> ( S C_ ( Z ` T ) /\ ( S i^i T ) = { .0. } ) ) )
19	6 7 18	mpbir2and	\|- ( ph -> G dom DProd { <. (/) , S >. , <. 1o , T >. } )
20	9 13 17 5 19	dprdsplit	\|- ( ph -> ( G DProd { <. (/) , S >. , <. 1o , T >. } ) = ( ( G DProd ( { <. (/) , S >. , <. 1o , T >. } \|` { (/) } ) ) .(+) ( G DProd ( { <. (/) , S >. , <. 1o , T >. } \|` { 1o } ) ) ) )
21	9	ffnd	\|- ( ph -> { <. (/) , S >. , <. 1o , T >. } Fn 2o )
22		0ex	\|- (/) e. _V
23	22	prid1	\|- (/) e. { (/) , 1o }
24	23 14	eleqtrri	\|- (/) e. 2o
25		fnressn	\|- ( ( { <. (/) , S >. , <. 1o , T >. } Fn 2o /\ (/) e. 2o ) -> ( { <. (/) , S >. , <. 1o , T >. } \|` { (/) } ) = { <. (/) , ( { <. (/) , S >. , <. 1o , T >. } ` (/) ) >. } )
26	21 24 25	sylancl	\|- ( ph -> ( { <. (/) , S >. , <. 1o , T >. } \|` { (/) } ) = { <. (/) , ( { <. (/) , S >. , <. 1o , T >. } ` (/) ) >. } )
27		fvpr0o	\|- ( S e. ( SubGrp ` G ) -> ( { <. (/) , S >. , <. 1o , T >. } ` (/) ) = S )
28	3 27	syl	\|- ( ph -> ( { <. (/) , S >. , <. 1o , T >. } ` (/) ) = S )
29	28	opeq2d	\|- ( ph -> <. (/) , ( { <. (/) , S >. , <. 1o , T >. } ` (/) ) >. = <. (/) , S >. )
30	29	sneqd	\|- ( ph -> { <. (/) , ( { <. (/) , S >. , <. 1o , T >. } ` (/) ) >. } = { <. (/) , S >. } )
31	26 30	eqtrd	\|- ( ph -> ( { <. (/) , S >. , <. 1o , T >. } \|` { (/) } ) = { <. (/) , S >. } )
32	31	oveq2d	\|- ( ph -> ( G DProd ( { <. (/) , S >. , <. 1o , T >. } \|` { (/) } ) ) = ( G DProd { <. (/) , S >. } ) )
33		dprdsn	\|- ( ( (/) e. _V /\ S e. ( SubGrp ` G ) ) -> ( G dom DProd { <. (/) , S >. } /\ ( G DProd { <. (/) , S >. } ) = S ) )
34	22 3 33	sylancr	\|- ( ph -> ( G dom DProd { <. (/) , S >. } /\ ( G DProd { <. (/) , S >. } ) = S ) )
35	34	simprd	\|- ( ph -> ( G DProd { <. (/) , S >. } ) = S )
36	32 35	eqtrd	\|- ( ph -> ( G DProd ( { <. (/) , S >. , <. 1o , T >. } \|` { (/) } ) ) = S )
37		1oex	\|- 1o e. _V
38	37	prid2	\|- 1o e. { (/) , 1o }
39	38 14	eleqtrri	\|- 1o e. 2o
40		fnressn	\|- ( ( { <. (/) , S >. , <. 1o , T >. } Fn 2o /\ 1o e. 2o ) -> ( { <. (/) , S >. , <. 1o , T >. } \|` { 1o } ) = { <. 1o , ( { <. (/) , S >. , <. 1o , T >. } ` 1o ) >. } )
41	21 39 40	sylancl	\|- ( ph -> ( { <. (/) , S >. , <. 1o , T >. } \|` { 1o } ) = { <. 1o , ( { <. (/) , S >. , <. 1o , T >. } ` 1o ) >. } )
42		fvpr1o	\|- ( T e. ( SubGrp ` G ) -> ( { <. (/) , S >. , <. 1o , T >. } ` 1o ) = T )
43	4 42	syl	\|- ( ph -> ( { <. (/) , S >. , <. 1o , T >. } ` 1o ) = T )
44	43	opeq2d	\|- ( ph -> <. 1o , ( { <. (/) , S >. , <. 1o , T >. } ` 1o ) >. = <. 1o , T >. )
45	44	sneqd	\|- ( ph -> { <. 1o , ( { <. (/) , S >. , <. 1o , T >. } ` 1o ) >. } = { <. 1o , T >. } )
46	41 45	eqtrd	\|- ( ph -> ( { <. (/) , S >. , <. 1o , T >. } \|` { 1o } ) = { <. 1o , T >. } )
47	46	oveq2d	\|- ( ph -> ( G DProd ( { <. (/) , S >. , <. 1o , T >. } \|` { 1o } ) ) = ( G DProd { <. 1o , T >. } ) )
48		1on	\|- 1o e. On
49		dprdsn	\|- ( ( 1o e. On /\ T e. ( SubGrp ` G ) ) -> ( G dom DProd { <. 1o , T >. } /\ ( G DProd { <. 1o , T >. } ) = T ) )
50	48 4 49	sylancr	\|- ( ph -> ( G dom DProd { <. 1o , T >. } /\ ( G DProd { <. 1o , T >. } ) = T ) )
51	50	simprd	\|- ( ph -> ( G DProd { <. 1o , T >. } ) = T )
52	47 51	eqtrd	\|- ( ph -> ( G DProd ( { <. (/) , S >. , <. 1o , T >. } \|` { 1o } ) ) = T )
53	36 52	oveq12d	\|- ( ph -> ( ( G DProd ( { <. (/) , S >. , <. 1o , T >. } \|` { (/) } ) ) .(+) ( G DProd ( { <. (/) , S >. , <. 1o , T >. } \|` { 1o } ) ) ) = ( S .(+) T ) )
54	20 53	eqtrd	\|- ( ph -> ( G DProd { <. (/) , S >. , <. 1o , T >. } ) = ( S .(+) T ) )

Metamath Proof Explorer

Theorem dprdpr

Proof