Metamath Proof Explorer

Theorem srapwov

Description: The "power" operation on a subring algebra. (Contributed by Thierry Arnoux, 10-Jan-2026)

Ref Expression
Hypotheses srapwov.a 
|- A = ( ( subringAlg ` W ) ` S )
srapwov.w 
|- ( ph -> W e. Ring )
srapwov.s 
|- ( ph -> S C_ ( Base ` W ) )
Assertion srapwov 
|- ( ph -> ( .g ` ( mulGrp ` W ) ) = ( .g ` ( mulGrp ` A ) ) )

Proof

Step Hyp Ref Expression
1 srapwov.a 
 |-  A = ( ( subringAlg ` W ) ` S )
2 srapwov.w 
 |-  ( ph -> W e. Ring )
3 srapwov.s 
 |-  ( ph -> S C_ ( Base ` W ) )
4 eqid 
 |-  ( .g ` ( mulGrp ` W ) ) = ( .g ` ( mulGrp ` W ) )
5 eqid 
 |-  ( .g ` ( mulGrp ` A ) ) = ( .g ` ( mulGrp ` A ) )
6 eqid 
 |-  ( mulGrp ` W ) = ( mulGrp ` W )
7 eqid 
 |-  ( Base ` W ) = ( Base ` W )
8 6 7 mgpbas 
 |-  ( Base ` W ) = ( Base ` ( mulGrp ` W ) )
9 8 a1i 
 |-  ( ph -> ( Base ` W ) = ( Base ` ( mulGrp ` W ) ) )
10 1 a1i 
 |-  ( ph -> A = ( ( subringAlg ` W ) ` S ) )
11 10 3 srabase 
 |-  ( ph -> ( Base ` W ) = ( Base ` A ) )
12 eqid 
 |-  ( mulGrp ` A ) = ( mulGrp ` A )
13 eqid 
 |-  ( Base ` A ) = ( Base ` A )
14 12 13 mgpbas 
 |-  ( Base ` A ) = ( Base ` ( mulGrp ` A ) )
15 11 14 eqtrdi 
 |-  ( ph -> ( Base ` W ) = ( Base ` ( mulGrp ` A ) ) )
16 ssidd 
 |-  ( ph -> ( Base ` W ) C_ ( Base ` W ) )
17 eqid 
 |-  ( .r ` W ) = ( .r ` W )
18 6 17 mgpplusg 
 |-  ( .r ` W ) = ( +g ` ( mulGrp ` W ) )
19 18 eqcomi 
 |-  ( +g ` ( mulGrp ` W ) ) = ( .r ` W )
20 2 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> W e. Ring )
21 simprl 
 |-  ( ( ph /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> x e. ( Base ` W ) )
22 simprr 
 |-  ( ( ph /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> y e. ( Base ` W ) )
23 7 19 20 21 22 ringcld 
 |-  ( ( ph /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> ( x ( +g ` ( mulGrp ` W ) ) y ) e. ( Base ` W ) )
24 10 3 sramulr 
 |-  ( ph -> ( .r ` W ) = ( .r ` A ) )
25 1 fveq2i 
 |-  ( mulGrp ` A ) = ( mulGrp ` ( ( subringAlg ` W ) ` S ) )
26 1 fveq2i 
 |-  ( .r ` A ) = ( .r ` ( ( subringAlg ` W ) ` S ) )
27 25 26 mgpplusg 
 |-  ( .r ` A ) = ( +g ` ( mulGrp ` A ) )
28 24 18 27 3eqtr3g 
 |-  ( ph -> ( +g ` ( mulGrp ` W ) ) = ( +g ` ( mulGrp ` A ) ) )
29 28 oveqdr 
 |-  ( ( ph /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> ( x ( +g ` ( mulGrp ` W ) ) y ) = ( x ( +g ` ( mulGrp ` A ) ) y ) )
30 4 5 9 15 16 23 29 mulgpropd 
 |-  ( ph -> ( .g ` ( mulGrp ` W ) ) = ( .g ` ( mulGrp ` A ) ) )