submacs

Description: Submonoids are an algebraic closure system. (Contributed by Stefan O'Rear, 22-Aug-2015)

		Ref	Expression
	Hypothesis	submacs.b	$⊢ B = {Base}_{G}$
	Assertion	submacs	$⊢ G \in Mnd \to SubMnd (G) \in ACS (B)$

Proof

Step	Hyp	Ref	Expression
1		submacs.b	$⊢ B = {Base}_{G}$
2		eqid	$⊢ 0_{G} = 0_{G}$
3		eqid	$⊢ +_{G} = +_{G}$
4	1 2 3	issubm	$⊢ G \in Mnd \to (s \in SubMnd (G) \leftrightarrow (s \subseteq B \land 0_{G} \in s \land \forall x \in s \forall y \in s x +_{G} y \in s))$
5		velpw	$⊢ s \in 𝒫 B \leftrightarrow s \subseteq B$
6	5	anbi1i	$⊢ (s \in 𝒫 B \land (0_{G} \in s \land \forall x \in s \forall y \in s x +_{G} y \in s)) \leftrightarrow (s \subseteq B \land (0_{G} \in s \land \forall x \in s \forall y \in s x +_{G} y \in s))$
7		3anass	$⊢ (s \subseteq B \land 0_{G} \in s \land \forall x \in s \forall y \in s x +_{G} y \in s) \leftrightarrow (s \subseteq B \land (0_{G} \in s \land \forall x \in s \forall y \in s x +_{G} y \in s))$
8	6 7	bitr4i	$⊢ (s \in 𝒫 B \land (0_{G} \in s \land \forall x \in s \forall y \in s x +_{G} y \in s)) \leftrightarrow (s \subseteq B \land 0_{G} \in s \land \forall x \in s \forall y \in s x +_{G} y \in s)$
9	4 8	bitr4di	$⊢ G \in Mnd \to (s \in SubMnd (G) \leftrightarrow (s \in 𝒫 B \land (0_{G} \in s \land \forall x \in s \forall y \in s x +_{G} y \in s)))$
10	9	abbi2dv	$⊢ G \in Mnd \to SubMnd (G) = \{s \| (s \in 𝒫 B \land (0_{G} \in s \land \forall x \in s \forall y \in s x +_{G} y \in s))\}$
11		df-rab	$⊢ \{s \in 𝒫 B \| (0_{G} \in s \land \forall x \in s \forall y \in s x +_{G} y \in s)\} = \{s \| (s \in 𝒫 B \land (0_{G} \in s \land \forall x \in s \forall y \in s x +_{G} y \in s))\}$
12	10 11	eqtr4di	$⊢ G \in Mnd \to SubMnd (G) = \{s \in 𝒫 B \| (0_{G} \in s \land \forall x \in s \forall y \in s x +_{G} y \in s)\}$
13		inrab	$⊢ \{s \in 𝒫 B \| 0_{G} \in s\} \cap \{s \in 𝒫 B \| \forall x \in s \forall y \in s x +_{G} y \in s\} = \{s \in 𝒫 B \| (0_{G} \in s \land \forall x \in s \forall y \in s x +_{G} y \in s)\}$
14	1	fvexi	$⊢ B \in V$
15		mreacs	$⊢ B \in V \to ACS (B) \in Moore (𝒫 B)$
16	14 15	mp1i	$⊢ G \in Mnd \to ACS (B) \in Moore (𝒫 B)$
17	1 2	mndidcl	$⊢ G \in Mnd \to 0_{G} \in B$
18		acsfn0	$⊢ (B \in V \land 0_{G} \in B) \to \{s \in 𝒫 B \| 0_{G} \in s\} \in ACS (B)$
19	14 17 18	sylancr	$⊢ G \in Mnd \to \{s \in 𝒫 B \| 0_{G} \in s\} \in ACS (B)$
20	1 3	mndcl	$⊢ (G \in Mnd \land x \in B \land y \in B) \to x +_{G} y \in B$
21	20	3expb	$⊢ (G \in Mnd \land (x \in B \land y \in B)) \to x +_{G} y \in B$
22	21	ralrimivva	$⊢ G \in Mnd \to \forall x \in B \forall y \in B x +_{G} y \in B$
23		acsfn2	$⊢ (B \in V \land \forall x \in B \forall y \in B x +_{G} y \in B) \to \{s \in 𝒫 B \| \forall x \in s \forall y \in s x +_{G} y \in s\} \in ACS (B)$
24	14 22 23	sylancr	$⊢ G \in Mnd \to \{s \in 𝒫 B \| \forall x \in s \forall y \in s x +_{G} y \in s\} \in ACS (B)$
25		mreincl	$⊢ (ACS (B) \in Moore (𝒫 B) \land \{s \in 𝒫 B \| 0_{G} \in s\} \in ACS (B) \land \{s \in 𝒫 B \| \forall x \in s \forall y \in s x +_{G} y \in s\} \in ACS (B)) \to \{s \in 𝒫 B \| 0_{G} \in s\} \cap \{s \in 𝒫 B \| \forall x \in s \forall y \in s x +_{G} y \in s\} \in ACS (B)$
26	16 19 24 25	syl3anc	$⊢ G \in Mnd \to \{s \in 𝒫 B \| 0_{G} \in s\} \cap \{s \in 𝒫 B \| \forall x \in s \forall y \in s x +_{G} y \in s\} \in ACS (B)$
27	13 26	eqeltrrid	$⊢ G \in Mnd \to \{s \in 𝒫 B \| (0_{G} \in s \land \forall x \in s \forall y \in s x +_{G} y \in s)\} \in ACS (B)$
28	12 27	eqeltrd	$⊢ G \in Mnd \to SubMnd (G) \in ACS (B)$

Metamath Proof Explorer

Theorem submacs

Proof