Step 
Hyp 
Ref 
Expression 
1 

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

srng1.t 
⊢ 1 = ( 1_{r} ‘ 𝑅 ) 
3 

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

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

ringidcl 
⊢ ( 𝑅 ∈ Ring → 1 ∈ ( Base ‘ 𝑅 ) ) 
6 

eqid 
⊢ ( *_{rf} ‘ 𝑅 ) = ( *_{rf} ‘ 𝑅 ) 
7 
4 1 6

stafval 
⊢ ( 1 ∈ ( Base ‘ 𝑅 ) → ( ( *_{rf} ‘ 𝑅 ) ‘ 1 ) = ( ∗ ‘ 1 ) ) 
8 
3 5 7

3syl 
⊢ ( 𝑅 ∈ *Ring → ( ( *_{rf} ‘ 𝑅 ) ‘ 1 ) = ( ∗ ‘ 1 ) ) 
9 

eqid 
⊢ ( opp_{r} ‘ 𝑅 ) = ( opp_{r} ‘ 𝑅 ) 
10 
9 6

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

oppr1 
⊢ 1 = ( 1_{r} ‘ ( opp_{r} ‘ 𝑅 ) ) 
12 
2 11

rhm1 
⊢ ( ( *_{rf} ‘ 𝑅 ) ∈ ( 𝑅 RingHom ( opp_{r} ‘ 𝑅 ) ) → ( ( *_{rf} ‘ 𝑅 ) ‘ 1 ) = 1 ) 
13 
10 12

syl 
⊢ ( 𝑅 ∈ *Ring → ( ( *_{rf} ‘ 𝑅 ) ‘ 1 ) = 1 ) 
14 
8 13

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