Step 
Hyp 
Ref 
Expression 
1 

srng0.i 
⊢ ∗ = ( *_{𝑟} ‘ 𝑅 ) 
2 

srng0.z 
⊢ 0 = ( 0_{g} ‘ 𝑅 ) 
3 

srngring 
⊢ ( 𝑅 ∈ *Ring → 𝑅 ∈ Ring ) 
4 

ringgrp 
⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp ) 
5 

eqid 
⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) 
6 
5 2

grpidcl 
⊢ ( 𝑅 ∈ Grp → 0 ∈ ( Base ‘ 𝑅 ) ) 
7 

eqid 
⊢ ( *_{rf} ‘ 𝑅 ) = ( *_{rf} ‘ 𝑅 ) 
8 
5 1 7

stafval 
⊢ ( 0 ∈ ( Base ‘ 𝑅 ) → ( ( *_{rf} ‘ 𝑅 ) ‘ 0 ) = ( ∗ ‘ 0 ) ) 
9 
3 4 6 8

4syl 
⊢ ( 𝑅 ∈ *Ring → ( ( *_{rf} ‘ 𝑅 ) ‘ 0 ) = ( ∗ ‘ 0 ) ) 
10 

eqid 
⊢ ( opp_{r} ‘ 𝑅 ) = ( opp_{r} ‘ 𝑅 ) 
11 
10 7

srngrhm 
⊢ ( 𝑅 ∈ *Ring → ( *_{rf} ‘ 𝑅 ) ∈ ( 𝑅 RingHom ( opp_{r} ‘ 𝑅 ) ) ) 
12 

rhmghm 
⊢ ( ( *_{rf} ‘ 𝑅 ) ∈ ( 𝑅 RingHom ( opp_{r} ‘ 𝑅 ) ) → ( *_{rf} ‘ 𝑅 ) ∈ ( 𝑅 GrpHom ( opp_{r} ‘ 𝑅 ) ) ) 
13 
10 2

oppr0 
⊢ 0 = ( 0_{g} ‘ ( opp_{r} ‘ 𝑅 ) ) 
14 
2 13

ghmid 
⊢ ( ( *_{rf} ‘ 𝑅 ) ∈ ( 𝑅 GrpHom ( opp_{r} ‘ 𝑅 ) ) → ( ( *_{rf} ‘ 𝑅 ) ‘ 0 ) = 0 ) 
15 
11 12 14

3syl 
⊢ ( 𝑅 ∈ *Ring → ( ( *_{rf} ‘ 𝑅 ) ‘ 0 ) = 0 ) 
16 
9 15

eqtr3d 
⊢ ( 𝑅 ∈ *Ring → ( ∗ ‘ 0 ) = 0 ) 