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𝑠A
mgpress.2 M=mulGrpR
Assertion mgpress RVAWM𝑠A=mulGrpS

Proof

Step Hyp Ref Expression
1 mgpress.1 S=R𝑠A
2 mgpress.2 M=mulGrpR
3 simpr RVAWBaseRABaseRA
4 2 fvexi MV
5 4 a1i RVAWBaseRAMV
6 simplr RVAWBaseRAAW
7 eqid M𝑠A=M𝑠A
8 eqid BaseR=BaseR
9 2 8 mgpbas BaseR=BaseM
10 7 9 ressid2 BaseRAMVAWM𝑠A=M
11 3 5 6 10 syl3anc RVAWBaseRAM𝑠A=M
12 simpll RVAWBaseRARV
13 1 8 ressid2 BaseRARVAWS=R
14 3 12 6 13 syl3anc RVAWBaseRAS=R
15 14 fveq2d RVAWBaseRAmulGrpS=mulGrpR
16 2 11 15 3eqtr4a RVAWBaseRAM𝑠A=mulGrpS
17 eqid R=R
18 2 17 mgpval M=RsSet+ndxR
19 18 oveq1i MsSetBasendxABaseR=RsSet+ndxRsSetBasendxABaseR
20 simpr RVAW¬BaseRA¬BaseRA
21 4 a1i RVAW¬BaseRAMV
22 simplr RVAW¬BaseRAAW
23 7 9 ressval2 ¬BaseRAMVAWM𝑠A=MsSetBasendxABaseR
24 20 21 22 23 syl3anc RVAW¬BaseRAM𝑠A=MsSetBasendxABaseR
25 eqid mulGrpS=mulGrpS
26 eqid S=S
27 25 26 mgpval mulGrpS=SsSet+ndxS
28 simpll RVAW¬BaseRARV
29 1 8 ressval2 ¬BaseRARVAWS=RsSetBasendxABaseR
30 20 28 22 29 syl3anc RVAW¬BaseRAS=RsSetBasendxABaseR
31 1 17 ressmulr AWR=S
32 31 eqcomd AWS=R
33 32 ad2antlr RVAW¬BaseRAS=R
34 33 opeq2d RVAW¬BaseRA+ndxS=+ndxR
35 30 34 oveq12d RVAW¬BaseRASsSet+ndxS=RsSetBasendxABaseRsSet+ndxR
36 27 35 eqtrid RVAW¬BaseRAmulGrpS=RsSetBasendxABaseRsSet+ndxR
37 basendxnplusgndx Basendx+ndx
38 37 necomi +ndxBasendx
39 fvex RV
40 fvex BaseRV
41 40 inex2 ABaseRV
42 fvex +ndxV
43 fvex BasendxV
44 42 43 setscom RV+ndxBasendxRVABaseRVRsSet+ndxRsSetBasendxABaseR=RsSetBasendxABaseRsSet+ndxR
45 39 41 44 mpanr12 RV+ndxBasendxRsSet+ndxRsSetBasendxABaseR=RsSetBasendxABaseRsSet+ndxR
46 28 38 45 sylancl RVAW¬BaseRARsSet+ndxRsSetBasendxABaseR=RsSetBasendxABaseRsSet+ndxR
47 36 46 eqtr4d RVAW¬BaseRAmulGrpS=RsSet+ndxRsSetBasendxABaseR
48 19 24 47 3eqtr4a RVAW¬BaseRAM𝑠A=mulGrpS
49 16 48 pm2.61dan RVAWM𝑠A=mulGrpS