insubm

Description: The intersection of two submonoids is a submonoid. (Contributed by AV, 25-Feb-2024)

		Ref	Expression
	Assertion	insubm	$⊢ (A \in SubMnd (M) \land B \in SubMnd (M)) \to A \cap B \in SubMnd (M)$

Proof

Step	Hyp	Ref	Expression
1		submrcl	$⊢ A \in SubMnd (M) \to M \in Mnd$
2		ssinss1	$⊢ A \subseteq {Base}_{M} \to A \cap B \subseteq {Base}_{M}$
3	2	3ad2ant1	$⊢ (A \subseteq {Base}_{M} \land 0_{M} \in A \land \forall a \in A \forall b \in A a +_{M} b \in A) \to A \cap B \subseteq {Base}_{M}$
4	3	ad2antrl	$⊢ (M \in Mnd \land ((A \subseteq {Base}_{M} \land 0_{M} \in A \land \forall a \in A \forall b \in A a +_{M} b \in A) \land (B \subseteq {Base}_{M} \land 0_{M} \in B \land \forall a \in B \forall b \in B a +_{M} b \in B))) \to A \cap B \subseteq {Base}_{M}$
5		elin	$⊢ 0_{M} \in (A \cap B) \leftrightarrow (0_{M} \in A \land 0_{M} \in B)$
6	5	simplbi2com	$⊢ 0_{M} \in B \to (0_{M} \in A \to 0_{M} \in (A \cap B))$
7	6	3ad2ant2	$⊢ (B \subseteq {Base}_{M} \land 0_{M} \in B \land \forall a \in B \forall b \in B a +_{M} b \in B) \to (0_{M} \in A \to 0_{M} \in (A \cap B))$
8	7	com12	$⊢ 0_{M} \in A \to ((B \subseteq {Base}_{M} \land 0_{M} \in B \land \forall a \in B \forall b \in B a +_{M} b \in B) \to 0_{M} \in (A \cap B))$
9	8	3ad2ant2	$⊢ (A \subseteq {Base}_{M} \land 0_{M} \in A \land \forall a \in A \forall b \in A a +_{M} b \in A) \to ((B \subseteq {Base}_{M} \land 0_{M} \in B \land \forall a \in B \forall b \in B a +_{M} b \in B) \to 0_{M} \in (A \cap B))$
10	9	imp	$⊢ ((A \subseteq {Base}_{M} \land 0_{M} \in A \land \forall a \in A \forall b \in A a +_{M} b \in A) \land (B \subseteq {Base}_{M} \land 0_{M} \in B \land \forall a \in B \forall b \in B a +_{M} b \in B)) \to 0_{M} \in (A \cap B)$
11	10	adantl	$⊢ (M \in Mnd \land ((A \subseteq {Base}_{M} \land 0_{M} \in A \land \forall a \in A \forall b \in A a +_{M} b \in A) \land (B \subseteq {Base}_{M} \land 0_{M} \in B \land \forall a \in B \forall b \in B a +_{M} b \in B))) \to 0_{M} \in (A \cap B)$
12		elin	$⊢ x \in (A \cap B) \leftrightarrow (x \in A \land x \in B)$
13		elin	$⊢ y \in (A \cap B) \leftrightarrow (y \in A \land y \in B)$
14	12 13	anbi12i	$⊢ (x \in (A \cap B) \land y \in (A \cap B)) \leftrightarrow ((x \in A \land x \in B) \land (y \in A \land y \in B))$
15		oveq1	$⊢ a = x \to a +_{M} b = x +_{M} b$
16	15	eleq1d	$⊢ a = x \to (a +_{M} b \in A \leftrightarrow x +_{M} b \in A)$
17		oveq2	$⊢ b = y \to x +_{M} b = x +_{M} y$
18	17	eleq1d	$⊢ b = y \to (x +_{M} b \in A \leftrightarrow x +_{M} y \in A)$
19		simpl	$⊢ (x \in A \land x \in B) \to x \in A$
20	19	adantr	$⊢ ((x \in A \land x \in B) \land (y \in A \land y \in B)) \to x \in A$
21		eqidd	$⊢ (((x \in A \land x \in B) \land (y \in A \land y \in B)) \land a = x) \to A = A$
22		simpl	$⊢ (y \in A \land y \in B) \to y \in A$
23	22	adantl	$⊢ ((x \in A \land x \in B) \land (y \in A \land y \in B)) \to y \in A$
24	16 18 20 21 23	rspc2vd	$⊢ ((x \in A \land x \in B) \land (y \in A \land y \in B)) \to (\forall a \in A \forall b \in A a +_{M} b \in A \to x +_{M} y \in A)$
25	24	com12	$⊢ \forall a \in A \forall b \in A a +_{M} b \in A \to (((x \in A \land x \in B) \land (y \in A \land y \in B)) \to x +_{M} y \in A)$
26	25	3ad2ant3	$⊢ (A \subseteq {Base}_{M} \land 0_{M} \in A \land \forall a \in A \forall b \in A a +_{M} b \in A) \to (((x \in A \land x \in B) \land (y \in A \land y \in B)) \to x +_{M} y \in A)$
27	26	ad2antrl	$⊢ (M \in Mnd \land ((A \subseteq {Base}_{M} \land 0_{M} \in A \land \forall a \in A \forall b \in A a +_{M} b \in A) \land (B \subseteq {Base}_{M} \land 0_{M} \in B \land \forall a \in B \forall b \in B a +_{M} b \in B))) \to (((x \in A \land x \in B) \land (y \in A \land y \in B)) \to x +_{M} y \in A)$
28	27	imp	$⊢ ((M \in Mnd \land ((A \subseteq {Base}_{M} \land 0_{M} \in A \land \forall a \in A \forall b \in A a +_{M} b \in A) \land (B \subseteq {Base}_{M} \land 0_{M} \in B \land \forall a \in B \forall b \in B a +_{M} b \in B))) \land ((x \in A \land x \in B) \land (y \in A \land y \in B))) \to x +_{M} y \in A$
29	15	eleq1d	$⊢ a = x \to (a +_{M} b \in B \leftrightarrow x +_{M} b \in B)$
30	17	eleq1d	$⊢ b = y \to (x +_{M} b \in B \leftrightarrow x +_{M} y \in B)$
31		simpr	$⊢ (x \in A \land x \in B) \to x \in B$
32	31	adantr	$⊢ ((x \in A \land x \in B) \land (y \in A \land y \in B)) \to x \in B$
33		eqidd	$⊢ (((x \in A \land x \in B) \land (y \in A \land y \in B)) \land a = x) \to B = B$
34		simpr	$⊢ (y \in A \land y \in B) \to y \in B$
35	34	adantl	$⊢ ((x \in A \land x \in B) \land (y \in A \land y \in B)) \to y \in B$
36	29 30 32 33 35	rspc2vd	$⊢ ((x \in A \land x \in B) \land (y \in A \land y \in B)) \to (\forall a \in B \forall b \in B a +_{M} b \in B \to x +_{M} y \in B)$
37	36	com12	$⊢ \forall a \in B \forall b \in B a +_{M} b \in B \to (((x \in A \land x \in B) \land (y \in A \land y \in B)) \to x +_{M} y \in B)$
38	37	3ad2ant3	$⊢ (B \subseteq {Base}_{M} \land 0_{M} \in B \land \forall a \in B \forall b \in B a +_{M} b \in B) \to (((x \in A \land x \in B) \land (y \in A \land y \in B)) \to x +_{M} y \in B)$
39	38	adantl	$⊢ ((A \subseteq {Base}_{M} \land 0_{M} \in A \land \forall a \in A \forall b \in A a +_{M} b \in A) \land (B \subseteq {Base}_{M} \land 0_{M} \in B \land \forall a \in B \forall b \in B a +_{M} b \in B)) \to (((x \in A \land x \in B) \land (y \in A \land y \in B)) \to x +_{M} y \in B)$
40	39	adantl	$⊢ (M \in Mnd \land ((A \subseteq {Base}_{M} \land 0_{M} \in A \land \forall a \in A \forall b \in A a +_{M} b \in A) \land (B \subseteq {Base}_{M} \land 0_{M} \in B \land \forall a \in B \forall b \in B a +_{M} b \in B))) \to (((x \in A \land x \in B) \land (y \in A \land y \in B)) \to x +_{M} y \in B)$
41	40	imp	$⊢ ((M \in Mnd \land ((A \subseteq {Base}_{M} \land 0_{M} \in A \land \forall a \in A \forall b \in A a +_{M} b \in A) \land (B \subseteq {Base}_{M} \land 0_{M} \in B \land \forall a \in B \forall b \in B a +_{M} b \in B))) \land ((x \in A \land x \in B) \land (y \in A \land y \in B))) \to x +_{M} y \in B$
42	28 41	elind	$⊢ ((M \in Mnd \land ((A \subseteq {Base}_{M} \land 0_{M} \in A \land \forall a \in A \forall b \in A a +_{M} b \in A) \land (B \subseteq {Base}_{M} \land 0_{M} \in B \land \forall a \in B \forall b \in B a +_{M} b \in B))) \land ((x \in A \land x \in B) \land (y \in A \land y \in B))) \to x +_{M} y \in (A \cap B)$
43	42	ex	$⊢ (M \in Mnd \land ((A \subseteq {Base}_{M} \land 0_{M} \in A \land \forall a \in A \forall b \in A a +_{M} b \in A) \land (B \subseteq {Base}_{M} \land 0_{M} \in B \land \forall a \in B \forall b \in B a +_{M} b \in B))) \to (((x \in A \land x \in B) \land (y \in A \land y \in B)) \to x +_{M} y \in (A \cap B))$
44	14 43	syl5bi	$⊢ (M \in Mnd \land ((A \subseteq {Base}_{M} \land 0_{M} \in A \land \forall a \in A \forall b \in A a +_{M} b \in A) \land (B \subseteq {Base}_{M} \land 0_{M} \in B \land \forall a \in B \forall b \in B a +_{M} b \in B))) \to ((x \in (A \cap B) \land y \in (A \cap B)) \to x +_{M} y \in (A \cap B))$
45	44	ralrimivv	$⊢ (M \in Mnd \land ((A \subseteq {Base}_{M} \land 0_{M} \in A \land \forall a \in A \forall b \in A a +_{M} b \in A) \land (B \subseteq {Base}_{M} \land 0_{M} \in B \land \forall a \in B \forall b \in B a +_{M} b \in B))) \to \forall x \in (A \cap B) \forall y \in (A \cap B) x +_{M} y \in (A \cap B)$
46	4 11 45	3jca	$⊢ (M \in Mnd \land ((A \subseteq {Base}_{M} \land 0_{M} \in A \land \forall a \in A \forall b \in A a +_{M} b \in A) \land (B \subseteq {Base}_{M} \land 0_{M} \in B \land \forall a \in B \forall b \in B a +_{M} b \in B))) \to (A \cap B \subseteq {Base}_{M} \land 0_{M} \in (A \cap B) \land \forall x \in (A \cap B) \forall y \in (A \cap B) x +_{M} y \in (A \cap B))$
47	46	ex	$⊢ M \in Mnd \to (((A \subseteq {Base}_{M} \land 0_{M} \in A \land \forall a \in A \forall b \in A a +_{M} b \in A) \land (B \subseteq {Base}_{M} \land 0_{M} \in B \land \forall a \in B \forall b \in B a +_{M} b \in B)) \to (A \cap B \subseteq {Base}_{M} \land 0_{M} \in (A \cap B) \land \forall x \in (A \cap B) \forall y \in (A \cap B) x +_{M} y \in (A \cap B)))$
48		eqid	$⊢ {Base}_{M} = {Base}_{M}$
49		eqid	$⊢ 0_{M} = 0_{M}$
50		eqid	$⊢ +_{M} = +_{M}$
51	48 49 50	issubm	$⊢ M \in Mnd \to (A \in SubMnd (M) \leftrightarrow (A \subseteq {Base}_{M} \land 0_{M} \in A \land \forall a \in A \forall b \in A a +_{M} b \in A))$
52	48 49 50	issubm	$⊢ M \in Mnd \to (B \in SubMnd (M) \leftrightarrow (B \subseteq {Base}_{M} \land 0_{M} \in B \land \forall a \in B \forall b \in B a +_{M} b \in B))$
53	51 52	anbi12d	$⊢ M \in Mnd \to ((A \in SubMnd (M) \land B \in SubMnd (M)) \leftrightarrow ((A \subseteq {Base}_{M} \land 0_{M} \in A \land \forall a \in A \forall b \in A a +_{M} b \in A) \land (B \subseteq {Base}_{M} \land 0_{M} \in B \land \forall a \in B \forall b \in B a +_{M} b \in B)))$
54	48 49 50	issubm	$⊢ M \in Mnd \to (A \cap B \in SubMnd (M) \leftrightarrow (A \cap B \subseteq {Base}_{M} \land 0_{M} \in (A \cap B) \land \forall x \in (A \cap B) \forall y \in (A \cap B) x +_{M} y \in (A \cap B)))$
55	47 53 54	3imtr4d	$⊢ M \in Mnd \to ((A \in SubMnd (M) \land B \in SubMnd (M)) \to A \cap B \in SubMnd (M))$
56	55	expd	$⊢ M \in Mnd \to (A \in SubMnd (M) \to (B \in SubMnd (M) \to A \cap B \in SubMnd (M)))$
57	1 56	mpcom	$⊢ A \in SubMnd (M) \to (B \in SubMnd (M) \to A \cap B \in SubMnd (M))$
58	57	imp	$⊢ (A \in SubMnd (M) \land B \in SubMnd (M)) \to A \cap B \in SubMnd (M)$

Metamath Proof Explorer

Theorem insubm

Proof