Theorem xpsringd

Description: A product of two rings is a ring ( xpsmnd analog). (Contributed by AV, 28-Feb-2025)

	Ref	Expression
Hypotheses	xpsringd.y	⊢ 𝑌 = ( 𝑆 ×s 𝑅 )
	xpsringd.s	⊢ ( 𝜑 → 𝑆 ∈ Ring )
	xpsringd.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
Assertion	xpsringd	⊢ ( 𝜑 → 𝑌 ∈ Ring )

Proof

Step	Hyp	Ref	Expression
1		xpsringd.y	⊢ 𝑌 = ( 𝑆 ×s 𝑅 )
2		xpsringd.s	⊢ ( 𝜑 → 𝑆 ∈ Ring )
3		xpsringd.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
4		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
5		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6		eqid	⊢ ( 𝑥 ∈ ( Base ‘ 𝑆 ) , 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) = ( 𝑥 ∈ ( Base ‘ 𝑆 ) , 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
7		eqid	⊢ ( Scalar ‘ 𝑆 ) = ( Scalar ‘ 𝑆 )
8		eqid	⊢ ( ( Scalar ‘ 𝑆 ) Xs { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑅 ⟩ } ) = ( ( Scalar ‘ 𝑆 ) Xs { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑅 ⟩ } )
9	1 4 5 2 3 6 7 8	xpsval	⊢ ( 𝜑 → 𝑌 = ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑆 ) , 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) “s ( ( Scalar ‘ 𝑆 ) Xs { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑅 ⟩ } ) ) )
10	6	xpsff1o2	⊢ ( 𝑥 ∈ ( Base ‘ 𝑆 ) , 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑅 ) ) –1-1-onto→ ran ( 𝑥 ∈ ( Base ‘ 𝑆 ) , 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
11	1 4 5 2 3 6 7 8	xpsrnbas	⊢ ( 𝜑 → ran ( 𝑥 ∈ ( Base ‘ 𝑆 ) , 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) = ( Base ‘ ( ( Scalar ‘ 𝑆 ) Xs { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑅 ⟩ } ) ) )
12	11	f1oeq3d	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( Base ‘ 𝑆 ) , 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑅 ) ) –1-1-onto→ ran ( 𝑥 ∈ ( Base ‘ 𝑆 ) , 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑆 ) , 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑅 ) ) –1-1-onto→ ( Base ‘ ( ( Scalar ‘ 𝑆 ) Xs { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑅 ⟩ } ) ) ) )
13	10 12	mpbii	⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝑆 ) , 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑅 ) ) –1-1-onto→ ( Base ‘ ( ( Scalar ‘ 𝑆 ) Xs { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑅 ⟩ } ) ) )
14		f1ocnv	⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑆 ) , 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑅 ) ) –1-1-onto→ ( Base ‘ ( ( Scalar ‘ 𝑆 ) Xs { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑅 ⟩ } ) ) → ◡ ( 𝑥 ∈ ( Base ‘ 𝑆 ) , 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( Base ‘ ( ( Scalar ‘ 𝑆 ) Xs { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑅 ⟩ } ) ) –1-1-onto→ ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑅 ) ) )
15		f1of1	⊢ ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑆 ) , 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( Base ‘ ( ( Scalar ‘ 𝑆 ) Xs { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑅 ⟩ } ) ) –1-1-onto→ ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑅 ) ) → ◡ ( 𝑥 ∈ ( Base ‘ 𝑆 ) , 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( Base ‘ ( ( Scalar ‘ 𝑆 ) Xs { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑅 ⟩ } ) ) –1-1→ ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑅 ) ) )
16	13 14 15	3syl	⊢ ( 𝜑 → ◡ ( 𝑥 ∈ ( Base ‘ 𝑆 ) , 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( Base ‘ ( ( Scalar ‘ 𝑆 ) Xs { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑅 ⟩ } ) ) –1-1→ ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑅 ) ) )
17		2on	⊢ 2o ∈ On
18	17	a1i	⊢ ( 𝜑 → 2o ∈ On )
19		fvexd	⊢ ( 𝜑 → ( Scalar ‘ 𝑆 ) ∈ V )
20		xpscf	⊢ ( { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑅 ⟩ } : 2o ⟶ Ring ↔ ( 𝑆 ∈ Ring ∧ 𝑅 ∈ Ring ) )
21	2 3 20	sylanbrc	⊢ ( 𝜑 → { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑅 ⟩ } : 2o ⟶ Ring )
22	8 18 19 21	prdsringd	⊢ ( 𝜑 → ( ( Scalar ‘ 𝑆 ) Xs { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑅 ⟩ } ) ∈ Ring )
23		eqid	⊢ ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑆 ) , 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) “s ( ( Scalar ‘ 𝑆 ) Xs { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑅 ⟩ } ) ) = ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑆 ) , 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) “s ( ( Scalar ‘ 𝑆 ) Xs { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑅 ⟩ } ) )
24		eqid	⊢ ( Base ‘ ( ( Scalar ‘ 𝑆 ) Xs { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑅 ⟩ } ) ) = ( Base ‘ ( ( Scalar ‘ 𝑆 ) Xs { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑅 ⟩ } ) )
25	23 24	imasringf1	⊢ ( ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑆 ) , 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( Base ‘ ( ( Scalar ‘ 𝑆 ) Xs { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑅 ⟩ } ) ) –1-1→ ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑅 ) ) ∧ ( ( Scalar ‘ 𝑆 ) Xs { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑅 ⟩ } ) ∈ Ring ) → ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑆 ) , 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) “s ( ( Scalar ‘ 𝑆 ) Xs { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑅 ⟩ } ) ) ∈ Ring )
26	16 22 25	syl2anc	⊢ ( 𝜑 → ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑆 ) , 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) “s ( ( Scalar ‘ 𝑆 ) Xs { ⟨ ∅ , 𝑆 ⟩ , ⟨ 1o , 𝑅 ⟩ } ) ) ∈ Ring )
27	9 26	eqeltrd	⊢ ( 𝜑 → 𝑌 ∈ Ring )