xpsmet

Description: The direct product of two metric spaces. Definition 14-1.5 of Gleason p. 225. (Contributed by NM, 20-Jun-2007) (Revised by Mario Carneiro, 20-Aug-2015)

	Ref	Expression
Hypotheses	xpsds.t	⊢ 𝑇 = ( 𝑅 ×_s 𝑆 )
	xpsds.x	⊢ 𝑋 = ( Base ‘ 𝑅 )
	xpsds.y	⊢ 𝑌 = ( Base ‘ 𝑆 )
	xpsds.1	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
	xpsds.2	⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
	xpsds.p	⊢ 𝑃 = ( dist ‘ 𝑇 )
	xpsds.m	⊢ 𝑀 = ( ( dist ‘ 𝑅 ) ↾ ( 𝑋 × 𝑋 ) )
	xpsds.n	⊢ 𝑁 = ( ( dist ‘ 𝑆 ) ↾ ( 𝑌 × 𝑌 ) )
	xpsmet.3	⊢ ( 𝜑 → 𝑀 ∈ ( Met ‘ 𝑋 ) )
	xpsmet.4	⊢ ( 𝜑 → 𝑁 ∈ ( Met ‘ 𝑌 ) )
Assertion	xpsmet	⊢ ( 𝜑 → 𝑃 ∈ ( Met ‘ ( 𝑋 × 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		xpsds.t	⊢ 𝑇 = ( 𝑅 ×_s 𝑆 )
2		xpsds.x	⊢ 𝑋 = ( Base ‘ 𝑅 )
3		xpsds.y	⊢ 𝑌 = ( Base ‘ 𝑆 )
4		xpsds.1	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
5		xpsds.2	⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
6		xpsds.p	⊢ 𝑃 = ( dist ‘ 𝑇 )
7		xpsds.m	⊢ 𝑀 = ( ( dist ‘ 𝑅 ) ↾ ( 𝑋 × 𝑋 ) )
8		xpsds.n	⊢ 𝑁 = ( ( dist ‘ 𝑆 ) ↾ ( 𝑌 × 𝑌 ) )
9		xpsmet.3	⊢ ( 𝜑 → 𝑀 ∈ ( Met ‘ 𝑋 ) )
10		xpsmet.4	⊢ ( 𝜑 → 𝑁 ∈ ( Met ‘ 𝑌 ) )
11		eqid	⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } )
12		eqid	⊢ ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑅 )
13		eqid	⊢ ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) = ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } )
14	1 2 3 4 5 11 12 13	xpsval	⊢ ( 𝜑 → 𝑇 = ( ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) “_s ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) )
15	1 2 3 4 5 11 12 13	xpsrnbas	⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) )
16	11	xpsff1o2	⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) –1-1-onto→ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } )
17		f1ocnv	⊢ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) –1-1-onto→ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) → ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) : ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) –1-1-onto→ ( 𝑋 × 𝑌 ) )
18	16 17	mp1i	⊢ ( 𝜑 → ^◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) : ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) –1-1-onto→ ( 𝑋 × 𝑌 ) )
19		ovexd	⊢ ( 𝜑 → ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ∈ V )
20		eqid	⊢ ( ( dist ‘ ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) ↾ ( ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) × ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ) ) = ( ( dist ‘ ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) ↾ ( ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) × ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ) )
21		eqid	⊢ ( ( Scalar ‘ 𝑅 ) X_s ( 𝑘 ∈ 2_o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) = ( ( Scalar ‘ 𝑅 ) X_s ( 𝑘 ∈ 2_o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) )
22		eqid	⊢ ( Base ‘ ( ( Scalar ‘ 𝑅 ) X_s ( 𝑘 ∈ 2_o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) X_s ( 𝑘 ∈ 2_o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) )
23		eqid	⊢ ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) = ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) )
24		eqid	⊢ ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) = ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) )
25		eqid	⊢ ( dist ‘ ( ( Scalar ‘ 𝑅 ) X_s ( 𝑘 ∈ 2_o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) = ( dist ‘ ( ( Scalar ‘ 𝑅 ) X_s ( 𝑘 ∈ 2_o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) )
26		fvexd	⊢ ( 𝜑 → ( Scalar ‘ 𝑅 ) ∈ V )
27		2onn	⊢ 2_o ∈ ω
28		nnfi	⊢ ( 2_o ∈ ω → 2_o ∈ Fin )
29	27 28	mp1i	⊢ ( 𝜑 → 2_o ∈ Fin )
30		fvexd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 2_o ) → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ∈ V )
31		elpri	⊢ ( 𝑘 ∈ { ∅ , 1_o } → ( 𝑘 = ∅ ∨ 𝑘 = 1_o ) )
32		df2o3	⊢ 2_o = { ∅ , 1_o }
33	31 32	eleq2s	⊢ ( 𝑘 ∈ 2_o → ( 𝑘 = ∅ ∨ 𝑘 = 1_o ) )
34	9	adantr	⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → 𝑀 ∈ ( Met ‘ 𝑋 ) )
35		fveq2	⊢ ( 𝑘 = ∅ → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) = ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ ∅ ) )
36		fvpr0o	⊢ ( 𝑅 ∈ 𝑉 → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ ∅ ) = 𝑅 )
37	4 36	syl	⊢ ( 𝜑 → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ ∅ ) = 𝑅 )
38	35 37	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) = 𝑅 )
39	38	fveq2d	⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) = ( dist ‘ 𝑅 ) )
40	38	fveq2d	⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) = ( Base ‘ 𝑅 ) )
41	40 2	eqtr4di	⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) = 𝑋 )
42	41	sqxpeqd	⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) = ( 𝑋 × 𝑋 ) )
43	39 42	reseq12d	⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) = ( ( dist ‘ 𝑅 ) ↾ ( 𝑋 × 𝑋 ) ) )
44	43 7	eqtr4di	⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) = 𝑀 )
45	41	fveq2d	⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → ( Met ‘ ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) = ( Met ‘ 𝑋 ) )
46	34 44 45	3eltr4d	⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) ∈ ( Met ‘ ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) )
47	10	adantr	⊢ ( ( 𝜑 ∧ 𝑘 = 1_o ) → 𝑁 ∈ ( Met ‘ 𝑌 ) )
48		fveq2	⊢ ( 𝑘 = 1_o → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) = ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 1_o ) )
49		fvpr1o	⊢ ( 𝑆 ∈ 𝑊 → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 1_o ) = 𝑆 )
50	5 49	syl	⊢ ( 𝜑 → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 1_o ) = 𝑆 )
51	48 50	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝑘 = 1_o ) → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) = 𝑆 )
52	51	fveq2d	⊢ ( ( 𝜑 ∧ 𝑘 = 1_o ) → ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) = ( dist ‘ 𝑆 ) )
53	51	fveq2d	⊢ ( ( 𝜑 ∧ 𝑘 = 1_o ) → ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) = ( Base ‘ 𝑆 ) )
54	53 3	eqtr4di	⊢ ( ( 𝜑 ∧ 𝑘 = 1_o ) → ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) = 𝑌 )
55	54	sqxpeqd	⊢ ( ( 𝜑 ∧ 𝑘 = 1_o ) → ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) = ( 𝑌 × 𝑌 ) )
56	52 55	reseq12d	⊢ ( ( 𝜑 ∧ 𝑘 = 1_o ) → ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) = ( ( dist ‘ 𝑆 ) ↾ ( 𝑌 × 𝑌 ) ) )
57	56 8	eqtr4di	⊢ ( ( 𝜑 ∧ 𝑘 = 1_o ) → ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) = 𝑁 )
58	54	fveq2d	⊢ ( ( 𝜑 ∧ 𝑘 = 1_o ) → ( Met ‘ ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) = ( Met ‘ 𝑌 ) )
59	47 57 58	3eltr4d	⊢ ( ( 𝜑 ∧ 𝑘 = 1_o ) → ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) ∈ ( Met ‘ ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) )
60	46 59	jaodan	⊢ ( ( 𝜑 ∧ ( 𝑘 = ∅ ∨ 𝑘 = 1_o ) ) → ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) ∈ ( Met ‘ ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) )
61	33 60	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 2_o ) → ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) ∈ ( Met ‘ ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) )
62	21 22 23 24 25 26 29 30 61	prdsmet	⊢ ( 𝜑 → ( dist ‘ ( ( Scalar ‘ 𝑅 ) X_s ( 𝑘 ∈ 2_o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) ∈ ( Met ‘ ( Base ‘ ( ( Scalar ‘ 𝑅 ) X_s ( 𝑘 ∈ 2_o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) ) )
63		fnpr2o	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } Fn 2_o )
64	4 5 63	syl2anc	⊢ ( 𝜑 → { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } Fn 2_o )
65		dffn5	⊢ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } Fn 2_o ↔ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } = ( 𝑘 ∈ 2_o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) )
66	64 65	sylib	⊢ ( 𝜑 → { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } = ( 𝑘 ∈ 2_o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) )
67	66	oveq2d	⊢ ( 𝜑 → ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) = ( ( Scalar ‘ 𝑅 ) X_s ( 𝑘 ∈ 2_o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) )
68	67	fveq2d	⊢ ( 𝜑 → ( dist ‘ ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) = ( dist ‘ ( ( Scalar ‘ 𝑅 ) X_s ( 𝑘 ∈ 2_o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) )
69	67	fveq2d	⊢ ( 𝜑 → ( Base ‘ ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) X_s ( 𝑘 ∈ 2_o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) )
70	15 69	eqtrd	⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) X_s ( 𝑘 ∈ 2_o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) )
71	70	fveq2d	⊢ ( 𝜑 → ( Met ‘ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ) = ( Met ‘ ( Base ‘ ( ( Scalar ‘ 𝑅 ) X_s ( 𝑘 ∈ 2_o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) ) )
72	62 68 71	3eltr4d	⊢ ( 𝜑 → ( dist ‘ ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) ∈ ( Met ‘ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ) )
73		ssid	⊢ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ⊆ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } )
74		metres2	⊢ ( ( ( dist ‘ ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) ∈ ( Met ‘ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ) ∧ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ⊆ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ) → ( ( dist ‘ ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) ↾ ( ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) × ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ) ) ∈ ( Met ‘ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ) )
75	72 73 74	sylancl	⊢ ( 𝜑 → ( ( dist ‘ ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) ↾ ( ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) × ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ) ) ∈ ( Met ‘ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ) )
76	14 15 18 19 20 6 75	imasf1omet	⊢ ( 𝜑 → 𝑃 ∈ ( Met ‘ ( 𝑋 × 𝑌 ) ) )

Metamath Proof Explorer

Theorem xpsmet

Proof