Metamath Proof Explorer

Theorem mgpress

Description: Subgroup commutes with the multiplicative group operator. (Contributed by Mario Carneiro, 10-Jan-2015) (Proof shortened by AV, 18-Oct-2024)

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 basendxnplusgndx 
 |-  ( Base ` ndx ) =/= ( +g ` ndx )
38 37 necomi 
 |-  ( +g ` ndx ) =/= ( Base ` ndx )
39 fvex 
 |-  ( .r ` R ) e. _V
40 fvex 
 |-  ( Base ` R ) e. _V
41 40 inex2 
 |-  ( A i^i ( Base ` R ) ) e. _V
42 fvex 
 |-  ( +g ` ndx ) e. _V
43 fvex 
 |-  ( Base ` ndx ) e. _V
44 42 43 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 ) >. ) )
45 39 41 44 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 ) >. ) )
46 28 38 45 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 ) >. ) )
47 36 46 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 ) ) >. ) )
48 19 24 47 3eqtr4a 
 |-  ( ( ( R e. V /\ A e. W ) /\ -. ( Base ` R ) C_ A ) -> ( M |`s A ) = ( mulGrp ` S ) )
49 16 48 pm2.61dan 
 |-  ( ( R e. V /\ A e. W ) -> ( M |`s A ) = ( mulGrp ` S ) )