Theorem rngm2neg

Description: Double negation of a product in a non-unital ring ( mul2neg analog). (Contributed by Mario Carneiro, 4-Dec-2014) Generalization of ringm2neg . (Revised by AV, 17-Feb-2025)

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

Proof

Step	Hyp	Ref	Expression
1		rngneglmul.b	|- B = ( Base ` R )
2		rngneglmul.t	|- .x. = ( .r ` R )
3		rngneglmul.n	|- N = ( invg ` R )
4		rngneglmul.r	|- ( ph -> R e. Rng )
5		rngneglmul.x	|- ( ph -> X e. B )
6		rngneglmul.y	|- ( ph -> Y e. B )
7		rnggrp	|- ( R e. Rng -> R e. Grp )
8	4 7	syl	|- ( ph -> R e. Grp )
9	1 3 8 6	grpinvcld	|- ( ph -> ( N ` Y ) e. B )
10	1 2 3 4 5 9	rngmneg1	|- ( ph -> ( ( N ` X ) .x. ( N ` Y ) ) = ( N ` ( X .x. ( N ` Y ) ) ) )
11	1 2 3 4 5 6	rngmneg2	|- ( ph -> ( X .x. ( N ` Y ) ) = ( N ` ( X .x. Y ) ) )
12	11	fveq2d	|- ( ph -> ( N ` ( X .x. ( N ` Y ) ) ) = ( N ` ( N ` ( X .x. Y ) ) ) )
13	1 2	rngcl	|- ( ( R e. Rng /\ X e. B /\ Y e. B ) -> ( X .x. Y ) e. B )
14	4 5 6 13	syl3anc	|- ( ph -> ( X .x. Y ) e. B )
15	1 3	grpinvinv	|- ( ( R e. Grp /\ ( X .x. Y ) e. B ) -> ( N ` ( N ` ( X .x. Y ) ) ) = ( X .x. Y ) )
16	8 14 15	syl2anc	|- ( ph -> ( N ` ( N ` ( X .x. Y ) ) ) = ( X .x. Y ) )
17	10 12 16	3eqtrd	|- ( ph -> ( ( N ` X ) .x. ( N ` Y ) ) = ( X .x. Y ) )