xpsring1d

Description: The multiplicative identity element of a binary product of rings. (Contributed by AV, 16-Mar-2025)

	Ref	Expression
Hypotheses	xpsringd.y	$⊢ Y = S \times_{𝑠} R$
	xpsringd.s	$⊢ φ \to S \in Ring$
	xpsringd.r	$⊢ φ \to R \in Ring$
Assertion	xpsring1d	$⊢ φ \to 1_{Y} = ⟨1_{S}, 1_{R}⟩$

Proof

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

Metamath Proof Explorer

Theorem xpsring1d

Proof