issubm

Description: Expand definition of a submonoid. (Contributed by Mario Carneiro, 7-Mar-2015)

	Ref	Expression
Hypotheses	issubm.b	$⊢ B = {Base}_{M}$
	issubm.z	$⊢ \underset{˙}{0} = 0_{M}$
	issubm.p	$⊢ \underset{˙}{+} = +_{M}$
Assertion	issubm	$⊢ M \in Mnd \to (S \in SubMnd (M) \leftrightarrow (S \subseteq B \land \underset{˙}{0} \in S \land \forall x \in S \forall y \in S x \underset{˙}{+} y \in S))$

Proof

Step	Hyp	Ref	Expression
1		issubm.b	$⊢ B = {Base}_{M}$
2		issubm.z	$⊢ \underset{˙}{0} = 0_{M}$
3		issubm.p	$⊢ \underset{˙}{+} = +_{M}$
4		fveq2	$⊢ m = M \to {Base}_{m} = {Base}_{M}$
5	4	pweqd	$⊢ m = M \to 𝒫 {Base}_{m} = 𝒫 {Base}_{M}$
6		fveq2	$⊢ m = M \to 0_{m} = 0_{M}$
7	6	eleq1d	$⊢ m = M \to (0_{m} \in t \leftrightarrow 0_{M} \in t)$
8		fveq2	$⊢ m = M \to +_{m} = +_{M}$
9	8	oveqd	$⊢ m = M \to x +_{m} y = x +_{M} y$
10	9	eleq1d	$⊢ m = M \to (x +_{m} y \in t \leftrightarrow x +_{M} y \in t)$
11	10	2ralbidv	$⊢ m = M \to (\forall x \in t \forall y \in t x +_{m} y \in t \leftrightarrow \forall x \in t \forall y \in t x +_{M} y \in t)$
12	7 11	anbi12d	$⊢ m = M \to ((0_{m} \in t \land \forall x \in t \forall y \in t x +_{m} y \in t) \leftrightarrow (0_{M} \in t \land \forall x \in t \forall y \in t x +_{M} y \in t))$
13	5 12	rabeqbidv	$⊢ m = M \to \{t \in 𝒫 {Base}_{m} \| (0_{m} \in t \land \forall x \in t \forall y \in t x +_{m} y \in t)\} = \{t \in 𝒫 {Base}_{M} \| (0_{M} \in t \land \forall x \in t \forall y \in t x +_{M} y \in t)\}$
14		df-submnd	$⊢ SubMnd = (m \in Mnd ⟼ \{t \in 𝒫 {Base}_{m} \| (0_{m} \in t \land \forall x \in t \forall y \in t x +_{m} y \in t)\})$
15		fvex	$⊢ {Base}_{M} \in V$
16	15	pwex	$⊢ 𝒫 {Base}_{M} \in V$
17	16	rabex	$⊢ \{t \in 𝒫 {Base}_{M} \| (0_{M} \in t \land \forall x \in t \forall y \in t x +_{M} y \in t)\} \in V$
18	13 14 17	fvmpt	$⊢ M \in Mnd \to SubMnd (M) = \{t \in 𝒫 {Base}_{M} \| (0_{M} \in t \land \forall x \in t \forall y \in t x +_{M} y \in t)\}$
19	18	eleq2d	$⊢ M \in Mnd \to (S \in SubMnd (M) \leftrightarrow S \in \{t \in 𝒫 {Base}_{M} \| (0_{M} \in t \land \forall x \in t \forall y \in t x +_{M} y \in t)\})$
20		eleq2	$⊢ t = S \to (0_{M} \in t \leftrightarrow 0_{M} \in S)$
21		eleq2	$⊢ t = S \to (x +_{M} y \in t \leftrightarrow x +_{M} y \in S)$
22	21	raleqbi1dv	$⊢ t = S \to (\forall y \in t x +_{M} y \in t \leftrightarrow \forall y \in S x +_{M} y \in S)$
23	22	raleqbi1dv	$⊢ t = S \to (\forall x \in t \forall y \in t x +_{M} y \in t \leftrightarrow \forall x \in S \forall y \in S x +_{M} y \in S)$
24	20 23	anbi12d	$⊢ t = S \to ((0_{M} \in t \land \forall x \in t \forall y \in t x +_{M} y \in t) \leftrightarrow (0_{M} \in S \land \forall x \in S \forall y \in S x +_{M} y \in S))$
25	24	elrab	$⊢ S \in \{t \in 𝒫 {Base}_{M} \| (0_{M} \in t \land \forall x \in t \forall y \in t x +_{M} y \in t)\} \leftrightarrow (S \in 𝒫 {Base}_{M} \land (0_{M} \in S \land \forall x \in S \forall y \in S x +_{M} y \in S))$
26	1	sseq2i	$⊢ S \subseteq B \leftrightarrow S \subseteq {Base}_{M}$
27	2	eleq1i	$⊢ \underset{˙}{0} \in S \leftrightarrow 0_{M} \in S$
28	3	oveqi	$⊢ x \underset{˙}{+} y = x +_{M} y$
29	28	eleq1i	$⊢ x \underset{˙}{+} y \in S \leftrightarrow x +_{M} y \in S$
30	29	2ralbii	$⊢ \forall x \in S \forall y \in S x \underset{˙}{+} y \in S \leftrightarrow \forall x \in S \forall y \in S x +_{M} y \in S$
31	27 30	anbi12i	$⊢ (\underset{˙}{0} \in S \land \forall x \in S \forall y \in S x \underset{˙}{+} y \in S) \leftrightarrow (0_{M} \in S \land \forall x \in S \forall y \in S x +_{M} y \in S)$
32	26 31	anbi12i	$⊢ (S \subseteq B \land (\underset{˙}{0} \in S \land \forall x \in S \forall y \in S x \underset{˙}{+} y \in S)) \leftrightarrow (S \subseteq {Base}_{M} \land (0_{M} \in S \land \forall x \in S \forall y \in S x +_{M} y \in S))$
33		3anass	$⊢ (S \subseteq B \land \underset{˙}{0} \in S \land \forall x \in S \forall y \in S x \underset{˙}{+} y \in S) \leftrightarrow (S \subseteq B \land (\underset{˙}{0} \in S \land \forall x \in S \forall y \in S x \underset{˙}{+} y \in S))$
34	15	elpw2	$⊢ S \in 𝒫 {Base}_{M} \leftrightarrow S \subseteq {Base}_{M}$
35	34	anbi1i	$⊢ (S \in 𝒫 {Base}_{M} \land (0_{M} \in S \land \forall x \in S \forall y \in S x +_{M} y \in S)) \leftrightarrow (S \subseteq {Base}_{M} \land (0_{M} \in S \land \forall x \in S \forall y \in S x +_{M} y \in S))$
36	32 33 35	3bitr4ri	$⊢ (S \in 𝒫 {Base}_{M} \land (0_{M} \in S \land \forall x \in S \forall y \in S x +_{M} y \in S)) \leftrightarrow (S \subseteq B \land \underset{˙}{0} \in S \land \forall x \in S \forall y \in S x \underset{˙}{+} y \in S)$
37	25 36	bitri	$⊢ S \in \{t \in 𝒫 {Base}_{M} \| (0_{M} \in t \land \forall x \in t \forall y \in t x +_{M} y \in t)\} \leftrightarrow (S \subseteq B \land \underset{˙}{0} \in S \land \forall x \in S \forall y \in S x \underset{˙}{+} y \in S)$
38	19 37	bitrdi	$⊢ M \in Mnd \to (S \in SubMnd (M) \leftrightarrow (S \subseteq B \land \underset{˙}{0} \in S \land \forall x \in S \forall y \in S x \underset{˙}{+} y \in S))$

Metamath Proof Explorer

Theorem issubm

Proof