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

Metamath Proof Explorer

Theorem grp1

Description: The (smallest) structure representing atrivial group. According to Wikipedia ("Trivial group", 28-Apr-2019, https://en.wikipedia.org/wiki/Trivial_group ) "In mathematics, a trivial group is a group consisting of a single element. All such groups are isomorphic, so one often speaks ofthe trivial group. The single element of the trivial group is the identity element". (Contributed by AV, 28-Apr-2019)

Ref Expression
Hypothesis grp1.m ⊢ 𝑀 = { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ }
Assertion grp1 ( 𝐼 ∈ 𝑉 → 𝑀 ∈ Grp )

Proof

Step Hyp Ref Expression
1 grp1.m ⊢ 𝑀 = { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ }
2 1 mnd1 ⊢ ( 𝐼 ∈ 𝑉 → 𝑀 ∈ Mnd )
3 df-ov ⊢ ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = ( { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ‘ ⟨ 𝐼 , 𝐼 ⟩ )
4 opex ⊢ ⟨ 𝐼 , 𝐼 ⟩ ∈ V
5 fvsng ⊢ ( ( ⟨ 𝐼 , 𝐼 ⟩ ∈ V ∧ 𝐼 ∈ 𝑉 ) → ( { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ‘ ⟨ 𝐼 , 𝐼 ⟩ ) = 𝐼 )
6 4 5 mpan ⊢ ( 𝐼 ∈ 𝑉 → ( { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ‘ ⟨ 𝐼 , 𝐼 ⟩ ) = 𝐼 )
7 3 6 eqtrid ⊢ ( 𝐼 ∈ 𝑉 → ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = 𝐼 )
8 1 mnd1id ⊢ ( 𝐼 ∈ 𝑉 → ( 0g ‘ 𝑀 ) = 𝐼 )
9 7 8 eqtr4d ⊢ ( 𝐼 ∈ 𝑉 → ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = ( 0g ‘ 𝑀 ) )
10 oveq2 ⊢ ( 𝑖 = 𝐼 → ( 𝑒 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑖 ) = ( 𝑒 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) )
11 10 eqeq1d ⊢ ( 𝑖 = 𝐼 → ( ( 𝑒 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑖 ) = ( 0g ‘ 𝑀 ) ↔ ( 𝑒 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = ( 0g ‘ 𝑀 ) ) )
12 11 rexbidv ⊢ ( 𝑖 = 𝐼 → ( ∃ 𝑒 ∈ { 𝐼 } ( 𝑒 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑖 ) = ( 0g ‘ 𝑀 ) ↔ ∃ 𝑒 ∈ { 𝐼 } ( 𝑒 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = ( 0g ‘ 𝑀 ) ) )
13 12 ralsng ⊢ ( 𝐼 ∈ 𝑉 → ( ∀ 𝑖 ∈ { 𝐼 } ∃ 𝑒 ∈ { 𝐼 } ( 𝑒 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑖 ) = ( 0g ‘ 𝑀 ) ↔ ∃ 𝑒 ∈ { 𝐼 } ( 𝑒 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = ( 0g ‘ 𝑀 ) ) )
14 oveq1 ⊢ ( 𝑒 = 𝐼 → ( 𝑒 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) )
15 14 eqeq1d ⊢ ( 𝑒 = 𝐼 → ( ( 𝑒 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = ( 0g ‘ 𝑀 ) ↔ ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = ( 0g ‘ 𝑀 ) ) )
16 15 rexsng ⊢ ( 𝐼 ∈ 𝑉 → ( ∃ 𝑒 ∈ { 𝐼 } ( 𝑒 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = ( 0g ‘ 𝑀 ) ↔ ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = ( 0g ‘ 𝑀 ) ) )
17 13 16 bitrd ⊢ ( 𝐼 ∈ 𝑉 → ( ∀ 𝑖 ∈ { 𝐼 } ∃ 𝑒 ∈ { 𝐼 } ( 𝑒 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑖 ) = ( 0g ‘ 𝑀 ) ↔ ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = ( 0g ‘ 𝑀 ) ) )
18 9 17 mpbird ⊢ ( 𝐼 ∈ 𝑉 → ∀ 𝑖 ∈ { 𝐼 } ∃ 𝑒 ∈ { 𝐼 } ( 𝑒 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑖 ) = ( 0g ‘ 𝑀 ) )
19 snex ⊢ { 𝐼 } ∈ V
20 1 grpbase ⊢ ( { 𝐼 } ∈ V → { 𝐼 } = ( Base ‘ 𝑀 ) )
21 19 20 ax-mp ⊢ { 𝐼 } = ( Base ‘ 𝑀 )
22 snex ⊢ { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ∈ V
23 1 grpplusg ⊢ ( { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ∈ V → { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } = ( +g ‘ 𝑀 ) )
24 22 23 ax-mp ⊢ { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } = ( +g ‘ 𝑀 )
25 eqid ⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
26 21 24 25 isgrp ⊢ ( 𝑀 ∈ Grp ↔ ( 𝑀 ∈ Mnd ∧ ∀ 𝑖 ∈ { 𝐼 } ∃ 𝑒 ∈ { 𝐼 } ( 𝑒 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝑖 ) = ( 0g ‘ 𝑀 ) ) )
27 2 18 26 sylanbrc ⊢ ( 𝐼 ∈ 𝑉 → 𝑀 ∈ Grp )