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 ˙ = 0 G
Assertion 0subm G Mnd 0 ˙ SubMnd G

Proof

Step Hyp Ref Expression
1 0subm.z 0 ˙ = 0 G
2 eqid Base G = Base G
3 2 1 mndidcl G Mnd 0 ˙ Base G
4 3 snssd G Mnd 0 ˙ Base G
5 1 fvexi 0 ˙ V
6 5 snid 0 ˙ 0 ˙
7 6 a1i G Mnd 0 ˙ 0 ˙
8 velsn a 0 ˙ a = 0 ˙
9 velsn b 0 ˙ b = 0 ˙
10 8 9 anbi12i a 0 ˙ b 0 ˙ a = 0 ˙ b = 0 ˙
11 eqid + G = + G
12 2 11 1 mndlid G Mnd 0 ˙ Base G 0 ˙ + G 0 ˙ = 0 ˙
13 3 12 mpdan G Mnd 0 ˙ + G 0 ˙ = 0 ˙
14 ovex 0 ˙ + G 0 ˙ V
15 14 elsn 0 ˙ + G 0 ˙ 0 ˙ 0 ˙ + G 0 ˙ = 0 ˙
16 13 15 sylibr G Mnd 0 ˙ + G 0 ˙ 0 ˙
17 oveq12 a = 0 ˙ b = 0 ˙ a + G b = 0 ˙ + G 0 ˙
18 17 eleq1d a = 0 ˙ b = 0 ˙ a + G b 0 ˙ 0 ˙ + G 0 ˙ 0 ˙
19 16 18 syl5ibrcom G Mnd a = 0 ˙ b = 0 ˙ a + G b 0 ˙
20 10 19 syl5bi G Mnd a 0 ˙ b 0 ˙ a + G b 0 ˙
21 20 ralrimivv G Mnd a 0 ˙ b 0 ˙ a + G b 0 ˙
22 2 1 11 issubm G Mnd 0 ˙ SubMnd G 0 ˙ Base G 0 ˙ 0 ˙ a 0 ˙ b 0 ˙ a + G b 0 ˙
23 4 7 21 22 mpbir3and G Mnd 0 ˙ SubMnd G