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 \times_{𝑠} R$
	xpsrngd.s	$⊢ φ \to S \in Rng$
	xpsrngd.r	$⊢ φ \to R \in Rng$
Assertion	xpsrngd	$⊢ φ \to Y \in Rng$

Proof

Step	Hyp	Ref	Expression
1		xpsrngd.y	$⊢ Y = S \times_{𝑠} R$
2		xpsrngd.s	$⊢ φ \to S \in Rng$
3		xpsrngd.r	$⊢ φ \to R \in Rng$
4		eqid	$⊢ {Base}_{S} = {Base}_{S}$
5		eqid	$⊢ {Base}_{R} = {Base}_{R}$
6		eqid	$⊢ (x \in {Base}_{S}, y \in {Base}_{R} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) = (x \in {Base}_{S}, y \in {Base}_{R} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})$
7		eqid	$⊢ Scalar (S) = Scalar (S)$
8		eqid	$⊢ Scalar (S) ⨉_{𝑠} \{⟨\emptyset, S⟩, ⟨1_{𝑜}, R⟩\} = Scalar (S) ⨉_{𝑠} \{⟨\emptyset, S⟩, ⟨1_{𝑜}, R⟩\}$
9	1 4 5 2 3 6 7 8	xpsval	$⊢ φ \to Y = {(x \in {Base}_{S}, y \in {Base}_{R} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} “_{𝑠} (Scalar (S) ⨉_{𝑠} \{⟨\emptyset, S⟩, ⟨1_{𝑜}, R⟩\})$
10	6	xpsff1o2	$⊢ (x \in {Base}_{S}, y \in {Base}_{R} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) : {Base}_{S} \times {Base}_{R} \underset{1-1 onto}{⟶} ran (x \in {Base}_{S}, y \in {Base}_{R} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})$
11	1 4 5 2 3 6 7 8	xpsrnbas	$⊢ φ \to ran (x \in {Base}_{S}, y \in {Base}_{R} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) = {Base}_{(Scalar (S) ⨉_{𝑠} \{⟨\emptyset, S⟩, ⟨1_{𝑜}, R⟩\})}$
12	11	f1oeq3d	$⊢ φ \to ((x \in {Base}_{S}, y \in {Base}_{R} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) : {Base}_{S} \times {Base}_{R} \underset{1-1 onto}{⟶} ran (x \in {Base}_{S}, y \in {Base}_{R} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) \leftrightarrow (x \in {Base}_{S}, y \in {Base}_{R} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) : {Base}_{S} \times {Base}_{R} \underset{1-1 onto}{⟶} {Base}_{(Scalar (S) ⨉_{𝑠} \{⟨\emptyset, S⟩, ⟨1_{𝑜}, R⟩\})})$
13	10 12	mpbii	$⊢ φ \to (x \in {Base}_{S}, y \in {Base}_{R} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) : {Base}_{S} \times {Base}_{R} \underset{1-1 onto}{⟶} {Base}_{(Scalar (S) ⨉_{𝑠} \{⟨\emptyset, S⟩, ⟨1_{𝑜}, R⟩\})}$
14		f1ocnv	$⊢ (x \in {Base}_{S}, y \in {Base}_{R} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) : {Base}_{S} \times {Base}_{R} \underset{1-1 onto}{⟶} {Base}_{(Scalar (S) ⨉_{𝑠} \{⟨\emptyset, S⟩, ⟨1_{𝑜}, R⟩\})} \to {(x \in {Base}_{S}, y \in {Base}_{R} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} : {Base}_{(Scalar (S) ⨉_{𝑠} \{⟨\emptyset, S⟩, ⟨1_{𝑜}, R⟩\})} \underset{1-1 onto}{⟶} {Base}_{S} \times {Base}_{R}$
15		f1of1	$⊢ {(x \in {Base}_{S}, y \in {Base}_{R} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} : {Base}_{(Scalar (S) ⨉_{𝑠} \{⟨\emptyset, S⟩, ⟨1_{𝑜}, R⟩\})} \underset{1-1 onto}{⟶} {Base}_{S} \times {Base}_{R} \to {(x \in {Base}_{S}, y \in {Base}_{R} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} : {Base}_{(Scalar (S) ⨉_{𝑠} \{⟨\emptyset, S⟩, ⟨1_{𝑜}, R⟩\})} \underset{1-1}{⟶} {Base}_{S} \times {Base}_{R}$
16	13 14 15	3syl	$⊢ φ \to {(x \in {Base}_{S}, y \in {Base}_{R} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} : {Base}_{(Scalar (S) ⨉_{𝑠} \{⟨\emptyset, S⟩, ⟨1_{𝑜}, R⟩\})} \underset{1-1}{⟶} {Base}_{S} \times {Base}_{R}$
17		2on	$⊢ 2_{𝑜} \in On$
18	17	a1i	$⊢ φ \to 2_{𝑜} \in On$
19		fvexd	$⊢ φ \to Scalar (S) \in V$
20		xpscf	$⊢ \{⟨\emptyset, S⟩, ⟨1_{𝑜}, R⟩\} : 2_{𝑜} ⟶ Rng \leftrightarrow (S \in Rng \land R \in Rng)$
21	2 3 20	sylanbrc	$⊢ φ \to \{⟨\emptyset, S⟩, ⟨1_{𝑜}, R⟩\} : 2_{𝑜} ⟶ Rng$
22	8 18 19 21	prdsrngd	$⊢ φ \to Scalar (S) ⨉_{𝑠} \{⟨\emptyset, S⟩, ⟨1_{𝑜}, R⟩\} \in Rng$
23		eqid	$⊢ {(x \in {Base}_{S}, y \in {Base}_{R} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} “_{𝑠} (Scalar (S) ⨉_{𝑠} \{⟨\emptyset, S⟩, ⟨1_{𝑜}, R⟩\}) = {(x \in {Base}_{S}, y \in {Base}_{R} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} “_{𝑠} (Scalar (S) ⨉_{𝑠} \{⟨\emptyset, S⟩, ⟨1_{𝑜}, R⟩\})$
24		eqid	$⊢ {Base}_{(Scalar (S) ⨉_{𝑠} \{⟨\emptyset, S⟩, ⟨1_{𝑜}, R⟩\})} = {Base}_{(Scalar (S) ⨉_{𝑠} \{⟨\emptyset, S⟩, ⟨1_{𝑜}, R⟩\})}$
25	23 24	imasrngf1	$⊢ ({(x \in {Base}_{S}, y \in {Base}_{R} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} : {Base}_{(Scalar (S) ⨉_{𝑠} \{⟨\emptyset, S⟩, ⟨1_{𝑜}, R⟩\})} \underset{1-1}{⟶} {Base}_{S} \times {Base}_{R} \land Scalar (S) ⨉_{𝑠} \{⟨\emptyset, S⟩, ⟨1_{𝑜}, R⟩\} \in Rng) \to {(x \in {Base}_{S}, y \in {Base}_{R} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} “_{𝑠} (Scalar (S) ⨉_{𝑠} \{⟨\emptyset, S⟩, ⟨1_{𝑜}, R⟩\}) \in Rng$
26	16 22 25	syl2anc	$⊢ φ \to {(x \in {Base}_{S}, y \in {Base}_{R} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} “_{𝑠} (Scalar (S) ⨉_{𝑠} \{⟨\emptyset, S⟩, ⟨1_{𝑜}, R⟩\}) \in Rng$
27	9 26	eqeltrd	$⊢ φ \to Y \in Rng$

Metamath Proof Explorer

Theorem xpsrngd

Proof