This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 0g0

Description: The identity element function evaluates to the empty set on an empty structure. (Contributed by Stefan O'Rear, 2-Oct-2015)

Ref Expression
Assertion 0g0 ∅ = ( 0g ‘ ∅ )

Proof

Step Hyp Ref Expression
1 base0 ⊢ ∅ = ( Base ‘ ∅ )
2 eqid ⊢ ( +g ‘ ∅ ) = ( +g ‘ ∅ )
3 eqid ⊢ ( 0g ‘ ∅ ) = ( 0g ‘ ∅ )
4 1 2 3 grpidval ⊢ ( 0g ‘ ∅ ) = ( ℩ 𝑒 ( 𝑒 ∈ ∅ ∧ ∀ 𝑥 ∈ ∅ ( ( 𝑒 ( +g ‘ ∅ ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ ∅ ) 𝑒 ) = 𝑥 ) ) )
5 noel ⊢ ¬ 𝑒 ∈ ∅
6 5 intnanr ⊢ ¬ ( 𝑒 ∈ ∅ ∧ ∀ 𝑥 ∈ ∅ ( ( 𝑒 ( +g ‘ ∅ ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ ∅ ) 𝑒 ) = 𝑥 ) )
7 6 nex ⊢ ¬ ∃ 𝑒 ( 𝑒 ∈ ∅ ∧ ∀ 𝑥 ∈ ∅ ( ( 𝑒 ( +g ‘ ∅ ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ ∅ ) 𝑒 ) = 𝑥 ) )
8 euex ⊢ ( ∃! 𝑒 ( 𝑒 ∈ ∅ ∧ ∀ 𝑥 ∈ ∅ ( ( 𝑒 ( +g ‘ ∅ ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ ∅ ) 𝑒 ) = 𝑥 ) ) → ∃ 𝑒 ( 𝑒 ∈ ∅ ∧ ∀ 𝑥 ∈ ∅ ( ( 𝑒 ( +g ‘ ∅ ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ ∅ ) 𝑒 ) = 𝑥 ) ) )
9 7 8 mto ⊢ ¬ ∃! 𝑒 ( 𝑒 ∈ ∅ ∧ ∀ 𝑥 ∈ ∅ ( ( 𝑒 ( +g ‘ ∅ ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ ∅ ) 𝑒 ) = 𝑥 ) )
10 iotanul ⊢ ( ¬ ∃! 𝑒 ( 𝑒 ∈ ∅ ∧ ∀ 𝑥 ∈ ∅ ( ( 𝑒 ( +g ‘ ∅ ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ ∅ ) 𝑒 ) = 𝑥 ) ) → ( ℩ 𝑒 ( 𝑒 ∈ ∅ ∧ ∀ 𝑥 ∈ ∅ ( ( 𝑒 ( +g ‘ ∅ ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ ∅ ) 𝑒 ) = 𝑥 ) ) ) = ∅ )
11 9 10 ax-mp ⊢ ( ℩ 𝑒 ( 𝑒 ∈ ∅ ∧ ∀ 𝑥 ∈ ∅ ( ( 𝑒 ( +g ‘ ∅ ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ ∅ ) 𝑒 ) = 𝑥 ) ) ) = ∅
12 4 11 eqtr2i ⊢ ∅ = ( 0g ‘ ∅ )