This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isunit3

Description: Alternate definition of being a unit. (Contributed by Thierry Arnoux, 3-Aug-2025)

		Ref	Expression
	Hypotheses	isunit2.b	$⊢ B = {Base}_{R}$
		isunit2.u	$⊢ U = Unit (R)$
		isunit2.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
		isunit2.1	$⊢ \underset{˙}{1} = 1_{R}$
		isunit3.x	$⊢ φ \to X \in B$
		isunit3.r	$⊢ φ \to R \in Ring$
	Assertion	isunit3	$⊢ φ \to (X \in U \leftrightarrow \exists y \in B (X \underset{˙}{\cdot} y = \underset{˙}{1} \land y \underset{˙}{\cdot} X = \underset{˙}{1}))$

Proof

Step	Hyp	Ref	Expression
1		isunit2.b	$⊢ B = {Base}_{R}$
2		isunit2.u	$⊢ U = Unit (R)$
3		isunit2.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		isunit2.1	$⊢ \underset{˙}{1} = 1_{R}$
5		isunit3.x	$⊢ φ \to X \in B$
6		isunit3.r	$⊢ φ \to R \in Ring$
7	1 2 3 4	isunit2	$⊢ X \in U \leftrightarrow (X \in B \land (\exists u \in B X \underset{˙}{\cdot} u = \underset{˙}{1} \land \exists v \in B v \underset{˙}{\cdot} X = \underset{˙}{1}))$
8	5	biantrurd	$⊢ φ \to ((\exists u \in B X \underset{˙}{\cdot} u = \underset{˙}{1} \land \exists v \in B v \underset{˙}{\cdot} X = \underset{˙}{1}) \leftrightarrow (X \in B \land (\exists u \in B X \underset{˙}{\cdot} u = \underset{˙}{1} \land \exists v \in B v \underset{˙}{\cdot} X = \underset{˙}{1})))$
9	7 8	bitr4id	$⊢ φ \to (X \in U \leftrightarrow (\exists u \in B X \underset{˙}{\cdot} u = \underset{˙}{1} \land \exists v \in B v \underset{˙}{\cdot} X = \underset{˙}{1}))$
10		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
11	10 1	mgpbas	$⊢ B = {Base}_{{mulGrp}_{R}}$
12	10 4	ringidval	$⊢ \underset{˙}{1} = 0_{{mulGrp}_{R}}$
13	10 3	mgpplusg	$⊢ \underset{˙}{\cdot} = +_{{mulGrp}_{R}}$
14	10	ringmgp	$⊢ R \in Ring \to {mulGrp}_{R} \in Mnd$
15	6 14	syl	$⊢ φ \to {mulGrp}_{R} \in Mnd$
16	11 12 13 15 5	mndlrinvb	$⊢ φ \to ((\exists u \in B X \underset{˙}{\cdot} u = \underset{˙}{1} \land \exists v \in B v \underset{˙}{\cdot} X = \underset{˙}{1}) \leftrightarrow \exists y \in B (X \underset{˙}{\cdot} y = \underset{˙}{1} \land y \underset{˙}{\cdot} X = \underset{˙}{1}))$
17	9 16	bitrd	$⊢ φ \to (X \in U \leftrightarrow \exists y \in B (X \underset{˙}{\cdot} y = \underset{˙}{1} \land y \underset{˙}{\cdot} X = \underset{˙}{1}))$