Metamath Proof Explorer


Theorem 0subm

Description: The zero submonoid of an arbitrary monoid. (Contributed by AV, 17-Feb-2024)

Ref Expression
Hypothesis 0subm.z
|- .0. = ( 0g ` G )
Assertion 0subm
|- ( G e. Mnd -> { .0. } e. ( SubMnd ` G ) )

Proof

Step Hyp Ref Expression
1 0subm.z
 |-  .0. = ( 0g ` G )
2 eqid
 |-  ( Base ` G ) = ( Base ` G )
3 2 1 mndidcl
 |-  ( G e. Mnd -> .0. e. ( Base ` G ) )
4 3 snssd
 |-  ( G e. Mnd -> { .0. } C_ ( Base ` G ) )
5 1 fvexi
 |-  .0. e. _V
6 5 snid
 |-  .0. e. { .0. }
7 6 a1i
 |-  ( G e. Mnd -> .0. e. { .0. } )
8 velsn
 |-  ( a e. { .0. } <-> a = .0. )
9 velsn
 |-  ( b e. { .0. } <-> b = .0. )
10 8 9 anbi12i
 |-  ( ( a e. { .0. } /\ b e. { .0. } ) <-> ( a = .0. /\ b = .0. ) )
11 eqid
 |-  ( +g ` G ) = ( +g ` G )
12 2 11 1 mndlid
 |-  ( ( G e. Mnd /\ .0. e. ( Base ` G ) ) -> ( .0. ( +g ` G ) .0. ) = .0. )
13 3 12 mpdan
 |-  ( G e. Mnd -> ( .0. ( +g ` G ) .0. ) = .0. )
14 ovex
 |-  ( .0. ( +g ` G ) .0. ) e. _V
15 14 elsn
 |-  ( ( .0. ( +g ` G ) .0. ) e. { .0. } <-> ( .0. ( +g ` G ) .0. ) = .0. )
16 13 15 sylibr
 |-  ( G e. Mnd -> ( .0. ( +g ` G ) .0. ) e. { .0. } )
17 oveq12
 |-  ( ( a = .0. /\ b = .0. ) -> ( a ( +g ` G ) b ) = ( .0. ( +g ` G ) .0. ) )
18 17 eleq1d
 |-  ( ( a = .0. /\ b = .0. ) -> ( ( a ( +g ` G ) b ) e. { .0. } <-> ( .0. ( +g ` G ) .0. ) e. { .0. } ) )
19 16 18 syl5ibrcom
 |-  ( G e. Mnd -> ( ( a = .0. /\ b = .0. ) -> ( a ( +g ` G ) b ) e. { .0. } ) )
20 10 19 syl5bi
 |-  ( G e. Mnd -> ( ( a e. { .0. } /\ b e. { .0. } ) -> ( a ( +g ` G ) b ) e. { .0. } ) )
21 20 ralrimivv
 |-  ( G e. Mnd -> A. a e. { .0. } A. b e. { .0. } ( a ( +g ` G ) b ) e. { .0. } )
22 2 1 11 issubm
 |-  ( G e. Mnd -> ( { .0. } e. ( SubMnd ` G ) <-> ( { .0. } C_ ( Base ` G ) /\ .0. e. { .0. } /\ A. a e. { .0. } A. b e. { .0. } ( a ( +g ` G ) b ) e. { .0. } ) ) )
23 4 7 21 22 mpbir3and
 |-  ( G e. Mnd -> { .0. } e. ( SubMnd ` G ) )