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	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	srng0	⊢ ( 𝑅 ∈ *-Ring → ( ∗ ‘ 0 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		srng0.i	⊢ ∗ = ( *𝑟 ‘ 𝑅 )
2		srng0.z	⊢ 0 = ( 0g ‘ 𝑅 )
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	⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
11	10 7	srngrhm	⊢ ( 𝑅 ∈ *-Ring → ( *rf ‘ 𝑅 ) ∈ ( 𝑅 RingHom ( oppr ‘ 𝑅 ) ) )
12		rhmghm	⊢ ( ( *rf ‘ 𝑅 ) ∈ ( 𝑅 RingHom ( oppr ‘ 𝑅 ) ) → ( *rf ‘ 𝑅 ) ∈ ( 𝑅 GrpHom ( oppr ‘ 𝑅 ) ) )
13	10 2	oppr0	⊢ 0 = ( 0g ‘ ( oppr ‘ 𝑅 ) )
14	2 13	ghmid	⊢ ( ( *rf ‘ 𝑅 ) ∈ ( 𝑅 GrpHom ( oppr ‘ 𝑅 ) ) → ( ( *rf ‘ 𝑅 ) ‘ 0 ) = 0 )
15	11 12 14	3syl	⊢ ( 𝑅 ∈ *-Ring → ( ( *rf ‘ 𝑅 ) ‘ 0 ) = 0 )
16	9 15	eqtr3d	⊢ ( 𝑅 ∈ *-Ring → ( ∗ ‘ 0 ) = 0 )