This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )