unitlinv

Description: A unit times its inverse is the identity. (Contributed by Mario Carneiro, 2-Dec-2014)

	Ref	Expression
Hypotheses	unitinvcl.1	$⊢ U = Unit (R)$
	unitinvcl.2	$⊢ I = {inv}_{r} (R)$
	unitinvcl.3	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	unitinvcl.4	$⊢ \underset{˙}{1} = 1_{R}$
Assertion	unitlinv	$⊢ (R \in Ring \land X \in U) \to I (X) \underset{˙}{\cdot} X = \underset{˙}{1}$

Step	Hyp	Ref	Expression
1		unitinvcl.1	$⊢ U = Unit (R)$
2		unitinvcl.2	$⊢ I = {inv}_{r} (R)$
3		unitinvcl.3	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		unitinvcl.4	$⊢ \underset{˙}{1} = 1_{R}$
5		eqid	$⊢ {mulGrp}_{R} ↾_{𝑠} U = {mulGrp}_{R} ↾_{𝑠} U$
6	1 5	unitgrp	$⊢ R \in Ring \to {mulGrp}_{R} ↾_{𝑠} U \in Grp$
7	1 5	unitgrpbas	$⊢ U = {Base}_{({mulGrp}_{R} ↾_{𝑠} U)}$
8	1	fvexi	$⊢ U \in V$
9		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
10	9 3	mgpplusg	$⊢ \underset{˙}{\cdot} = +_{{mulGrp}_{R}}$
11	5 10	ressplusg	$⊢ U \in V \to \underset{˙}{\cdot} = +_{({mulGrp}_{R} ↾_{𝑠} U)}$
12	8 11	ax-mp	$⊢ \underset{˙}{\cdot} = +_{({mulGrp}_{R} ↾_{𝑠} U)}$
13		eqid	$⊢ 0_{({mulGrp}_{R} ↾_{𝑠} U)} = 0_{({mulGrp}_{R} ↾_{𝑠} U)}$
14	1 5 2	invrfval	$⊢ I = {inv}_{g} ({mulGrp}_{R} ↾_{𝑠} U)$
15	7 12 13 14	grplinv	$⊢ ({mulGrp}_{R} ↾_{𝑠} U \in Grp \land X \in U) \to I (X) \underset{˙}{\cdot} X = 0_{({mulGrp}_{R} ↾_{𝑠} U)}$
16	6 15	sylan	$⊢ (R \in Ring \land X \in U) \to I (X) \underset{˙}{\cdot} X = 0_{({mulGrp}_{R} ↾_{𝑠} U)}$
17	1 5 4	unitgrpid	$⊢ R \in Ring \to \underset{˙}{1} = 0_{({mulGrp}_{R} ↾_{𝑠} U)}$
18	17	adantr	$⊢ (R \in Ring \land X \in U) \to \underset{˙}{1} = 0_{({mulGrp}_{R} ↾_{𝑠} U)}$
19	16 18	eqtr4d	$⊢ (R \in Ring \land X \in U) \to I (X) \underset{˙}{\cdot} X = \underset{˙}{1}$

Metamath Proof Explorer