Metamath Proof Explorer


Theorem grpidval

Description: The value of the identity element of a group. (Contributed by NM, 20-Aug-2011) (Revised by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses grpidval.b 𝐵 = ( Base ‘ 𝐺 )
grpidval.p + = ( +g𝐺 )
grpidval.o 0 = ( 0g𝐺 )
Assertion grpidval 0 = ( ℩ 𝑒 ( 𝑒𝐵 ∧ ∀ 𝑥𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 grpidval.b 𝐵 = ( Base ‘ 𝐺 )
2 grpidval.p + = ( +g𝐺 )
3 grpidval.o 0 = ( 0g𝐺 )
4 fveq2 ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = ( Base ‘ 𝐺 ) )
5 4 1 eqtr4di ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = 𝐵 )
6 5 eleq2d ( 𝑔 = 𝐺 → ( 𝑒 ∈ ( Base ‘ 𝑔 ) ↔ 𝑒𝐵 ) )
7 fveq2 ( 𝑔 = 𝐺 → ( +g𝑔 ) = ( +g𝐺 ) )
8 7 2 eqtr4di ( 𝑔 = 𝐺 → ( +g𝑔 ) = + )
9 8 oveqd ( 𝑔 = 𝐺 → ( 𝑒 ( +g𝑔 ) 𝑥 ) = ( 𝑒 + 𝑥 ) )
10 9 eqeq1d ( 𝑔 = 𝐺 → ( ( 𝑒 ( +g𝑔 ) 𝑥 ) = 𝑥 ↔ ( 𝑒 + 𝑥 ) = 𝑥 ) )
11 8 oveqd ( 𝑔 = 𝐺 → ( 𝑥 ( +g𝑔 ) 𝑒 ) = ( 𝑥 + 𝑒 ) )
12 11 eqeq1d ( 𝑔 = 𝐺 → ( ( 𝑥 ( +g𝑔 ) 𝑒 ) = 𝑥 ↔ ( 𝑥 + 𝑒 ) = 𝑥 ) )
13 10 12 anbi12d ( 𝑔 = 𝐺 → ( ( ( 𝑒 ( +g𝑔 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g𝑔 ) 𝑒 ) = 𝑥 ) ↔ ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) )
14 5 13 raleqbidv ( 𝑔 = 𝐺 → ( ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ( ( 𝑒 ( +g𝑔 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g𝑔 ) 𝑒 ) = 𝑥 ) ↔ ∀ 𝑥𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) )
15 6 14 anbi12d ( 𝑔 = 𝐺 → ( ( 𝑒 ∈ ( Base ‘ 𝑔 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ( ( 𝑒 ( +g𝑔 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g𝑔 ) 𝑒 ) = 𝑥 ) ) ↔ ( 𝑒𝐵 ∧ ∀ 𝑥𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) ) )
16 15 iotabidv ( 𝑔 = 𝐺 → ( ℩ 𝑒 ( 𝑒 ∈ ( Base ‘ 𝑔 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ( ( 𝑒 ( +g𝑔 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g𝑔 ) 𝑒 ) = 𝑥 ) ) ) = ( ℩ 𝑒 ( 𝑒𝐵 ∧ ∀ 𝑥𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) ) )
17 df-0g 0g = ( 𝑔 ∈ V ↦ ( ℩ 𝑒 ( 𝑒 ∈ ( Base ‘ 𝑔 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ( ( 𝑒 ( +g𝑔 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g𝑔 ) 𝑒 ) = 𝑥 ) ) ) )
18 iotaex ( ℩ 𝑒 ( 𝑒𝐵 ∧ ∀ 𝑥𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) ) ∈ V
19 16 17 18 fvmpt ( 𝐺 ∈ V → ( 0g𝐺 ) = ( ℩ 𝑒 ( 𝑒𝐵 ∧ ∀ 𝑥𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) ) )
20 fvprc ( ¬ 𝐺 ∈ V → ( 0g𝐺 ) = ∅ )
21 euex ( ∃! 𝑒 ( 𝑒𝐵 ∧ ∀ 𝑥𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) → ∃ 𝑒 ( 𝑒𝐵 ∧ ∀ 𝑥𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) )
22 n0i ( 𝑒𝐵 → ¬ 𝐵 = ∅ )
23 fvprc ( ¬ 𝐺 ∈ V → ( Base ‘ 𝐺 ) = ∅ )
24 1 23 eqtrid ( ¬ 𝐺 ∈ V → 𝐵 = ∅ )
25 22 24 nsyl2 ( 𝑒𝐵𝐺 ∈ V )
26 25 adantr ( ( 𝑒𝐵 ∧ ∀ 𝑥𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) → 𝐺 ∈ V )
27 26 exlimiv ( ∃ 𝑒 ( 𝑒𝐵 ∧ ∀ 𝑥𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) → 𝐺 ∈ V )
28 21 27 syl ( ∃! 𝑒 ( 𝑒𝐵 ∧ ∀ 𝑥𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) → 𝐺 ∈ V )
29 iotanul ( ¬ ∃! 𝑒 ( 𝑒𝐵 ∧ ∀ 𝑥𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) → ( ℩ 𝑒 ( 𝑒𝐵 ∧ ∀ 𝑥𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) ) = ∅ )
30 28 29 nsyl5 ( ¬ 𝐺 ∈ V → ( ℩ 𝑒 ( 𝑒𝐵 ∧ ∀ 𝑥𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) ) = ∅ )
31 20 30 eqtr4d ( ¬ 𝐺 ∈ V → ( 0g𝐺 ) = ( ℩ 𝑒 ( 𝑒𝐵 ∧ ∀ 𝑥𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) ) )
32 19 31 pm2.61i ( 0g𝐺 ) = ( ℩ 𝑒 ( 𝑒𝐵 ∧ ∀ 𝑥𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) )
33 3 32 eqtri 0 = ( ℩ 𝑒 ( 𝑒𝐵 ∧ ∀ 𝑥𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) )