Theorem 0subm

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

	Ref	Expression
Hypothesis	0subm.z	$$⊢\underset{\dot{}}{0}=0_G$$
Assertion	0subm	$$⊢G\in \mathrm{Mnd}\to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{SubMnd}\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		0subm.z	$$⊢\underset{\dot{}}{0}=0_G$$
2		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
3	2 1	mndidcl	$$⊢G\in \mathrm{Mnd}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_G$$
4	3	snssd	$$⊢G\in \mathrm{Mnd}\to \left\{\underset{\dot{}}{0}\right\}\subseteq {\mathrm{Base}}_G$$
5	1	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
6	5	snid	$$⊢\underset{\dot{}}{0}\in \left\{\underset{\dot{}}{0}\right\}$$
7	6	a1i	$$⊢G\in \mathrm{Mnd}\to \underset{\dot{}}{0}\in \left\{\underset{\dot{}}{0}\right\}$$
8		velsn	$$⊢a\in \left\{\underset{\dot{}}{0}\right\}\leftrightarrow a=\underset{\dot{}}{0}$$
9		velsn	$$⊢b\in \left\{\underset{\dot{}}{0}\right\}\leftrightarrow b=\underset{\dot{}}{0}$$
10	8 9	anbi12i	$$⊢\left(a\in \left\{\underset{\dot{}}{0}\right\}\wedge b\in \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(a=\underset{\dot{}}{0}\wedge b=\underset{\dot{}}{0}\right)$$
11		eqid	$$⊢{+}_G={+}_G$$
12	2 11 1	mndlid	$$⊢\left(G\in \mathrm{Mnd}\wedge \underset{\dot{}}{0}\in {\mathrm{Base}}_G\right)\to \underset{\dot{}}{0}{+}_G\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
13	3 12	mpdan	$$⊢G\in \mathrm{Mnd}\to \underset{\dot{}}{0}{+}_G\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
14		ovex	$$⊢\underset{\dot{}}{0}{+}_G\underset{\dot{}}{0}\in \mathrm{V}$$
15	14	elsn	$$⊢\underset{\dot{}}{0}{+}_G\underset{\dot{}}{0}\in \left\{\underset{\dot{}}{0}\right\}\leftrightarrow \underset{\dot{}}{0}{+}_G\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
16	13 15	sylibr	$$⊢G\in \mathrm{Mnd}\to \underset{\dot{}}{0}{+}_G\underset{\dot{}}{0}\in \left\{\underset{\dot{}}{0}\right\}$$
17		oveq12	$$⊢\left(a=\underset{\dot{}}{0}\wedge b=\underset{\dot{}}{0}\right)\to a{+}_{G}b=\underset{\dot{}}{0}{+}_G\underset{\dot{}}{0}$$
18	17	eleq1d	$$⊢\left(a=\underset{\dot{}}{0}\wedge b=\underset{\dot{}}{0}\right)\to \left(a{+}_{G}b\in \left\{\underset{\dot{}}{0}\right\}\leftrightarrow \underset{\dot{}}{0}{+}_G\underset{\dot{}}{0}\in \left\{\underset{\dot{}}{0}\right\}\right)$$
19	16 18	syl5ibrcom	$$⊢G\in \mathrm{Mnd}\to \left(\left(a=\underset{\dot{}}{0}\wedge b=\underset{\dot{}}{0}\right)\to a{+}_{G}b\in \left\{\underset{\dot{}}{0}\right\}\right)$$
20	10 19	syl5bi	$$⊢G\in \mathrm{Mnd}\to \left(\left(a\in \left\{\underset{\dot{}}{0}\right\}\wedge b\in \left\{\underset{\dot{}}{0}\right\}\right)\to a{+}_{G}b\in \left\{\underset{\dot{}}{0}\right\}\right)$$
21	20	ralrimivv	$$⊢G\in \mathrm{Mnd}\to \forall a\in \left\{\underset{\dot{}}{0}\right\}\forall b\in \left\{\underset{\dot{}}{0}\right\}a{+}_{G}b\in \left\{\underset{\dot{}}{0}\right\}$$
22	2 1 11	issubm	$$⊢G\in \mathrm{Mnd}\to \left(\left\{\underset{\dot{}}{0}\right\}\in \mathrm{SubMnd}\left(G\right)\leftrightarrow \left(\left\{\underset{\dot{}}{0}\right\}\subseteq {\mathrm{Base}}_G\wedge \underset{\dot{}}{0}\in \left\{\underset{\dot{}}{0}\right\}\wedge \forall a\in \left\{\underset{\dot{}}{0}\right\}\forall b\in \left\{\underset{\dot{}}{0}\right\}a{+}_{G}b\in \left\{\underset{\dot{}}{0}\right\}\right)\right)$$
23	4 7 21 22	mpbir3and	$$⊢G\in \mathrm{Mnd}\to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{SubMnd}\left(G\right)$$