xpsms

Description: A binary product of metric spaces is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015)

		Ref	Expression
	Hypothesis	xpsms.t	$⊢ T = R \times_{𝑠} S$
	Assertion	xpsms	$⊢ (R \in MetSp \land S \in MetSp) \to T \in MetSp$

Proof

Step	Hyp	Ref	Expression
1		xpsms.t	$⊢ T = R \times_{𝑠} S$
2		eqid	$⊢ {Base}_{R} = {Base}_{R}$
3		eqid	$⊢ {Base}_{S} = {Base}_{S}$
4		simpl	$⊢ (R \in MetSp \land S \in MetSp) \to R \in MetSp$
5		simpr	$⊢ (R \in MetSp \land S \in MetSp) \to S \in MetSp$
6		eqid	$⊢ (x \in {Base}_{R}, y \in {Base}_{S} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) = (x \in {Base}_{R}, y \in {Base}_{S} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})$
7		eqid	$⊢ Scalar (R) = Scalar (R)$
8		eqid	$⊢ Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} = Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\}$
9	1 2 3 4 5 6 7 8	xpsval	$⊢ (R \in MetSp \land S \in MetSp) \to T = {(x \in {Base}_{R}, y \in {Base}_{S} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} “_{𝑠} (Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})$
10	1 2 3 4 5 6 7 8	xpsrnbas	$⊢ (R \in MetSp \land S \in MetSp) \to ran (x \in {Base}_{R}, y \in {Base}_{S} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) = {Base}_{(Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\})}$
11	6	xpsff1o2	$⊢ (x \in {Base}_{R}, y \in {Base}_{S} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) : {Base}_{R} \times {Base}_{S} \underset{1-1 onto}{⟶} ran (x \in {Base}_{R}, y \in {Base}_{S} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})$
12		f1ocnv	$⊢ (x \in {Base}_{R}, y \in {Base}_{S} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) : {Base}_{R} \times {Base}_{S} \underset{1-1 onto}{⟶} ran (x \in {Base}_{R}, y \in {Base}_{S} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) \to {(x \in {Base}_{R}, y \in {Base}_{S} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} : ran (x \in {Base}_{R}, y \in {Base}_{S} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) \underset{1-1 onto}{⟶} {Base}_{R} \times {Base}_{S}$
13	11 12	mp1i	$⊢ (R \in MetSp \land S \in MetSp) \to {(x \in {Base}_{R}, y \in {Base}_{S} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})}^{-1} : ran (x \in {Base}_{R}, y \in {Base}_{S} ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\}) \underset{1-1 onto}{⟶} {Base}_{R} \times {Base}_{S}$
14		fvexd	$⊢ (R \in MetSp \land S \in MetSp) \to Scalar (R) \in V$
15		2onn	$⊢ 2_{𝑜} \in ω$
16		nnfi	$⊢ 2_{𝑜} \in ω \to 2_{𝑜} \in Fin$
17	15 16	mp1i	$⊢ (R \in MetSp \land S \in MetSp) \to 2_{𝑜} \in Fin$
18		xpscf	$⊢ \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} : 2_{𝑜} ⟶ MetSp \leftrightarrow (R \in MetSp \land S \in MetSp)$
19	18	biimpri	$⊢ (R \in MetSp \land S \in MetSp) \to \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} : 2_{𝑜} ⟶ MetSp$
20	8	prdsms	$⊢ (Scalar (R) \in V \land 2_{𝑜} \in Fin \land \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} : 2_{𝑜} ⟶ MetSp) \to Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} \in MetSp$
21	14 17 19 20	syl3anc	$⊢ (R \in MetSp \land S \in MetSp) \to Scalar (R) ⨉_{𝑠} \{⟨\emptyset, R⟩, ⟨1_{𝑜}, S⟩\} \in MetSp$
22	9 10 13 21	imasf1oms	$⊢ (R \in MetSp \land S \in MetSp) \to T \in MetSp$

Metamath Proof Explorer

Theorem xpsms

Proof