xpsmnd0

Description: The identity element of a binary product of monoids. (Contributed by AV, 25-Feb-2025)

		Ref	Expression
	Hypothesis	xpsmnd0.t	$⊢ T = R \times_{𝑠} S$
	Assertion	xpsmnd0	$⊢ (R \in Mnd \land S \in Mnd) \to 0_{T} = ⟨0_{R}, 0_{S}⟩$

Proof

Step	Hyp	Ref	Expression
1		xpsmnd0.t	$⊢ T = R \times_{𝑠} S$
2		eqid	$⊢ {Base}_{T} = {Base}_{T}$
3		eqid	$⊢ 0_{T} = 0_{T}$
4		eqid	$⊢ +_{T} = +_{T}$
5		eqid	$⊢ {Base}_{R} = {Base}_{R}$
6		eqid	$⊢ 0_{R} = 0_{R}$
7	5 6	mndidcl	$⊢ R \in Mnd \to 0_{R} \in {Base}_{R}$
8	7	adantr	$⊢ (R \in Mnd \land S \in Mnd) \to 0_{R} \in {Base}_{R}$
9		eqid	$⊢ {Base}_{S} = {Base}_{S}$
10		eqid	$⊢ 0_{S} = 0_{S}$
11	9 10	mndidcl	$⊢ S \in Mnd \to 0_{S} \in {Base}_{S}$
12	11	adantl	$⊢ (R \in Mnd \land S \in Mnd) \to 0_{S} \in {Base}_{S}$
13	8 12	opelxpd	$⊢ (R \in Mnd \land S \in Mnd) \to ⟨0_{R}, 0_{S}⟩ \in ({Base}_{R} \times {Base}_{S})$
14		simpl	$⊢ (R \in Mnd \land S \in Mnd) \to R \in Mnd$
15		simpr	$⊢ (R \in Mnd \land S \in Mnd) \to S \in Mnd$
16	1 5 9 14 15	xpsbas	$⊢ (R \in Mnd \land S \in Mnd) \to {Base}_{R} \times {Base}_{S} = {Base}_{T}$
17	13 16	eleqtrd	$⊢ (R \in Mnd \land S \in Mnd) \to ⟨0_{R}, 0_{S}⟩ \in {Base}_{T}$
18	16	eleq2d	$⊢ (R \in Mnd \land S \in Mnd) \to (x \in ({Base}_{R} \times {Base}_{S}) \leftrightarrow x \in {Base}_{T})$
19		elxp2	$⊢ x \in ({Base}_{R} \times {Base}_{S}) \leftrightarrow \exists a \in {Base}_{R} \exists b \in {Base}_{S} x = ⟨a, b⟩$
20	14	adantr	$⊢ ((R \in Mnd \land S \in Mnd) \land (a \in {Base}_{R} \land b \in {Base}_{S})) \to R \in Mnd$
21	15	adantr	$⊢ ((R \in Mnd \land S \in Mnd) \land (a \in {Base}_{R} \land b \in {Base}_{S})) \to S \in Mnd$
22	8	adantr	$⊢ ((R \in Mnd \land S \in Mnd) \land (a \in {Base}_{R} \land b \in {Base}_{S})) \to 0_{R} \in {Base}_{R}$
23	12	adantr	$⊢ ((R \in Mnd \land S \in Mnd) \land (a \in {Base}_{R} \land b \in {Base}_{S})) \to 0_{S} \in {Base}_{S}$
24		simpl	$⊢ (a \in {Base}_{R} \land b \in {Base}_{S}) \to a \in {Base}_{R}$
25	24	adantl	$⊢ ((R \in Mnd \land S \in Mnd) \land (a \in {Base}_{R} \land b \in {Base}_{S})) \to a \in {Base}_{R}$
26		simpr	$⊢ (a \in {Base}_{R} \land b \in {Base}_{S}) \to b \in {Base}_{S}$
27	26	adantl	$⊢ ((R \in Mnd \land S \in Mnd) \land (a \in {Base}_{R} \land b \in {Base}_{S})) \to b \in {Base}_{S}$
28		eqid	$⊢ +_{R} = +_{R}$
29	5 28	mndcl	$⊢ (R \in Mnd \land 0_{R} \in {Base}_{R} \land a \in {Base}_{R}) \to 0_{R} +_{R} a \in {Base}_{R}$
30	20 22 25 29	syl3anc	$⊢ ((R \in Mnd \land S \in Mnd) \land (a \in {Base}_{R} \land b \in {Base}_{S})) \to 0_{R} +_{R} a \in {Base}_{R}$
31		eqid	$⊢ +_{S} = +_{S}$
32	9 31	mndcl	$⊢ (S \in Mnd \land 0_{S} \in {Base}_{S} \land b \in {Base}_{S}) \to 0_{S} +_{S} b \in {Base}_{S}$
33	21 23 27 32	syl3anc	$⊢ ((R \in Mnd \land S \in Mnd) \land (a \in {Base}_{R} \land b \in {Base}_{S})) \to 0_{S} +_{S} b \in {Base}_{S}$
34	1 5 9 20 21 22 23 25 27 30 33 28 31 4	xpsadd	$⊢ ((R \in Mnd \land S \in Mnd) \land (a \in {Base}_{R} \land b \in {Base}_{S})) \to ⟨0_{R}, 0_{S}⟩ +_{T} ⟨a, b⟩ = ⟨0_{R} +_{R} a, 0_{S} +_{S} b⟩$
35	5 28 6	mndlid	$⊢ (R \in Mnd \land a \in {Base}_{R}) \to 0_{R} +_{R} a = a$
36	14 24 35	syl2an	$⊢ ((R \in Mnd \land S \in Mnd) \land (a \in {Base}_{R} \land b \in {Base}_{S})) \to 0_{R} +_{R} a = a$
37	9 31 10	mndlid	$⊢ (S \in Mnd \land b \in {Base}_{S}) \to 0_{S} +_{S} b = b$
38	15 26 37	syl2an	$⊢ ((R \in Mnd \land S \in Mnd) \land (a \in {Base}_{R} \land b \in {Base}_{S})) \to 0_{S} +_{S} b = b$
39	36 38	opeq12d	$⊢ ((R \in Mnd \land S \in Mnd) \land (a \in {Base}_{R} \land b \in {Base}_{S})) \to ⟨0_{R} +_{R} a, 0_{S} +_{S} b⟩ = ⟨a, b⟩$
40	34 39	eqtrd	$⊢ ((R \in Mnd \land S \in Mnd) \land (a \in {Base}_{R} \land b \in {Base}_{S})) \to ⟨0_{R}, 0_{S}⟩ +_{T} ⟨a, b⟩ = ⟨a, b⟩$
41		oveq2	$⊢ x = ⟨a, b⟩ \to ⟨0_{R}, 0_{S}⟩ +_{T} x = ⟨0_{R}, 0_{S}⟩ +_{T} ⟨a, b⟩$
42		id	$⊢ x = ⟨a, b⟩ \to x = ⟨a, b⟩$
43	41 42	eqeq12d	$⊢ x = ⟨a, b⟩ \to (⟨0_{R}, 0_{S}⟩ +_{T} x = x \leftrightarrow ⟨0_{R}, 0_{S}⟩ +_{T} ⟨a, b⟩ = ⟨a, b⟩)$
44	40 43	syl5ibrcom	$⊢ ((R \in Mnd \land S \in Mnd) \land (a \in {Base}_{R} \land b \in {Base}_{S})) \to (x = ⟨a, b⟩ \to ⟨0_{R}, 0_{S}⟩ +_{T} x = x)$
45	44	rexlimdvva	$⊢ (R \in Mnd \land S \in Mnd) \to (\exists a \in {Base}_{R} \exists b \in {Base}_{S} x = ⟨a, b⟩ \to ⟨0_{R}, 0_{S}⟩ +_{T} x = x)$
46	19 45	biimtrid	$⊢ (R \in Mnd \land S \in Mnd) \to (x \in ({Base}_{R} \times {Base}_{S}) \to ⟨0_{R}, 0_{S}⟩ +_{T} x = x)$
47	18 46	sylbird	$⊢ (R \in Mnd \land S \in Mnd) \to (x \in {Base}_{T} \to ⟨0_{R}, 0_{S}⟩ +_{T} x = x)$
48	47	imp	$⊢ ((R \in Mnd \land S \in Mnd) \land x \in {Base}_{T}) \to ⟨0_{R}, 0_{S}⟩ +_{T} x = x$
49	5 28	mndcl	$⊢ (R \in Mnd \land a \in {Base}_{R} \land 0_{R} \in {Base}_{R}) \to a +_{R} 0_{R} \in {Base}_{R}$
50	20 25 22 49	syl3anc	$⊢ ((R \in Mnd \land S \in Mnd) \land (a \in {Base}_{R} \land b \in {Base}_{S})) \to a +_{R} 0_{R} \in {Base}_{R}$
51	9 31	mndcl	$⊢ (S \in Mnd \land b \in {Base}_{S} \land 0_{S} \in {Base}_{S}) \to b +_{S} 0_{S} \in {Base}_{S}$
52	21 27 23 51	syl3anc	$⊢ ((R \in Mnd \land S \in Mnd) \land (a \in {Base}_{R} \land b \in {Base}_{S})) \to b +_{S} 0_{S} \in {Base}_{S}$
53	1 5 9 20 21 25 27 22 23 50 52 28 31 4	xpsadd	$⊢ ((R \in Mnd \land S \in Mnd) \land (a \in {Base}_{R} \land b \in {Base}_{S})) \to ⟨a, b⟩ +_{T} ⟨0_{R}, 0_{S}⟩ = ⟨a +_{R} 0_{R}, b +_{S} 0_{S}⟩$
54	5 28 6	mndrid	$⊢ (R \in Mnd \land a \in {Base}_{R}) \to a +_{R} 0_{R} = a$
55	14 24 54	syl2an	$⊢ ((R \in Mnd \land S \in Mnd) \land (a \in {Base}_{R} \land b \in {Base}_{S})) \to a +_{R} 0_{R} = a$
56	9 31 10	mndrid	$⊢ (S \in Mnd \land b \in {Base}_{S}) \to b +_{S} 0_{S} = b$
57	15 26 56	syl2an	$⊢ ((R \in Mnd \land S \in Mnd) \land (a \in {Base}_{R} \land b \in {Base}_{S})) \to b +_{S} 0_{S} = b$
58	55 57	opeq12d	$⊢ ((R \in Mnd \land S \in Mnd) \land (a \in {Base}_{R} \land b \in {Base}_{S})) \to ⟨a +_{R} 0_{R}, b +_{S} 0_{S}⟩ = ⟨a, b⟩$
59	53 58	eqtrd	$⊢ ((R \in Mnd \land S \in Mnd) \land (a \in {Base}_{R} \land b \in {Base}_{S})) \to ⟨a, b⟩ +_{T} ⟨0_{R}, 0_{S}⟩ = ⟨a, b⟩$
60		oveq1	$⊢ x = ⟨a, b⟩ \to x +_{T} ⟨0_{R}, 0_{S}⟩ = ⟨a, b⟩ +_{T} ⟨0_{R}, 0_{S}⟩$
61	60 42	eqeq12d	$⊢ x = ⟨a, b⟩ \to (x +_{T} ⟨0_{R}, 0_{S}⟩ = x \leftrightarrow ⟨a, b⟩ +_{T} ⟨0_{R}, 0_{S}⟩ = ⟨a, b⟩)$
62	59 61	syl5ibrcom	$⊢ ((R \in Mnd \land S \in Mnd) \land (a \in {Base}_{R} \land b \in {Base}_{S})) \to (x = ⟨a, b⟩ \to x +_{T} ⟨0_{R}, 0_{S}⟩ = x)$
63	62	rexlimdvva	$⊢ (R \in Mnd \land S \in Mnd) \to (\exists a \in {Base}_{R} \exists b \in {Base}_{S} x = ⟨a, b⟩ \to x +_{T} ⟨0_{R}, 0_{S}⟩ = x)$
64	19 63	biimtrid	$⊢ (R \in Mnd \land S \in Mnd) \to (x \in ({Base}_{R} \times {Base}_{S}) \to x +_{T} ⟨0_{R}, 0_{S}⟩ = x)$
65	18 64	sylbird	$⊢ (R \in Mnd \land S \in Mnd) \to (x \in {Base}_{T} \to x +_{T} ⟨0_{R}, 0_{S}⟩ = x)$
66	65	imp	$⊢ ((R \in Mnd \land S \in Mnd) \land x \in {Base}_{T}) \to x +_{T} ⟨0_{R}, 0_{S}⟩ = x$
67	2 3 4 17 48 66	ismgmid2	$⊢ (R \in Mnd \land S \in Mnd) \to ⟨0_{R}, 0_{S}⟩ = 0_{T}$
68	67	eqcomd	$⊢ (R \in Mnd \land S \in Mnd) \to 0_{T} = ⟨0_{R}, 0_{S}⟩$

Metamath Proof Explorer

Theorem xpsmnd0

Proof