Metamath Proof Explorer

Theorem mgpress

Description: Subgroup commutes with the multiplication group operator. (Contributed by Mario Carneiro, 10-Jan-2015)

Ref Expression
Hypotheses mgpress.1 
|- S = ( R |`s A )
mgpress.2 
|- M = ( mulGrp ` R )
Assertion mgpress 
|- ( ( R e. V /\ A e. W ) -> ( M |`s A ) = ( mulGrp ` S ) )

Proof

Step Hyp Ref Expression
1 mgpress.1 
 |-  S = ( R |`s A )
2 mgpress.2 
 |-  M = ( mulGrp ` R )
3 simpr 
 |-  ( ( ( R e. V /\ A e. W ) /\ ( Base ` R ) C_ A ) -> ( Base ` R ) C_ A )
4 2 fvexi 
 |-  M e. _V
5 4 a1i 
 |-  ( ( ( R e. V /\ A e. W ) /\ ( Base ` R ) C_ A ) -> M e. _V )
6 simplr 
 |-  ( ( ( R e. V /\ A e. W ) /\ ( Base ` R ) C_ A ) -> A e. W )
7 eqid 
 |-  ( M |`s A ) = ( M |`s A )
8 eqid 
 |-  ( Base ` R ) = ( Base ` R )
9 2 8 mgpbas 
 |-  ( Base ` R ) = ( Base ` M )
10 7 9 ressid2 
 |-  ( ( ( Base ` R ) C_ A /\ M e. _V /\ A e. W ) -> ( M |`s A ) = M )
11 3 5 6 10 syl3anc 
 |-  ( ( ( R e. V /\ A e. W ) /\ ( Base ` R ) C_ A ) -> ( M |`s A ) = M )
12 simpll 
 |-  ( ( ( R e. V /\ A e. W ) /\ ( Base ` R ) C_ A ) -> R e. V )
13 1 8 ressid2 
 |-  ( ( ( Base ` R ) C_ A /\ R e. V /\ A e. W ) -> S = R )
14 3 12 6 13 syl3anc 
 |-  ( ( ( R e. V /\ A e. W ) /\ ( Base ` R ) C_ A ) -> S = R )
15 14 fveq2d 
 |-  ( ( ( R e. V /\ A e. W ) /\ ( Base ` R ) C_ A ) -> ( mulGrp ` S ) = ( mulGrp ` R ) )
16 2 11 15 3eqtr4a 
 |-  ( ( ( R e. V /\ A e. W ) /\ ( Base ` R ) C_ A ) -> ( M |`s A ) = ( mulGrp ` S ) )
17 eqid 
 |-  ( .r ` R ) = ( .r ` R )
18 2 17 mgpval 
 |-  M = ( R sSet <. ( +g ` ndx ) , ( .r ` R ) >. )
19 18 oveq1i 
 |-  ( M sSet <. ( Base ` ndx ) , ( A i^i ( Base ` R ) ) >. ) = ( ( R sSet <. ( +g ` ndx ) , ( .r ` R ) >. ) sSet <. ( Base ` ndx ) , ( A i^i ( Base ` R ) ) >. )
20 simpr 
 |-  ( ( ( R e. V /\ A e. W ) /\ -. ( Base ` R ) C_ A ) -> -. ( Base ` R ) C_ A )
21 4 a1i 
 |-  ( ( ( R e. V /\ A e. W ) /\ -. ( Base ` R ) C_ A ) -> M e. _V )
22 simplr 
 |-  ( ( ( R e. V /\ A e. W ) /\ -. ( Base ` R ) C_ A ) -> A e. W )
23 7 9 ressval2 
 |-  ( ( -. ( Base ` R ) C_ A /\ M e. _V /\ A e. W ) -> ( M |`s A ) = ( M sSet <. ( Base ` ndx ) , ( A i^i ( Base ` R ) ) >. ) )
24 20 21 22 23 syl3anc 
 |-  ( ( ( R e. V /\ A e. W ) /\ -. ( Base ` R ) C_ A ) -> ( M |`s A ) = ( M sSet <. ( Base ` ndx ) , ( A i^i ( Base ` R ) ) >. ) )
25 eqid 
 |-  ( mulGrp ` S ) = ( mulGrp ` S )
26 eqid 
 |-  ( .r ` S ) = ( .r ` S )
27 25 26 mgpval 
 |-  ( mulGrp ` S ) = ( S sSet <. ( +g ` ndx ) , ( .r ` S ) >. )
28 simpll 
 |-  ( ( ( R e. V /\ A e. W ) /\ -. ( Base ` R ) C_ A ) -> R e. V )
29 1 8 ressval2 
 |-  ( ( -. ( Base ` R ) C_ A /\ R e. V /\ A e. W ) -> S = ( R sSet <. ( Base ` ndx ) , ( A i^i ( Base ` R ) ) >. ) )
30 20 28 22 29 syl3anc 
 |-  ( ( ( R e. V /\ A e. W ) /\ -. ( Base ` R ) C_ A ) -> S = ( R sSet <. ( Base ` ndx ) , ( A i^i ( Base ` R ) ) >. ) )
31 1 17 ressmulr 
 |-  ( A e. W -> ( .r ` R ) = ( .r ` S ) )
32 31 eqcomd 
 |-  ( A e. W -> ( .r ` S ) = ( .r ` R ) )
33 32 ad2antlr 
 |-  ( ( ( R e. V /\ A e. W ) /\ -. ( Base ` R ) C_ A ) -> ( .r ` S ) = ( .r ` R ) )
34 33 opeq2d 
 |-  ( ( ( R e. V /\ A e. W ) /\ -. ( Base ` R ) C_ A ) -> <. ( +g ` ndx ) , ( .r ` S ) >. = <. ( +g ` ndx ) , ( .r ` R ) >. )
35 30 34 oveq12d 
 |-  ( ( ( R e. V /\ A e. W ) /\ -. ( Base ` R ) C_ A ) -> ( S sSet <. ( +g ` ndx ) , ( .r ` S ) >. ) = ( ( R sSet <. ( Base ` ndx ) , ( A i^i ( Base ` R ) ) >. ) sSet <. ( +g ` ndx ) , ( .r ` R ) >. ) )
36 27 35 eqtrid 
 |-  ( ( ( R e. V /\ A e. W ) /\ -. ( Base ` R ) C_ A ) -> ( mulGrp ` S ) = ( ( R sSet <. ( Base ` ndx ) , ( A i^i ( Base ` R ) ) >. ) sSet <. ( +g ` ndx ) , ( .r ` R ) >. ) )
37 1ne2 
 |-  1 =/= 2
38 37 necomi 
 |-  2 =/= 1
39 plusgndx 
 |-  ( +g ` ndx ) = 2
40 basendx 
 |-  ( Base ` ndx ) = 1
41 39 40 neeq12i 
 |-  ( ( +g ` ndx ) =/= ( Base ` ndx ) <-> 2 =/= 1 )
42 38 41 mpbir 
 |-  ( +g ` ndx ) =/= ( Base ` ndx )
43 fvex 
 |-  ( .r ` R ) e. _V
44 fvex 
 |-  ( Base ` R ) e. _V
45 44 inex2 
 |-  ( A i^i ( Base ` R ) ) e. _V
46 fvex 
 |-  ( +g ` ndx ) e. _V
47 fvex 
 |-  ( Base ` ndx ) e. _V
48 46 47 setscom 
 |-  ( ( ( R e. V /\ ( +g ` ndx ) =/= ( Base ` ndx ) ) /\ ( ( .r ` R ) e. _V /\ ( A i^i ( Base ` R ) ) e. _V ) ) -> ( ( R sSet <. ( +g ` ndx ) , ( .r ` R ) >. ) sSet <. ( Base ` ndx ) , ( A i^i ( Base ` R ) ) >. ) = ( ( R sSet <. ( Base ` ndx ) , ( A i^i ( Base ` R ) ) >. ) sSet <. ( +g ` ndx ) , ( .r ` R ) >. ) )
49 43 45 48 mpanr12 
 |-  ( ( R e. V /\ ( +g ` ndx ) =/= ( Base ` ndx ) ) -> ( ( R sSet <. ( +g ` ndx ) , ( .r ` R ) >. ) sSet <. ( Base ` ndx ) , ( A i^i ( Base ` R ) ) >. ) = ( ( R sSet <. ( Base ` ndx ) , ( A i^i ( Base ` R ) ) >. ) sSet <. ( +g ` ndx ) , ( .r ` R ) >. ) )
50 28 42 49 sylancl 
 |-  ( ( ( R e. V /\ A e. W ) /\ -. ( Base ` R ) C_ A ) -> ( ( R sSet <. ( +g ` ndx ) , ( .r ` R ) >. ) sSet <. ( Base ` ndx ) , ( A i^i ( Base ` R ) ) >. ) = ( ( R sSet <. ( Base ` ndx ) , ( A i^i ( Base ` R ) ) >. ) sSet <. ( +g ` ndx ) , ( .r ` R ) >. ) )
51 36 50 eqtr4d 
 |-  ( ( ( R e. V /\ A e. W ) /\ -. ( Base ` R ) C_ A ) -> ( mulGrp ` S ) = ( ( R sSet <. ( +g ` ndx ) , ( .r ` R ) >. ) sSet <. ( Base ` ndx ) , ( A i^i ( Base ` R ) ) >. ) )
52 19 24 51 3eqtr4a 
 |-  ( ( ( R e. V /\ A e. W ) /\ -. ( Base ` R ) C_ A ) -> ( M |`s A ) = ( mulGrp ` S ) )
53 16 52 pm2.61dan 
 |-  ( ( R e. V /\ A e. W ) -> ( M |`s A ) = ( mulGrp ` S ) )