rngonegrmul

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	rngonegrmul	$⊢ (R \in RingOps \land A \in X \land B \in X) \to N (A H B) = A H N (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 (A \in X \land B \in X \land N (GId (H)) \in X)) \to (A H B) H N (GId (H)) = A H (B H N (GId (H)))$
12	11	3exp2	$⊢ R \in RingOps \to (A \in X \to (B \in X \to (N (GId (H)) \in X \to (A H B) H N (GId (H)) = A H (B H N (GId (H))))))$
13	12	com24	$⊢ R \in RingOps \to (N (GId (H)) \in X \to (B \in X \to (A \in X \to (A H B) H N (GId (H)) = A H (B H N (GId (H))))))$
14	13	com34	$⊢ R \in RingOps \to (N (GId (H)) \in X \to (A \in X \to (B \in X \to (A H B) H N (GId (H)) = A H (B H N (GId (H))))))$
15	10 14	mpd	$⊢ R \in RingOps \to (A \in X \to (B \in X \to (A H B) H N (GId (H)) = A H (B H N (GId (H)))))$
16	15	3imp	$⊢ (R \in RingOps \land A \in X \land B \in X) \to (A H B) H N (GId (H)) = A H (B H N (GId (H)))$
17	1 2 3	rngocl	$⊢ (R \in RingOps \land A \in X \land B \in X) \to A H B \in X$
18	17	3expb	$⊢ (R \in RingOps \land (A \in X \land B \in X)) \to A H B \in X$
19	1 2 3 4 7	rngonegmn1r	$⊢ (R \in RingOps \land A H B \in X) \to N (A H B) = (A H B) H N (GId (H))$
20	18 19	syldan	$⊢ (R \in RingOps \land (A \in X \land B \in X)) \to N (A H B) = (A H B) H N (GId (H))$
21	20	3impb	$⊢ (R \in RingOps \land A \in X \land B \in X) \to N (A H B) = (A H B) H N (GId (H))$
22	1 2 3 4 7	rngonegmn1r	$⊢ (R \in RingOps \land B \in X) \to N (B) = B H N (GId (H))$
23	22	3adant2	$⊢ (R \in RingOps \land A \in X \land B \in X) \to N (B) = B H N (GId (H))$
24	23	oveq2d	$⊢ (R \in RingOps \land A \in X \land B \in X) \to A H N (B) = A H (B H N (GId (H)))$
25	16 21 24	3eqtr4d	$⊢ (R \in RingOps \land A \in X \land B \in X) \to N (A H B) = A H N (B)$

Metamath Proof Explorer

Theorem rngonegrmul

Proof