invginvrid

Description: Identity for a multiplication with additive and multiplicative inverses in a ring. (Contributed by AV, 18-May-2018)

	Ref	Expression
Hypotheses	invginvrid.b	$⊢ B = {Base}_{R}$
	invginvrid.u	$⊢ U = Unit (R)$
	invginvrid.n	$⊢ N = {inv}_{g} (R)$
	invginvrid.i	$⊢ I = {inv}_{r} (R)$
	invginvrid.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	invginvrid	$⊢ (R \in Ring \land X \in B \land Y \in U) \to N (Y) \underset{˙}{\cdot} (I (N (Y)) \underset{˙}{\cdot} X) = X$

Proof

Step	Hyp	Ref	Expression
1		invginvrid.b	$⊢ B = {Base}_{R}$
2		invginvrid.u	$⊢ U = Unit (R)$
3		invginvrid.n	$⊢ N = {inv}_{g} (R)$
4		invginvrid.i	$⊢ I = {inv}_{r} (R)$
5		invginvrid.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
6		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
7	6	ringmgp	$⊢ R \in Ring \to {mulGrp}_{R} \in Mnd$
8	7	3ad2ant1	$⊢ (R \in Ring \land X \in B \land Y \in U) \to {mulGrp}_{R} \in Mnd$
9		ringgrp	$⊢ R \in Ring \to R \in Grp$
10	1 2	unitcl	$⊢ Y \in U \to Y \in B$
11	1 3	grpinvcl	$⊢ (R \in Grp \land Y \in B) \to N (Y) \in B$
12	9 10 11	syl2an	$⊢ (R \in Ring \land Y \in U) \to N (Y) \in B$
13	12	3adant2	$⊢ (R \in Ring \land X \in B \land Y \in U) \to N (Y) \in B$
14	2 3	unitnegcl	$⊢ (R \in Ring \land Y \in U) \to N (Y) \in U$
15	2 4 1	ringinvcl	$⊢ (R \in Ring \land N (Y) \in U) \to I (N (Y)) \in B$
16	14 15	syldan	$⊢ (R \in Ring \land Y \in U) \to I (N (Y)) \in B$
17	16	3adant2	$⊢ (R \in Ring \land X \in B \land Y \in U) \to I (N (Y)) \in B$
18		simp2	$⊢ (R \in Ring \land X \in B \land Y \in U) \to X \in B$
19	6 1	mgpbas	$⊢ B = {Base}_{{mulGrp}_{R}}$
20	6 5	mgpplusg	$⊢ \underset{˙}{\cdot} = +_{{mulGrp}_{R}}$
21	19 20	mndass	$⊢ ({mulGrp}_{R} \in Mnd \land (N (Y) \in B \land I (N (Y)) \in B \land X \in B)) \to (N (Y) \underset{˙}{\cdot} I (N (Y))) \underset{˙}{\cdot} X = N (Y) \underset{˙}{\cdot} (I (N (Y)) \underset{˙}{\cdot} X)$
22	21	eqcomd	$⊢ ({mulGrp}_{R} \in Mnd \land (N (Y) \in B \land I (N (Y)) \in B \land X \in B)) \to N (Y) \underset{˙}{\cdot} (I (N (Y)) \underset{˙}{\cdot} X) = (N (Y) \underset{˙}{\cdot} I (N (Y))) \underset{˙}{\cdot} X$
23	8 13 17 18 22	syl13anc	$⊢ (R \in Ring \land X \in B \land Y \in U) \to N (Y) \underset{˙}{\cdot} (I (N (Y)) \underset{˙}{\cdot} X) = (N (Y) \underset{˙}{\cdot} I (N (Y))) \underset{˙}{\cdot} X$
24		simp1	$⊢ (R \in Ring \land X \in B \land Y \in U) \to R \in Ring$
25	14	3adant2	$⊢ (R \in Ring \land X \in B \land Y \in U) \to N (Y) \in U$
26		eqid	$⊢ 1_{R} = 1_{R}$
27	2 4 5 26	unitrinv	$⊢ (R \in Ring \land N (Y) \in U) \to N (Y) \underset{˙}{\cdot} I (N (Y)) = 1_{R}$
28	24 25 27	syl2anc	$⊢ (R \in Ring \land X \in B \land Y \in U) \to N (Y) \underset{˙}{\cdot} I (N (Y)) = 1_{R}$
29	28	oveq1d	$⊢ (R \in Ring \land X \in B \land Y \in U) \to (N (Y) \underset{˙}{\cdot} I (N (Y))) \underset{˙}{\cdot} X = 1_{R} \underset{˙}{\cdot} X$
30	1 5 26	ringlidm	$⊢ (R \in Ring \land X \in B) \to 1_{R} \underset{˙}{\cdot} X = X$
31	30	3adant3	$⊢ (R \in Ring \land X \in B \land Y \in U) \to 1_{R} \underset{˙}{\cdot} X = X$
32	23 29 31	3eqtrd	$⊢ (R \in Ring \land X \in B \land Y \in U) \to N (Y) \underset{˙}{\cdot} (I (N (Y)) \underset{˙}{\cdot} X) = X$

Metamath Proof Explorer

Theorem invginvrid

Proof