rngonegmn1r

Description: Negation in a ring is the same as right multiplication by -u 1 . (Contributed by Jeff Madsen, 19-Jun-2010)

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

Proof

Step	Hyp	Ref	Expression
1		ringneg.1	$⊢ G = 1^{st} (R)$
2		ringneg.2	$⊢ H = 2^{nd} (R)$
3		ringneg.3	$⊢ X = ran G$
4		ringneg.4	$⊢ N = inv (G)$
5		ringneg.5	$⊢ U = GId (H)$
6	1	rneqi	$⊢ ran G = ran 1^{st} (R)$
7	3 6	eqtri	$⊢ X = ran 1^{st} (R)$
8	7 2 5	rngo1cl	$⊢ R \in RingOps \to U \in X$
9	1 3 4	rngonegcl	$⊢ (R \in RingOps \land U \in X) \to N (U) \in X$
10	8 9	mpdan	$⊢ R \in RingOps \to N (U) \in X$
11	10	adantr	$⊢ (R \in RingOps \land A \in X) \to N (U) \in X$
12	8	adantr	$⊢ (R \in RingOps \land A \in X) \to U \in X$
13	11 12	jca	$⊢ (R \in RingOps \land A \in X) \to (N (U) \in X \land U \in X)$
14	1 2 3	rngodi	$⊢ (R \in RingOps \land (A \in X \land N (U) \in X \land U \in X)) \to A H (N (U) G U) = (A H N (U)) G (A H U)$
15	14	3exp2	$⊢ R \in RingOps \to (A \in X \to (N (U) \in X \to (U \in X \to A H (N (U) G U) = (A H N (U)) G (A H U))))$
16	15	imp43	$⊢ ((R \in RingOps \land A \in X) \land (N (U) \in X \land U \in X)) \to A H (N (U) G U) = (A H N (U)) G (A H U)$
17	13 16	mpdan	$⊢ (R \in RingOps \land A \in X) \to A H (N (U) G U) = (A H N (U)) G (A H U)$
18		eqid	$⊢ GId (G) = GId (G)$
19	1 3 4 18	rngoaddneg2	$⊢ (R \in RingOps \land U \in X) \to N (U) G U = GId (G)$
20	8 19	mpdan	$⊢ R \in RingOps \to N (U) G U = GId (G)$
21	20	adantr	$⊢ (R \in RingOps \land A \in X) \to N (U) G U = GId (G)$
22	21	oveq2d	$⊢ (R \in RingOps \land A \in X) \to A H (N (U) G U) = A H GId (G)$
23	18 3 1 2	rngorz	$⊢ (R \in RingOps \land A \in X) \to A H GId (G) = GId (G)$
24	22 23	eqtrd	$⊢ (R \in RingOps \land A \in X) \to A H (N (U) G U) = GId (G)$
25	2 7 5	rngoridm	$⊢ (R \in RingOps \land A \in X) \to A H U = A$
26	25	oveq2d	$⊢ (R \in RingOps \land A \in X) \to (A H N (U)) G (A H U) = (A H N (U)) G A$
27	17 24 26	3eqtr3rd	$⊢ (R \in RingOps \land A \in X) \to (A H N (U)) G A = GId (G)$
28	1 2 3	rngocl	$⊢ (R \in RingOps \land A \in X \land N (U) \in X) \to A H N (U) \in X$
29	11 28	mpd3an3	$⊢ (R \in RingOps \land A \in X) \to A H N (U) \in X$
30	1	rngogrpo	$⊢ R \in RingOps \to G \in GrpOp$
31	3 18 4	grpoinvid2	$⊢ (G \in GrpOp \land A \in X \land A H N (U) \in X) \to (N (A) = A H N (U) \leftrightarrow (A H N (U)) G A = GId (G))$
32	30 31	syl3an1	$⊢ (R \in RingOps \land A \in X \land A H N (U) \in X) \to (N (A) = A H N (U) \leftrightarrow (A H N (U)) G A = GId (G))$
33	29 32	mpd3an3	$⊢ (R \in RingOps \land A \in X) \to (N (A) = A H N (U) \leftrightarrow (A H N (U)) G A = GId (G))$
34	27 33	mpbird	$⊢ (R \in RingOps \land A \in X) \to N (A) = A H N (U)$

Metamath Proof Explorer

Theorem rngonegmn1r

Proof