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 = ( ℩ 𝑒 ( 𝑒 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑒 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑒 ) = 𝑥 ) ) )