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 ⊢ M = Base ndx I + ndx I I I
Assertion grp1 ⊢ I ∈ V → M ∈ Grp

Proof

Step Hyp Ref Expression
1 grp1.m ⊢ M = Base ndx I + ndx I I I
2 1 mnd1 ⊢ I ∈ V → M ∈ Mnd
3 df-ov ⊢ I I I I I = I I I ⁡ I I
4 opex ⊢ I I ∈ V
5 fvsng ⊢ I I ∈ V ∧ I ∈ V → I I I ⁡ I I = I
6 4 5 mpan ⊢ I ∈ V → I I I ⁡ I I = I
7 3 6 eqtrid ⊢ I ∈ V → I I I I I = I
8 1 mnd1id ⊢ I ∈ V → 0 M = I
9 7 8 eqtr4d ⊢ I ∈ V → I I I I I = 0 M
10 oveq2 ⊢ i = I → e I I I i = e I I I I
11 10 eqeq1d ⊢ i = I → e I I I i = 0 M ↔ e I I I I = 0 M
12 11 rexbidv ⊢ i = I → ∃ e ∈ I e I I I i = 0 M ↔ ∃ e ∈ I e I I I I = 0 M
13 12 ralsng ⊢ I ∈ V → ∀ i ∈ I ∃ e ∈ I e I I I i = 0 M ↔ ∃ e ∈ I e I I I I = 0 M
14 oveq1 ⊢ e = I → e I I I I = I I I I I
15 14 eqeq1d ⊢ e = I → e I I I I = 0 M ↔ I I I I I = 0 M
16 15 rexsng ⊢ I ∈ V → ∃ e ∈ I e I I I I = 0 M ↔ I I I I I = 0 M
17 13 16 bitrd ⊢ I ∈ V → ∀ i ∈ I ∃ e ∈ I e I I I i = 0 M ↔ I I I I I = 0 M
18 9 17 mpbird ⊢ I ∈ V → ∀ i ∈ I ∃ e ∈ I e I I I i = 0 M
19 snex ⊢ I ∈ V
20 1 grpbase ⊢ I ∈ V → I = Base M
21 19 20 ax-mp ⊢ I = Base M
22 snex ⊢ I I I ∈ V
23 1 grpplusg ⊢ I I I ∈ V → I I I = + M
24 22 23 ax-mp ⊢ I I I = + M
25 eqid ⊢ 0 M = 0 M
26 21 24 25 isgrp ⊢ M ∈ Grp ↔ M ∈ Mnd ∧ ∀ i ∈ I ∃ e ∈ I e I I I i = 0 M
27 2 18 26 sylanbrc ⊢ I ∈ V → M ∈ Grp