Theorem ringm2neg

Description: Double negation of a product in a ring. ( mul2neg analog.) (Contributed by Mario Carneiro, 4-Dec-2014)

	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		ringgrp	|- ( R e. Ring -> R e. Grp )
8	4 7	syl	|- ( ph -> R e. Grp )
9	1 3	grpinvcl	|- ( ( R e. Grp /\ Y e. B ) -> ( N ` Y ) e. B )
10	8 6 9	syl2anc	|- ( ph -> ( N ` Y ) e. B )
11	1 2 3 4 5 10	ringmneg1	|- ( ph -> ( ( N ` X ) .x. ( N ` Y ) ) = ( N ` ( X .x. ( N ` Y ) ) ) )
12	1 2 3 4 5 6	ringmneg2	|- ( ph -> ( X .x. ( N ` Y ) ) = ( N ` ( X .x. Y ) ) )
13	12	fveq2d	|- ( ph -> ( N ` ( X .x. ( N ` Y ) ) ) = ( N ` ( N ` ( X .x. Y ) ) ) )
14	1 2	ringcl	|- ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( X .x. Y ) e. B )
15	4 5 6 14	syl3anc	|- ( ph -> ( X .x. Y ) e. B )
16	1 3	grpinvinv	|- ( ( R e. Grp /\ ( X .x. Y ) e. B ) -> ( N ` ( N ` ( X .x. Y ) ) ) = ( X .x. Y ) )
17	8 15 16	syl2anc	|- ( ph -> ( N ` ( N ` ( X .x. Y ) ) ) = ( X .x. Y ) )
18	11 13 17	3eqtrd	|- ( ph -> ( ( N ` X ) .x. ( N ` Y ) ) = ( X .x. Y ) )