rngoneglmul

Description: Negation of a product in a ring. (Contributed by Jeff Madsen, 19-Jun-2010)

	Ref	Expression
Hypotheses	ringnegmul.1	$⊢ G = 1^{st} (R)$
	ringnegmul.2	$⊢ H = 2^{nd} (R)$
	ringnegmul.3	$⊢ X = ran G$
	ringnegmul.4	$⊢ N = inv (G)$
Assertion	rngoneglmul	$⊢ (R \in RingOps \land A \in X \land B \in X) \to N (A H B) = N (A) H B$

Proof

Step	Hyp	Ref	Expression
1		ringnegmul.1	$⊢ G = 1^{st} (R)$
2		ringnegmul.2	$⊢ H = 2^{nd} (R)$
3		ringnegmul.3	$⊢ X = ran G$
4		ringnegmul.4	$⊢ N = inv (G)$
5	1	rneqi	$⊢ ran G = ran 1^{st} (R)$
6	3 5	eqtri	$⊢ X = ran 1^{st} (R)$
7		eqid	$⊢ GId (H) = GId (H)$
8	6 2 7	rngo1cl	$⊢ R \in RingOps \to GId (H) \in X$
9	1 3 4	rngonegcl	$⊢ (R \in RingOps \land GId (H) \in X) \to N (GId (H)) \in X$
10	8 9	mpdan	$⊢ R \in RingOps \to N (GId (H)) \in X$
11	1 2 3	rngoass	$⊢ (R \in RingOps \land (N (GId (H)) \in X \land A \in X \land B \in X)) \to (N (GId (H)) H A) H B = N (GId (H)) H (A H B)$
12	11	3exp2	$⊢ R \in RingOps \to (N (GId (H)) \in X \to (A \in X \to (B \in X \to (N (GId (H)) H A) H B = N (GId (H)) H (A H B))))$
13	10 12	mpd	$⊢ R \in RingOps \to (A \in X \to (B \in X \to (N (GId (H)) H A) H B = N (GId (H)) H (A H B)))$
14	13	3imp	$⊢ (R \in RingOps \land A \in X \land B \in X) \to (N (GId (H)) H A) H B = N (GId (H)) H (A H B)$
15	1 2 3 4 7	rngonegmn1l	$⊢ (R \in RingOps \land A \in X) \to N (A) = N (GId (H)) H A$
16	15	3adant3	$⊢ (R \in RingOps \land A \in X \land B \in X) \to N (A) = N (GId (H)) H A$
17	16	oveq1d	$⊢ (R \in RingOps \land A \in X \land B \in X) \to N (A) H B = (N (GId (H)) H A) H B$
18	1 2 3	rngocl	$⊢ (R \in RingOps \land A \in X \land B \in X) \to A H B \in X$
19	18	3expb	$⊢ (R \in RingOps \land (A \in X \land B \in X)) \to A H B \in X$
20	1 2 3 4 7	rngonegmn1l	$⊢ (R \in RingOps \land A H B \in X) \to N (A H B) = N (GId (H)) H (A H B)$
21	19 20	syldan	$⊢ (R \in RingOps \land (A \in X \land B \in X)) \to N (A H B) = N (GId (H)) H (A H B)$
22	21	3impb	$⊢ (R \in RingOps \land A \in X \land B \in X) \to N (A H B) = N (GId (H)) H (A H B)$
23	14 17 22	3eqtr4rd	$⊢ (R \in RingOps \land A \in X \land B \in X) \to N (A H B) = N (A) H B$

Metamath Proof Explorer

Theorem rngoneglmul

Proof