Theorem dsmmsubg

Description: The finite hull of a product of groups is additionally closed under negation and thus is a subgroup of the product. (Contributed by Stefan O'Rear, 11-Jan-2015)

	Ref	Expression
Hypotheses	dsmmsubg.p	|- P = ( S Xs_ R )
	dsmmsubg.h	|- H = ( Base ` ( S (+)m R ) )
	dsmmsubg.i	|- ( ph -> I e. W )
	dsmmsubg.s	|- ( ph -> S e. V )
	dsmmsubg.r	|- ( ph -> R : I --> Grp )
Assertion	dsmmsubg	|- ( ph -> H e. ( SubGrp ` P ) )

Proof

Step	Hyp	Ref	Expression
1		dsmmsubg.p	|- P = ( S Xs_ R )
2		dsmmsubg.h	|- H = ( Base ` ( S (+)m R ) )
3		dsmmsubg.i	|- ( ph -> I e. W )
4		dsmmsubg.s	|- ( ph -> S e. V )
5		dsmmsubg.r	|- ( ph -> R : I --> Grp )
6		eqidd	|- ( ph -> ( P |`s H ) = ( P |`s H ) )
7		eqidd	|- ( ph -> ( 0g ` P ) = ( 0g ` P ) )
8		eqidd	|- ( ph -> ( +g ` P ) = ( +g ` P ) )
9		fex	|- ( ( R : I --> Grp /\ I e. W ) -> R e. _V )
10	5 3 9	syl2anc	|- ( ph -> R e. _V )
11		eqid	|- { a e. ( Base ` ( S Xs_ R ) ) | { b e. dom R | ( a ` b ) =/= ( 0g ` ( R ` b ) ) } e. Fin } = { a e. ( Base ` ( S Xs_ R ) ) | { b e. dom R | ( a ` b ) =/= ( 0g ` ( R ` b ) ) } e. Fin }
12	11	dsmmbase	|- ( R e. _V -> { a e. ( Base ` ( S Xs_ R ) ) | { b e. dom R | ( a ` b ) =/= ( 0g ` ( R ` b ) ) } e. Fin } = ( Base ` ( S (+)m R ) ) )
13	10 12	syl	|- ( ph -> { a e. ( Base ` ( S Xs_ R ) ) | { b e. dom R | ( a ` b ) =/= ( 0g ` ( R ` b ) ) } e. Fin } = ( Base ` ( S (+)m R ) ) )
14		ssrab2	|- { a e. ( Base ` ( S Xs_ R ) ) | { b e. dom R | ( a ` b ) =/= ( 0g ` ( R ` b ) ) } e. Fin } C_ ( Base ` ( S Xs_ R ) )
15	13 14	eqsstrrdi	|- ( ph -> ( Base ` ( S (+)m R ) ) C_ ( Base ` ( S Xs_ R ) ) )
16	1	fveq2i	|- ( Base ` P ) = ( Base ` ( S Xs_ R ) )
17	15 2 16	3sstr4g	|- ( ph -> H C_ ( Base ` P ) )
18		grpmnd	|- ( a e. Grp -> a e. Mnd )
19	18	ssriv	|- Grp C_ Mnd
20		fss	|- ( ( R : I --> Grp /\ Grp C_ Mnd ) -> R : I --> Mnd )
21	5 19 20	sylancl	|- ( ph -> R : I --> Mnd )
22		eqid	|- ( 0g ` P ) = ( 0g ` P )
23	1 2 3 4 21 22	dsmm0cl	|- ( ph -> ( 0g ` P ) e. H )
24	3	3ad2ant1	|- ( ( ph /\ a e. H /\ b e. H ) -> I e. W )
25	4	3ad2ant1	|- ( ( ph /\ a e. H /\ b e. H ) -> S e. V )
26	21	3ad2ant1	|- ( ( ph /\ a e. H /\ b e. H ) -> R : I --> Mnd )
27		simp2	|- ( ( ph /\ a e. H /\ b e. H ) -> a e. H )
28		simp3	|- ( ( ph /\ a e. H /\ b e. H ) -> b e. H )
29		eqid	|- ( +g ` P ) = ( +g ` P )
30	1 2 24 25 26 27 28 29	dsmmacl	|- ( ( ph /\ a e. H /\ b e. H ) -> ( a ( +g ` P ) b ) e. H )
31	1 3 4 5	prdsgrpd	|- ( ph -> P e. Grp )
32	31	adantr	|- ( ( ph /\ a e. H ) -> P e. Grp )
33	17	sselda	|- ( ( ph /\ a e. H ) -> a e. ( Base ` P ) )
34		eqid	|- ( Base ` P ) = ( Base ` P )
35		eqid	|- ( invg ` P ) = ( invg ` P )
36	34 35	grpinvcl	|- ( ( P e. Grp /\ a e. ( Base ` P ) ) -> ( ( invg ` P ) ` a ) e. ( Base ` P ) )
37	32 33 36	syl2anc	|- ( ( ph /\ a e. H ) -> ( ( invg ` P ) ` a ) e. ( Base ` P ) )
38		simpr	|- ( ( ph /\ a e. H ) -> a e. H )
39		eqid	|- ( S (+)m R ) = ( S (+)m R )
40	3	adantr	|- ( ( ph /\ a e. H ) -> I e. W )
41	5	ffnd	|- ( ph -> R Fn I )
42	41	adantr	|- ( ( ph /\ a e. H ) -> R Fn I )
43	1 39 34 2 40 42	dsmmelbas	|- ( ( ph /\ a e. H ) -> ( a e. H <-> ( a e. ( Base ` P ) /\ { b e. I | ( a ` b ) =/= ( 0g ` ( R ` b ) ) } e. Fin ) ) )
44	38 43	mpbid	|- ( ( ph /\ a e. H ) -> ( a e. ( Base ` P ) /\ { b e. I | ( a ` b ) =/= ( 0g ` ( R ` b ) ) } e. Fin ) )
45	44	simprd	|- ( ( ph /\ a e. H ) -> { b e. I | ( a ` b ) =/= ( 0g ` ( R ` b ) ) } e. Fin )
46	3	ad2antrr	|- ( ( ( ph /\ a e. H ) /\ b e. I ) -> I e. W )
47	4	ad2antrr	|- ( ( ( ph /\ a e. H ) /\ b e. I ) -> S e. V )
48	5	ad2antrr	|- ( ( ( ph /\ a e. H ) /\ b e. I ) -> R : I --> Grp )
49	33	adantr	|- ( ( ( ph /\ a e. H ) /\ b e. I ) -> a e. ( Base ` P ) )
50		simpr	|- ( ( ( ph /\ a e. H ) /\ b e. I ) -> b e. I )
51	1 46 47 48 34 35 49 50	prdsinvgd2	|- ( ( ( ph /\ a e. H ) /\ b e. I ) -> ( ( ( invg ` P ) ` a ) ` b ) = ( ( invg ` ( R ` b ) ) ` ( a ` b ) ) )
52	51	adantrr	|- ( ( ( ph /\ a e. H ) /\ ( b e. I /\ ( a ` b ) = ( 0g ` ( R ` b ) ) ) ) -> ( ( ( invg ` P ) ` a ) ` b ) = ( ( invg ` ( R ` b ) ) ` ( a ` b ) ) )
53		fveq2	|- ( ( a ` b ) = ( 0g ` ( R ` b ) ) -> ( ( invg ` ( R ` b ) ) ` ( a ` b ) ) = ( ( invg ` ( R ` b ) ) ` ( 0g ` ( R ` b ) ) ) )
54	53	ad2antll	|- ( ( ( ph /\ a e. H ) /\ ( b e. I /\ ( a ` b ) = ( 0g ` ( R ` b ) ) ) ) -> ( ( invg ` ( R ` b ) ) ` ( a ` b ) ) = ( ( invg ` ( R ` b ) ) ` ( 0g ` ( R ` b ) ) ) )
55	5	ffvelrnda	|- ( ( ph /\ b e. I ) -> ( R ` b ) e. Grp )
56	55	adantlr	|- ( ( ( ph /\ a e. H ) /\ b e. I ) -> ( R ` b ) e. Grp )
57		eqid	|- ( 0g ` ( R ` b ) ) = ( 0g ` ( R ` b ) )
58		eqid	|- ( invg ` ( R ` b ) ) = ( invg ` ( R ` b ) )
59	57 58	grpinvid	|- ( ( R ` b ) e. Grp -> ( ( invg ` ( R ` b ) ) ` ( 0g ` ( R ` b ) ) ) = ( 0g ` ( R ` b ) ) )
60	56 59	syl	|- ( ( ( ph /\ a e. H ) /\ b e. I ) -> ( ( invg ` ( R ` b ) ) ` ( 0g ` ( R ` b ) ) ) = ( 0g ` ( R ` b ) ) )
61	60	adantrr	|- ( ( ( ph /\ a e. H ) /\ ( b e. I /\ ( a ` b ) = ( 0g ` ( R ` b ) ) ) ) -> ( ( invg ` ( R ` b ) ) ` ( 0g ` ( R ` b ) ) ) = ( 0g ` ( R ` b ) ) )
62	52 54 61	3eqtrd	|- ( ( ( ph /\ a e. H ) /\ ( b e. I /\ ( a ` b ) = ( 0g ` ( R ` b ) ) ) ) -> ( ( ( invg ` P ) ` a ) ` b ) = ( 0g ` ( R ` b ) ) )
63	62	expr	|- ( ( ( ph /\ a e. H ) /\ b e. I ) -> ( ( a ` b ) = ( 0g ` ( R ` b ) ) -> ( ( ( invg ` P ) ` a ) ` b ) = ( 0g ` ( R ` b ) ) ) )
64	63	necon3d	|- ( ( ( ph /\ a e. H ) /\ b e. I ) -> ( ( ( ( invg ` P ) ` a ) ` b ) =/= ( 0g ` ( R ` b ) ) -> ( a ` b ) =/= ( 0g ` ( R ` b ) ) ) )
65	64	ss2rabdv	|- ( ( ph /\ a e. H ) -> { b e. I | ( ( ( invg ` P ) ` a ) ` b ) =/= ( 0g ` ( R ` b ) ) } C_ { b e. I | ( a ` b ) =/= ( 0g ` ( R ` b ) ) } )
66	45 65	ssfid	|- ( ( ph /\ a e. H ) -> { b e. I | ( ( ( invg ` P ) ` a ) ` b ) =/= ( 0g ` ( R ` b ) ) } e. Fin )
67	1 39 34 2 40 42	dsmmelbas	|- ( ( ph /\ a e. H ) -> ( ( ( invg ` P ) ` a ) e. H <-> ( ( ( invg ` P ) ` a ) e. ( Base ` P ) /\ { b e. I | ( ( ( invg ` P ) ` a ) ` b ) =/= ( 0g ` ( R ` b ) ) } e. Fin ) ) )
68	37 66 67	mpbir2and	|- ( ( ph /\ a e. H ) -> ( ( invg ` P ) ` a ) e. H )
69	6 7 8 17 23 30 68 31	issubgrpd2	|- ( ph -> H e. ( SubGrp ` P ) )