Theorem odeq1

Description: The group identity is the unique element of a group with order one. (Contributed by Mario Carneiro, 14-Jan-2015) (Revised by Mario Carneiro, 23-Sep-2015)

	Ref	Expression
Hypotheses	od1.1	$$⊢O=\mathrm{od}\left(G\right)$$
	od1.2	$$⊢\underset{\dot{}}{0}=0_G$$
	odeq1.3	$$⊢X={\mathrm{Base}}_G$$
Assertion	odeq1	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\right)\to \left(O\left(A\right)=1\leftrightarrow A=\underset{\dot{}}{0}\right)$$

Proof

Step	Hyp	Ref	Expression
1		od1.1	$$⊢O=\mathrm{od}\left(G\right)$$
2		od1.2	$$⊢\underset{\dot{}}{0}=0_G$$
3		odeq1.3	$$⊢X={\mathrm{Base}}_G$$
4		oveq1	$$⊢O\left(A\right)=1\to O\left(A\right){\cdot }_{G}A=1{\cdot }_{G}A$$
5	4	eqcomd	$$⊢O\left(A\right)=1\to 1{\cdot }_{G}A=O\left(A\right){\cdot }_{G}A$$
6		eqid	$$⊢{\cdot }_G={\cdot }_G$$
7	3 6	mulg1	$$⊢A\in X\to 1{\cdot }_{G}A=A$$
8	3 1 6 2	odid	$$⊢A\in X\to O\left(A\right){\cdot }_{G}A=\underset{\dot{}}{0}$$
9	7 8	eqeq12d	$$⊢A\in X\to \left(1{\cdot }_{G}A=O\left(A\right){\cdot }_{G}A\leftrightarrow A=\underset{\dot{}}{0}\right)$$
10	9	adantl	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\right)\to \left(1{\cdot }_{G}A=O\left(A\right){\cdot }_{G}A\leftrightarrow A=\underset{\dot{}}{0}\right)$$
11	5 10	syl5ib	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\right)\to \left(O\left(A\right)=1\to A=\underset{\dot{}}{0}\right)$$
12	1 2	od1	$$⊢G\in \mathrm{Grp}\to O\left(\underset{\dot{}}{0}\right)=1$$
13	12	adantr	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\right)\to O\left(\underset{\dot{}}{0}\right)=1$$
14		fveqeq2	$$⊢A=\underset{\dot{}}{0}\to \left(O\left(A\right)=1\leftrightarrow O\left(\underset{\dot{}}{0}\right)=1\right)$$
15	13 14	syl5ibrcom	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\right)\to \left(A=\underset{\dot{}}{0}\to O\left(A\right)=1\right)$$
16	11 15	impbid	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\right)\to \left(O\left(A\right)=1\leftrightarrow A=\underset{\dot{}}{0}\right)$$