Theorem srng0

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

	Ref	Expression
Hypotheses	srng0.i	|- .* = ( *r ` R )
	srng0.z	|- .0. = ( 0g ` R )
Assertion	srng0	|- ( R e. *Ring -> ( .* ` .0. ) = .0. )

Proof

Step	Hyp	Ref	Expression
1		srng0.i	|- .* = ( *r ` R )
2		srng0.z	|- .0. = ( 0g ` R )
3		srngring	|- ( R e. *Ring -> R e. Ring )
4		ringgrp	|- ( R e. Ring -> R e. Grp )
5		eqid	|- ( Base ` R ) = ( Base ` R )
6	5 2	grpidcl	|- ( R e. Grp -> .0. e. ( Base ` R ) )
7		eqid	|- ( *rf ` R ) = ( *rf ` R )
8	5 1 7	stafval	|- ( .0. e. ( Base ` R ) -> ( ( *rf ` R ) ` .0. ) = ( .* ` .0. ) )
9	3 4 6 8	4syl	|- ( R e. *Ring -> ( ( *rf ` R ) ` .0. ) = ( .* ` .0. ) )
10		eqid	|- ( oppR ` R ) = ( oppR ` R )
11	10 7	srngrhm	|- ( R e. *Ring -> ( *rf ` R ) e. ( R RingHom ( oppR ` R ) ) )
12		rhmghm	|- ( ( *rf ` R ) e. ( R RingHom ( oppR ` R ) ) -> ( *rf ` R ) e. ( R GrpHom ( oppR ` R ) ) )
13	10 2	oppr0	|- .0. = ( 0g ` ( oppR ` R ) )
14	2 13	ghmid	|- ( ( *rf ` R ) e. ( R GrpHom ( oppR ` R ) ) -> ( ( *rf ` R ) ` .0. ) = .0. )
15	11 12 14	3syl	|- ( R e. *Ring -> ( ( *rf ` R ) ` .0. ) = .0. )
16	9 15	eqtr3d	|- ( R e. *Ring -> ( .* ` .0. ) = .0. )