# Metamath Proof Explorer

Description: The involution function in a star ring distributes over addition. (Contributed by Mario Carneiro, 6-Oct-2015)

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

### Proof

Step Hyp Ref Expression
1 srngcl.i
2 srngcl.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
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 rhmghm ${⊢}{\ast }_{\mathrm{𝑟𝑓}}\left({R}\right)\in \left({R}\mathrm{RingHom}{opp}_{r}\left({R}\right)\right)\to {\ast }_{\mathrm{𝑟𝑓}}\left({R}\right)\in \left({R}\mathrm{GrpHom}{opp}_{r}\left({R}\right)\right)$
8 6 7 syl ${⊢}{R}\in \mathrm{*-Ring}\to {\ast }_{\mathrm{𝑟𝑓}}\left({R}\right)\in \left({R}\mathrm{GrpHom}{opp}_{r}\left({R}\right)\right)$
12 srngring ${⊢}{R}\in \mathrm{*-Ring}\to {R}\in \mathrm{Ring}$