grpidd

Description: Deduce the identity element of a magma from its properties. (Contributed by Mario Carneiro, 6-Jan-2015)

	Ref	Expression
Hypotheses	grpidd.b	$⊢ φ \to B = {Base}_{G}$
	grpidd.p	$⊢ φ \to \underset{˙}{+} = +_{G}$
	grpidd.z	$⊢ φ \to \underset{˙}{0} \in B$
	grpidd.i	$⊢ (φ \land x \in B) \to \underset{˙}{0} \underset{˙}{+} x = x$
	grpidd.j	$⊢ (φ \land x \in B) \to x \underset{˙}{+} \underset{˙}{0} = x$
Assertion	grpidd	$⊢ φ \to \underset{˙}{0} = 0_{G}$

Step	Hyp	Ref	Expression
1		grpidd.b	$⊢ φ \to B = {Base}_{G}$
2		grpidd.p	$⊢ φ \to \underset{˙}{+} = +_{G}$
3		grpidd.z	$⊢ φ \to \underset{˙}{0} \in B$
4		grpidd.i	$⊢ (φ \land x \in B) \to \underset{˙}{0} \underset{˙}{+} x = x$
5		grpidd.j	$⊢ (φ \land x \in B) \to x \underset{˙}{+} \underset{˙}{0} = x$
6		eqid	$⊢ {Base}_{G} = {Base}_{G}$
7		eqid	$⊢ 0_{G} = 0_{G}$
8		eqid	$⊢ +_{G} = +_{G}$
9	3 1	eleqtrd	$⊢ φ \to \underset{˙}{0} \in {Base}_{G}$
10	1	eleq2d	$⊢ φ \to (x \in B \leftrightarrow x \in {Base}_{G})$
11	10	biimpar	$⊢ (φ \land x \in {Base}_{G}) \to x \in B$
12	2	adantr	$⊢ (φ \land x \in B) \to \underset{˙}{+} = +_{G}$
13	12	oveqd	$⊢ (φ \land x \in B) \to \underset{˙}{0} \underset{˙}{+} x = \underset{˙}{0} +_{G} x$
14	13 4	eqtr3d	$⊢ (φ \land x \in B) \to \underset{˙}{0} +_{G} x = x$
15	11 14	syldan	$⊢ (φ \land x \in {Base}_{G}) \to \underset{˙}{0} +_{G} x = x$
16	12	oveqd	$⊢ (φ \land x \in B) \to x \underset{˙}{+} \underset{˙}{0} = x +_{G} \underset{˙}{0}$
17	16 5	eqtr3d	$⊢ (φ \land x \in B) \to x +_{G} \underset{˙}{0} = x$
18	11 17	syldan	$⊢ (φ \land x \in {Base}_{G}) \to x +_{G} \underset{˙}{0} = x$
19	6 7 8 9 15 18	ismgmid2	$⊢ φ \to \underset{˙}{0} = 0_{G}$

Metamath Proof Explorer