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

Metamath Proof Explorer

Theorem mgmidsssn0

Description: Property of the set of identities of G . Either G has no identities, and O = (/) , or it has one and this identity is unique and identified by the 0g function. (Contributed by Mario Carneiro, 7-Dec-2014)

Ref Expression
Hypotheses mgmidsssn0.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
mgmidsssn0.z ⊢ 0 = ( 0g ‘ 𝐺 )
mgmidsssn0.p ⊢ + = ( +g ‘ 𝐺 )
mgmidsssn0.o ⊢ 𝑂 = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) }
Assertion mgmidsssn0 ( 𝐺 ∈ 𝑉 → 𝑂 ⊆ { 0 } )

Proof

Step Hyp Ref Expression
1 mgmidsssn0.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 mgmidsssn0.z ⊢ 0 = ( 0g ‘ 𝐺 )
3 mgmidsssn0.p ⊢ + = ( +g ‘ 𝐺 )
4 mgmidsssn0.o ⊢ 𝑂 = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) }
5 simpr ⊢ ( ( 𝐺 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) ) ) → ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) ) )
6 oveq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 + 𝑦 ) = ( 𝑥 + 𝑦 ) )
7 6 eqeq1d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑧 + 𝑦 ) = 𝑦 ↔ ( 𝑥 + 𝑦 ) = 𝑦 ) )
8 7 ovanraleqv ⊢ ( 𝑧 = 𝑥 → ( ∀ 𝑦 ∈ 𝐵 ( ( 𝑧 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑧 ) = 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) ) )
9 8 rspcev ⊢ ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) ) → ∃ 𝑧 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑧 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑧 ) = 𝑦 ) )
10 9 adantl ⊢ ( ( 𝐺 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) ) ) → ∃ 𝑧 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑧 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑧 ) = 𝑦 ) )
11 1 2 3 10 ismgmid ⊢ ( ( 𝐺 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) ) ) → ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) ) ↔ 0 = 𝑥 ) )
12 5 11 mpbid ⊢ ( ( 𝐺 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) ) ) → 0 = 𝑥 )
13 12 eqcomd ⊢ ( ( 𝐺 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) ) ) → 𝑥 = 0 )
14 velsn ⊢ ( 𝑥 ∈ { 0 } ↔ 𝑥 = 0 )
15 13 14 sylibr ⊢ ( ( 𝐺 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) ) ) → 𝑥 ∈ { 0 } )
16 15 expr ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ) → ( ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) → 𝑥 ∈ { 0 } ) )
17 16 ralrimiva ⊢ ( 𝐺 ∈ 𝑉 → ∀ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) → 𝑥 ∈ { 0 } ) )
18 rabss ⊢ ( { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ⊆ { 0 } ↔ ∀ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) → 𝑥 ∈ { 0 } ) )
19 17 18 sylibr ⊢ ( 𝐺 ∈ 𝑉 → { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } ⊆ { 0 } )
20 4 19 eqsstrid ⊢ ( 𝐺 ∈ 𝑉 → 𝑂 ⊆ { 0 } )