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

Metamath Proof Explorer

Theorem grpidinv2

Description: A group's properties using the explicit identity element. (Contributed by NM, 5-Feb-2010) (Revised by AV, 1-Sep-2021)

		Ref	Expression
	Hypotheses	grplrinv.b	$⊢ B = {Base}_{G}$
		grplrinv.p	$⊢ \underset{˙}{+} = +_{G}$
		grplrinv.i	$⊢ \underset{˙}{0} = 0_{G}$
	Assertion	grpidinv2	$⊢ (G \in Grp \land A \in B) \to ((\underset{˙}{0} \underset{˙}{+} A = A \land A \underset{˙}{+} \underset{˙}{0} = A) \land \exists y \in B (y \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} y = \underset{˙}{0}))$

Proof

Step	Hyp	Ref	Expression
1		grplrinv.b	$⊢ B = {Base}_{G}$
2		grplrinv.p	$⊢ \underset{˙}{+} = +_{G}$
3		grplrinv.i	$⊢ \underset{˙}{0} = 0_{G}$
4	1 2 3	grplid	$⊢ (G \in Grp \land A \in B) \to \underset{˙}{0} \underset{˙}{+} A = A$
5	1 2 3	grprid	$⊢ (G \in Grp \land A \in B) \to A \underset{˙}{+} \underset{˙}{0} = A$
6	1 2 3	grplrinv	$⊢ G \in Grp \to \forall z \in B \exists y \in B (y \underset{˙}{+} z = \underset{˙}{0} \land z \underset{˙}{+} y = \underset{˙}{0})$
7		oveq2	$⊢ z = A \to y \underset{˙}{+} z = y \underset{˙}{+} A$
8	7	eqeq1d	$⊢ z = A \to (y \underset{˙}{+} z = \underset{˙}{0} \leftrightarrow y \underset{˙}{+} A = \underset{˙}{0})$
9		oveq1	$⊢ z = A \to z \underset{˙}{+} y = A \underset{˙}{+} y$
10	9	eqeq1d	$⊢ z = A \to (z \underset{˙}{+} y = \underset{˙}{0} \leftrightarrow A \underset{˙}{+} y = \underset{˙}{0})$
11	8 10	anbi12d	$⊢ z = A \to ((y \underset{˙}{+} z = \underset{˙}{0} \land z \underset{˙}{+} y = \underset{˙}{0}) \leftrightarrow (y \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} y = \underset{˙}{0}))$
12	11	rexbidv	$⊢ z = A \to (\exists y \in B (y \underset{˙}{+} z = \underset{˙}{0} \land z \underset{˙}{+} y = \underset{˙}{0}) \leftrightarrow \exists y \in B (y \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} y = \underset{˙}{0}))$
13	12	rspcv	$⊢ A \in B \to (\forall z \in B \exists y \in B (y \underset{˙}{+} z = \underset{˙}{0} \land z \underset{˙}{+} y = \underset{˙}{0}) \to \exists y \in B (y \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} y = \underset{˙}{0}))$
14	6 13	mpan9	$⊢ (G \in Grp \land A \in B) \to \exists y \in B (y \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} y = \underset{˙}{0})$
15	4 5 14	jca31	$⊢ (G \in Grp \land A \in B) \to ((\underset{˙}{0} \underset{˙}{+} A = A \land A \underset{˙}{+} \underset{˙}{0} = A) \land \exists y \in B (y \underset{˙}{+} A = \underset{˙}{0} \land A \underset{˙}{+} y = \underset{˙}{0}))$