This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 )
srapwov.w ⊢ ( 𝜑 → 𝑊 ∈ Ring )
srapwov.s ⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
Assertion srapwov ( 𝜑 → ( .g ‘ ( mulGrp ‘ 𝑊 ) ) = ( .g ‘ ( mulGrp ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 srapwov.a ⊢ 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 )
2 srapwov.w ⊢ ( 𝜑 → 𝑊 ∈ Ring )
3 srapwov.s ⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
4 eqid ⊢ ( .g ‘ ( mulGrp ‘ 𝑊 ) ) = ( .g ‘ ( mulGrp ‘ 𝑊 ) )
5 eqid ⊢ ( .g ‘ ( mulGrp ‘ 𝐴 ) ) = ( .g ‘ ( mulGrp ‘ 𝐴 ) )
6 eqid ⊢ ( mulGrp ‘ 𝑊 ) = ( mulGrp ‘ 𝑊 )
7 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
8 6 7 mgpbas ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ ( mulGrp ‘ 𝑊 ) )
9 8 a1i ⊢ ( 𝜑 → ( Base ‘ 𝑊 ) = ( Base ‘ ( mulGrp ‘ 𝑊 ) ) )
10 1 a1i ⊢ ( 𝜑 → 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) )
11 10 3 srabase ⊢ ( 𝜑 → ( Base ‘ 𝑊 ) = ( Base ‘ 𝐴 ) )
12 eqid ⊢ ( mulGrp ‘ 𝐴 ) = ( mulGrp ‘ 𝐴 )
13 eqid ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
14 12 13 mgpbas ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ ( mulGrp ‘ 𝐴 ) )
15 11 14 eqtrdi ⊢ ( 𝜑 → ( Base ‘ 𝑊 ) = ( Base ‘ ( mulGrp ‘ 𝐴 ) ) )
16 ssidd ⊢ ( 𝜑 → ( Base ‘ 𝑊 ) ⊆ ( Base ‘ 𝑊 ) )
17 eqid ⊢ ( .r ‘ 𝑊 ) = ( .r ‘ 𝑊 )
18 6 17 mgpplusg ⊢ ( .r ‘ 𝑊 ) = ( +g ‘ ( mulGrp ‘ 𝑊 ) )
19 18 eqcomi ⊢ ( +g ‘ ( mulGrp ‘ 𝑊 ) ) = ( .r ‘ 𝑊 )
20 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑊 ∈ Ring )
21 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑊 ) )
22 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑊 ) )
23 7 19 20 21 22 ringcld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑥 ( +g ‘ ( mulGrp ‘ 𝑊 ) ) 𝑦 ) ∈ ( Base ‘ 𝑊 ) )
24 10 3 sramulr ⊢ ( 𝜑 → ( .r ‘ 𝑊 ) = ( .r ‘ 𝐴 ) )
25 1 fveq2i ⊢ ( mulGrp ‘ 𝐴 ) = ( mulGrp ‘ ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) )
26 1 fveq2i ⊢ ( .r ‘ 𝐴 ) = ( .r ‘ ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) )
27 25 26 mgpplusg ⊢ ( .r ‘ 𝐴 ) = ( +g ‘ ( mulGrp ‘ 𝐴 ) )
28 24 18 27 3eqtr3g ⊢ ( 𝜑 → ( +g ‘ ( mulGrp ‘ 𝑊 ) ) = ( +g ‘ ( mulGrp ‘ 𝐴 ) ) )
29 28 oveqdr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑥 ( +g ‘ ( mulGrp ‘ 𝑊 ) ) 𝑦 ) = ( 𝑥 ( +g ‘ ( mulGrp ‘ 𝐴 ) ) 𝑦 ) )
30 4 5 9 15 16 23 29 mulgpropd ⊢ ( 𝜑 → ( .g ‘ ( mulGrp ‘ 𝑊 ) ) = ( .g ‘ ( mulGrp ‘ 𝐴 ) ) )