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 } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. }
Assertion grp1 
|- ( I e. V -> M e. Grp )

Proof

Step Hyp Ref Expression
1 grp1.m 
 |-  M = { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. }
2 1 mnd1 
 |-  ( I e. V -> M e. Mnd )
3 df-ov 
 |-  ( I { <. <. I , I >. , I >. } I ) = ( { <. <. I , I >. , I >. } ` <. I , I >. )
4 opex 
 |-  <. I , I >. e. _V
5 fvsng 
 |-  ( ( <. I , I >. e. _V /\ I e. V ) -> ( { <. <. I , I >. , I >. } ` <. I , I >. ) = I )
6 4 5 mpan 
 |-  ( I e. V -> ( { <. <. I , I >. , I >. } ` <. I , I >. ) = I )
7 3 6 syl5eq 
 |-  ( I e. V -> ( I { <. <. I , I >. , I >. } I ) = I )
8 1 mnd1id 
 |-  ( I e. V -> ( 0g ` M ) = I )
9 7 8 eqtr4d 
 |-  ( I e. V -> ( I { <. <. I , I >. , I >. } I ) = ( 0g ` 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 ) = ( 0g ` M ) <-> ( e { <. <. I , I >. , I >. } I ) = ( 0g ` M ) ) )
12 11 rexbidv 
 |-  ( i = I -> ( E. e e. { I } ( e { <. <. I , I >. , I >. } i ) = ( 0g ` M ) <-> E. e e. { I } ( e { <. <. I , I >. , I >. } I ) = ( 0g ` M ) ) )
13 12 ralsng 
 |-  ( I e. V -> ( A. i e. { I } E. e e. { I } ( e { <. <. I , I >. , I >. } i ) = ( 0g ` M ) <-> E. e e. { I } ( e { <. <. I , I >. , I >. } I ) = ( 0g ` 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 ) = ( 0g ` M ) <-> ( I { <. <. I , I >. , I >. } I ) = ( 0g ` M ) ) )
16 15 rexsng 
 |-  ( I e. V -> ( E. e e. { I } ( e { <. <. I , I >. , I >. } I ) = ( 0g ` M ) <-> ( I { <. <. I , I >. , I >. } I ) = ( 0g ` M ) ) )
17 13 16 bitrd 
 |-  ( I e. V -> ( A. i e. { I } E. e e. { I } ( e { <. <. I , I >. , I >. } i ) = ( 0g ` M ) <-> ( I { <. <. I , I >. , I >. } I ) = ( 0g ` M ) ) )
18 9 17 mpbird 
 |-  ( I e. V -> A. i e. { I } E. e e. { I } ( e { <. <. I , I >. , I >. } i ) = ( 0g ` M ) )
19 snex 
 |-  { I } e. _V
20 1 grpbase 
 |-  ( { I } e. _V -> { I } = ( Base ` M ) )
21 19 20 ax-mp 
 |-  { I } = ( Base ` M )
22 snex 
 |-  { <. <. I , I >. , I >. } e. _V
23 1 grpplusg 
 |-  ( { <. <. I , I >. , I >. } e. _V -> { <. <. I , I >. , I >. } = ( +g ` M ) )
24 22 23 ax-mp 
 |-  { <. <. I , I >. , I >. } = ( +g ` M )
25 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
26 21 24 25 isgrp 
 |-  ( M e. Grp <-> ( M e. Mnd /\ A. i e. { I } E. e e. { I } ( e { <. <. I , I >. , I >. } i ) = ( 0g ` M ) ) )
27 2 18 26 sylanbrc 
 |-  ( I e. V -> M e. Grp )