# Metamath Proof Explorer

## Theorem srng0

Description: The conjugate of the ring zero is zero. (Contributed by Mario Carneiro, 7-Oct-2015)

Ref Expression
Hypotheses srng0.i
srng0.z
Assertion srng0

### Proof

Step Hyp Ref Expression
1 srng0.i
2 srng0.z
3 srngring ${⊢}{R}\in \mathrm{*-Ring}\to {R}\in \mathrm{Ring}$
4 ringgrp ${⊢}{R}\in \mathrm{Ring}\to {R}\in \mathrm{Grp}$
5 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
6 5 2 grpidcl
7 eqid ${⊢}{\ast }_{\mathrm{𝑟𝑓}}\left({R}\right)={\ast }_{\mathrm{𝑟𝑓}}\left({R}\right)$
8 5 1 7 stafval
9 3 4 6 8 4syl
10 eqid ${⊢}{opp}_{r}\left({R}\right)={opp}_{r}\left({R}\right)$
11 10 7 srngrhm ${⊢}{R}\in \mathrm{*-Ring}\to {\ast }_{\mathrm{𝑟𝑓}}\left({R}\right)\in \left({R}\mathrm{RingHom}{opp}_{r}\left({R}\right)\right)$
12 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)$
13 10 2 oppr0
14 2 13 ghmid
15 11 12 14 3syl
16 9 15 eqtr3d