Theorem ringm2neg

Description: Double negation of a product in a ring. ( mul2neg analog.) (Contributed by Mario Carneiro, 4-Dec-2014) (Proof shortened by AV, 30-Mar-2025)

	Ref	Expression
Hypotheses	ringneglmul.b	|- B = ( Base ` R )
	ringneglmul.t	|- .x. = ( .r ` R )
	ringneglmul.n	|- N = ( invg ` R )
	ringneglmul.r	|- ( ph -> R e. Ring )
	ringneglmul.x	|- ( ph -> X e. B )
	ringneglmul.y	|- ( ph -> Y e. B )
Assertion	ringm2neg	|- ( ph -> ( ( N ` X ) .x. ( N ` Y ) ) = ( X .x. Y ) )

Proof

Step	Hyp	Ref	Expression
1		ringneglmul.b	|- B = ( Base ` R )
2		ringneglmul.t	|- .x. = ( .r ` R )
3		ringneglmul.n	|- N = ( invg ` R )
4		ringneglmul.r	|- ( ph -> R e. Ring )
5		ringneglmul.x	|- ( ph -> X e. B )
6		ringneglmul.y	|- ( ph -> Y e. B )
7		ringrng	|- ( R e. Ring -> R e. Rng )
8	4 7	syl	|- ( ph -> R e. Rng )
9	1 2 3 8 5 6	rngm2neg	|- ( ph -> ( ( N ` X ) .x. ( N ` Y ) ) = ( X .x. Y ) )