Metamath Proof Explorer

Theorem xpsrngd

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

Ref Expression
Hypotheses xpsrngd.y 
|- Y = ( S Xs. R )
xpsrngd.s 
|- ( ph -> S e. Rng )
xpsrngd.r 
|- ( ph -> R e. Rng )
Assertion xpsrngd 
|- ( ph -> Y e. Rng )

Proof

Step Hyp Ref Expression
1 xpsrngd.y 
 |-  Y = ( S Xs. R )
2 xpsrngd.s 
 |-  ( ph -> S e. Rng )
3 xpsrngd.r 
 |-  ( ph -> R e. Rng )
4 eqid 
 |-  ( Base ` S ) = ( Base ` S )
5 eqid 
 |-  ( Base ` R ) = ( Base ` R )
6 eqid 
 |-  ( x e. ( Base ` S ) , y e. ( Base ` R ) |-> { <. (/) , x >. , <. 1o , y >. } ) = ( x e. ( Base ` S ) , y e. ( Base ` R ) |-> { <. (/) , x >. , <. 1o , y >. } )
7 eqid 
 |-  ( Scalar ` S ) = ( Scalar ` S )
8 eqid 
 |-  ( ( Scalar ` S ) Xs_ { <. (/) , S >. , <. 1o , R >. } ) = ( ( Scalar ` S ) Xs_ { <. (/) , S >. , <. 1o , R >. } )
9 1 4 5 2 3 6 7 8 xpsval 
 |-  ( ph -> Y = ( `' ( x e. ( Base ` S ) , y e. ( Base ` R ) |-> { <. (/) , x >. , <. 1o , y >. } ) "s ( ( Scalar ` S ) Xs_ { <. (/) , S >. , <. 1o , R >. } ) ) )
10 6 xpsff1o2 
 |-  ( x e. ( Base ` S ) , y e. ( Base ` R ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ( ( Base ` S ) X. ( Base ` R ) ) -1-1-onto-> ran ( x e. ( Base ` S ) , y e. ( Base ` R ) |-> { <. (/) , x >. , <. 1o , y >. } )
11 1 4 5 2 3 6 7 8 xpsrnbas 
 |-  ( ph -> ran ( x e. ( Base ` S ) , y e. ( Base ` R ) |-> { <. (/) , x >. , <. 1o , y >. } ) = ( Base ` ( ( Scalar ` S ) Xs_ { <. (/) , S >. , <. 1o , R >. } ) ) )
12 11 f1oeq3d 
 |-  ( ph -> ( ( x e. ( Base ` S ) , y e. ( Base ` R ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ( ( Base ` S ) X. ( Base ` R ) ) -1-1-onto-> ran ( x e. ( Base ` S ) , y e. ( Base ` R ) |-> { <. (/) , x >. , <. 1o , y >. } ) <-> ( x e. ( Base ` S ) , y e. ( Base ` R ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ( ( Base ` S ) X. ( Base ` R ) ) -1-1-onto-> ( Base ` ( ( Scalar ` S ) Xs_ { <. (/) , S >. , <. 1o , R >. } ) ) ) )
13 10 12 mpbii 
 |-  ( ph -> ( x e. ( Base ` S ) , y e. ( Base ` R ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ( ( Base ` S ) X. ( Base ` R ) ) -1-1-onto-> ( Base ` ( ( Scalar ` S ) Xs_ { <. (/) , S >. , <. 1o , R >. } ) ) )
14 f1ocnv 
 |-  ( ( x e. ( Base ` S ) , y e. ( Base ` R ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ( ( Base ` S ) X. ( Base ` R ) ) -1-1-onto-> ( Base ` ( ( Scalar ` S ) Xs_ { <. (/) , S >. , <. 1o , R >. } ) ) -> `' ( x e. ( Base ` S ) , y e. ( Base ` R ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ( Base ` ( ( Scalar ` S ) Xs_ { <. (/) , S >. , <. 1o , R >. } ) ) -1-1-onto-> ( ( Base ` S ) X. ( Base ` R ) ) )
15 f1of1 
 |-  ( `' ( x e. ( Base ` S ) , y e. ( Base ` R ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ( Base ` ( ( Scalar ` S ) Xs_ { <. (/) , S >. , <. 1o , R >. } ) ) -1-1-onto-> ( ( Base ` S ) X. ( Base ` R ) ) -> `' ( x e. ( Base ` S ) , y e. ( Base ` R ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ( Base ` ( ( Scalar ` S ) Xs_ { <. (/) , S >. , <. 1o , R >. } ) ) -1-1-> ( ( Base ` S ) X. ( Base ` R ) ) )
16 13 14 15 3syl 
 |-  ( ph -> `' ( x e. ( Base ` S ) , y e. ( Base ` R ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ( Base ` ( ( Scalar ` S ) Xs_ { <. (/) , S >. , <. 1o , R >. } ) ) -1-1-> ( ( Base ` S ) X. ( Base ` R ) ) )
17 2on 
 |-  2o e. On
18 17 a1i 
 |-  ( ph -> 2o e. On )
19 fvexd 
 |-  ( ph -> ( Scalar ` S ) e. _V )
20 xpscf 
 |-  ( { <. (/) , S >. , <. 1o , R >. } : 2o --> Rng <-> ( S e. Rng /\ R e. Rng ) )
21 2 3 20 sylanbrc 
 |-  ( ph -> { <. (/) , S >. , <. 1o , R >. } : 2o --> Rng )
22 8 18 19 21 prdsrngd 
 |-  ( ph -> ( ( Scalar ` S ) Xs_ { <. (/) , S >. , <. 1o , R >. } ) e. Rng )
23 eqid 
 |-  ( `' ( x e. ( Base ` S ) , y e. ( Base ` R ) |-> { <. (/) , x >. , <. 1o , y >. } ) "s ( ( Scalar ` S ) Xs_ { <. (/) , S >. , <. 1o , R >. } ) ) = ( `' ( x e. ( Base ` S ) , y e. ( Base ` R ) |-> { <. (/) , x >. , <. 1o , y >. } ) "s ( ( Scalar ` S ) Xs_ { <. (/) , S >. , <. 1o , R >. } ) )
24 eqid 
 |-  ( Base ` ( ( Scalar ` S ) Xs_ { <. (/) , S >. , <. 1o , R >. } ) ) = ( Base ` ( ( Scalar ` S ) Xs_ { <. (/) , S >. , <. 1o , R >. } ) )
25 23 24 imasrngf1 
 |-  ( ( `' ( x e. ( Base ` S ) , y e. ( Base ` R ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ( Base ` ( ( Scalar ` S ) Xs_ { <. (/) , S >. , <. 1o , R >. } ) ) -1-1-> ( ( Base ` S ) X. ( Base ` R ) ) /\ ( ( Scalar ` S ) Xs_ { <. (/) , S >. , <. 1o , R >. } ) e. Rng ) -> ( `' ( x e. ( Base ` S ) , y e. ( Base ` R ) |-> { <. (/) , x >. , <. 1o , y >. } ) "s ( ( Scalar ` S ) Xs_ { <. (/) , S >. , <. 1o , R >. } ) ) e. Rng )
26 16 22 25 syl2anc 
 |-  ( ph -> ( `' ( x e. ( Base ` S ) , y e. ( Base ` R ) |-> { <. (/) , x >. , <. 1o , y >. } ) "s ( ( Scalar ` S ) Xs_ { <. (/) , S >. , <. 1o , R >. } ) ) e. Rng )
27 9 26 eqeltrd 
 |-  ( ph -> Y e. Rng )