Metamath Proof Explorer


Theorem grpidd

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

Ref Expression
Hypotheses grpidd.b ( 𝜑𝐵 = ( Base ‘ 𝐺 ) )
grpidd.p ( 𝜑+ = ( +g𝐺 ) )
grpidd.z ( 𝜑0𝐵 )
grpidd.i ( ( 𝜑𝑥𝐵 ) → ( 0 + 𝑥 ) = 𝑥 )
grpidd.j ( ( 𝜑𝑥𝐵 ) → ( 𝑥 + 0 ) = 𝑥 )
Assertion grpidd ( 𝜑0 = ( 0g𝐺 ) )

Proof

Step Hyp Ref Expression
1 grpidd.b ( 𝜑𝐵 = ( Base ‘ 𝐺 ) )
2 grpidd.p ( 𝜑+ = ( +g𝐺 ) )
3 grpidd.z ( 𝜑0𝐵 )
4 grpidd.i ( ( 𝜑𝑥𝐵 ) → ( 0 + 𝑥 ) = 𝑥 )
5 grpidd.j ( ( 𝜑𝑥𝐵 ) → ( 𝑥 + 0 ) = 𝑥 )
6 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
7 eqid ( 0g𝐺 ) = ( 0g𝐺 )
8 eqid ( +g𝐺 ) = ( +g𝐺 )
9 3 1 eleqtrd ( 𝜑0 ∈ ( Base ‘ 𝐺 ) )
10 1 eleq2d ( 𝜑 → ( 𝑥𝐵𝑥 ∈ ( Base ‘ 𝐺 ) ) )
11 10 biimpar ( ( 𝜑𝑥 ∈ ( Base ‘ 𝐺 ) ) → 𝑥𝐵 )
12 2 adantr ( ( 𝜑𝑥𝐵 ) → + = ( +g𝐺 ) )
13 12 oveqd ( ( 𝜑𝑥𝐵 ) → ( 0 + 𝑥 ) = ( 0 ( +g𝐺 ) 𝑥 ) )
14 13 4 eqtr3d ( ( 𝜑𝑥𝐵 ) → ( 0 ( +g𝐺 ) 𝑥 ) = 𝑥 )
15 11 14 syldan ( ( 𝜑𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( 0 ( +g𝐺 ) 𝑥 ) = 𝑥 )
16 12 oveqd ( ( 𝜑𝑥𝐵 ) → ( 𝑥 + 0 ) = ( 𝑥 ( +g𝐺 ) 0 ) )
17 16 5 eqtr3d ( ( 𝜑𝑥𝐵 ) → ( 𝑥 ( +g𝐺 ) 0 ) = 𝑥 )
18 11 17 syldan ( ( 𝜑𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑥 ( +g𝐺 ) 0 ) = 𝑥 )
19 6 7 8 9 15 18 ismgmid2 ( 𝜑0 = ( 0g𝐺 ) )