grpidd2

Description: Deduce the identity element of a group from its properties. Useful in conjunction with isgrpd . (Contributed by Mario Carneiro, 14-Jun-2015)

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

Proof

Step	Hyp	Ref	Expression
1		grpidd2.b	$⊢ φ \to B = {Base}_{G}$
2		grpidd2.p	$⊢ φ \to \underset{˙}{+} = +_{G}$
3		grpidd2.z	$⊢ φ \to \underset{˙}{0} \in B$
4		grpidd2.i	$⊢ (φ \land x \in B) \to \underset{˙}{0} \underset{˙}{+} x = x$
5		grpidd2.j	$⊢ φ \to G \in Grp$
6	2	oveqd	$⊢ φ \to \underset{˙}{0} \underset{˙}{+} \underset{˙}{0} = \underset{˙}{0} +_{G} \underset{˙}{0}$
7		oveq2	$⊢ x = \underset{˙}{0} \to \underset{˙}{0} \underset{˙}{+} x = \underset{˙}{0} \underset{˙}{+} \underset{˙}{0}$
8		id	$⊢ x = \underset{˙}{0} \to x = \underset{˙}{0}$
9	7 8	eqeq12d	$⊢ x = \underset{˙}{0} \to (\underset{˙}{0} \underset{˙}{+} x = x \leftrightarrow \underset{˙}{0} \underset{˙}{+} \underset{˙}{0} = \underset{˙}{0})$
10	4	ralrimiva	$⊢ φ \to \forall x \in B \underset{˙}{0} \underset{˙}{+} x = x$
11	9 10 3	rspcdva	$⊢ φ \to \underset{˙}{0} \underset{˙}{+} \underset{˙}{0} = \underset{˙}{0}$
12	6 11	eqtr3d	$⊢ φ \to \underset{˙}{0} +_{G} \underset{˙}{0} = \underset{˙}{0}$
13	3 1	eleqtrd	$⊢ φ \to \underset{˙}{0} \in {Base}_{G}$
14		eqid	$⊢ {Base}_{G} = {Base}_{G}$
15		eqid	$⊢ +_{G} = +_{G}$
16		eqid	$⊢ 0_{G} = 0_{G}$
17	14 15 16	grpid	$⊢ (G \in Grp \land \underset{˙}{0} \in {Base}_{G}) \to (\underset{˙}{0} +_{G} \underset{˙}{0} = \underset{˙}{0} \leftrightarrow 0_{G} = \underset{˙}{0})$
18	5 13 17	syl2anc	$⊢ φ \to (\underset{˙}{0} +_{G} \underset{˙}{0} = \underset{˙}{0} \leftrightarrow 0_{G} = \underset{˙}{0})$
19	12 18	mpbid	$⊢ φ \to 0_{G} = \underset{˙}{0}$
20	19	eqcomd	$⊢ φ \to \underset{˙}{0} = 0_{G}$

Metamath Proof Explorer

Theorem grpidd2

Proof