Metamath Proof Explorer

Theorem srngmul

Description: The involution function in a star ring distributes over multiplication, with a change in the order of the factors. (Contributed by Mario Carneiro, 6-Oct-2015)

Ref Expression
Hypotheses srngcl.i
srngcl.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
srngmul.t
Assertion srngmul

Proof

Step Hyp Ref Expression
1 srngcl.i
2 srngcl.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
3 srngmul.t
4 eqid ${⊢}{opp}_{r}\left({R}\right)={opp}_{r}\left({R}\right)$
5 eqid ${⊢}{\ast }_{\mathrm{𝑟𝑓}}\left({R}\right)={\ast }_{\mathrm{𝑟𝑓}}\left({R}\right)$
6 4 5 srngrhm ${⊢}{R}\in \mathrm{*-Ring}\to {\ast }_{\mathrm{𝑟𝑓}}\left({R}\right)\in \left({R}\mathrm{RingHom}{opp}_{r}\left({R}\right)\right)$
7 eqid ${⊢}{\cdot }_{{opp}_{r}\left({R}\right)}={\cdot }_{{opp}_{r}\left({R}\right)}$
8 2 3 7 rhmmul
9 6 8 syl3an1
10 2 3 4 7 opprmul
11 9 10 syl6eq
12 srngring ${⊢}{R}\in \mathrm{*-Ring}\to {R}\in \mathrm{Ring}$
13 2 3 ringcl
14 12 13 syl3an1
15 2 1 5 stafval
16 14 15 syl
17 2 1 5 stafval