Metamath Proof Explorer

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