xpsxmetlem

	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 ‘ 𝑆 ) ↾ ( 𝑌 × 𝑌 ) )
	xpsds.3	⊢ ( 𝜑 → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) )
	xpsds.4	⊢ ( 𝜑 → 𝑁 ∈ ( ∞Met ‘ 𝑌 ) )
Assertion	xpsxmetlem	⊢ ( 𝜑 → ( dist ‘ ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) ∈ ( ∞Met ‘ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ) )

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		xpsds.3	⊢ ( 𝜑 → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) )
10		xpsds.4	⊢ ( 𝜑 → 𝑁 ∈ ( ∞Met ‘ 𝑌 ) )
11		eqid	⊢ ( ( Scalar ‘ 𝑅 ) X_s ( 𝑘 ∈ 2_o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) = ( ( Scalar ‘ 𝑅 ) X_s ( 𝑘 ∈ 2_o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) )
12		eqid	⊢ ( Base ‘ ( ( Scalar ‘ 𝑅 ) X_s ( 𝑘 ∈ 2_o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) X_s ( 𝑘 ∈ 2_o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) )
13		eqid	⊢ ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) = ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) )
14		eqid	⊢ ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) = ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) )
15		eqid	⊢ ( dist ‘ ( ( Scalar ‘ 𝑅 ) X_s ( 𝑘 ∈ 2_o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) = ( dist ‘ ( ( Scalar ‘ 𝑅 ) X_s ( 𝑘 ∈ 2_o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) )
16		fvexd	⊢ ( 𝜑 → ( Scalar ‘ 𝑅 ) ∈ V )
17		2on	⊢ 2_o ∈ On
18	17	a1i	⊢ ( 𝜑 → 2_o ∈ On )
19		fvexd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 2_o ) → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ∈ V )
20		elpri	⊢ ( 𝑘 ∈ { ∅ , 1_o } → ( 𝑘 = ∅ ∨ 𝑘 = 1_o ) )
21		df2o3	⊢ 2_o = { ∅ , 1_o }
22	20 21	eleq2s	⊢ ( 𝑘 ∈ 2_o → ( 𝑘 = ∅ ∨ 𝑘 = 1_o ) )
23	9	adantr	⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) )
24		fveq2	⊢ ( 𝑘 = ∅ → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) = ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ ∅ ) )
25		fvpr0o	⊢ ( 𝑅 ∈ 𝑉 → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ ∅ ) = 𝑅 )
26	4 25	syl	⊢ ( 𝜑 → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ ∅ ) = 𝑅 )
27	24 26	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) = 𝑅 )
28	27	fveq2d	⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) = ( dist ‘ 𝑅 ) )
29	27	fveq2d	⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) = ( Base ‘ 𝑅 ) )
30	29 2	eqtr4di	⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) = 𝑋 )
31	30	sqxpeqd	⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) = ( 𝑋 × 𝑋 ) )
32	28 31	reseq12d	⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) = ( ( dist ‘ 𝑅 ) ↾ ( 𝑋 × 𝑋 ) ) )
33	32 7	eqtr4di	⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) = 𝑀 )
34	30	fveq2d	⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → ( ∞Met ‘ ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) = ( ∞Met ‘ 𝑋 ) )
35	23 33 34	3eltr4d	⊢ ( ( 𝜑 ∧ 𝑘 = ∅ ) → ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) ∈ ( ∞Met ‘ ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) )
36	10	adantr	⊢ ( ( 𝜑 ∧ 𝑘 = 1_o ) → 𝑁 ∈ ( ∞Met ‘ 𝑌 ) )
37		fveq2	⊢ ( 𝑘 = 1_o → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) = ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 1_o ) )
38		fvpr1o	⊢ ( 𝑆 ∈ 𝑊 → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 1_o ) = 𝑆 )
39	5 38	syl	⊢ ( 𝜑 → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 1_o ) = 𝑆 )
40	37 39	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝑘 = 1_o ) → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) = 𝑆 )
41	40	fveq2d	⊢ ( ( 𝜑 ∧ 𝑘 = 1_o ) → ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) = ( dist ‘ 𝑆 ) )
42	40	fveq2d	⊢ ( ( 𝜑 ∧ 𝑘 = 1_o ) → ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) = ( Base ‘ 𝑆 ) )
43	42 3	eqtr4di	⊢ ( ( 𝜑 ∧ 𝑘 = 1_o ) → ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) = 𝑌 )
44	43	sqxpeqd	⊢ ( ( 𝜑 ∧ 𝑘 = 1_o ) → ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) = ( 𝑌 × 𝑌 ) )
45	41 44	reseq12d	⊢ ( ( 𝜑 ∧ 𝑘 = 1_o ) → ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) = ( ( dist ‘ 𝑆 ) ↾ ( 𝑌 × 𝑌 ) ) )
46	45 8	eqtr4di	⊢ ( ( 𝜑 ∧ 𝑘 = 1_o ) → ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) = 𝑁 )
47	43	fveq2d	⊢ ( ( 𝜑 ∧ 𝑘 = 1_o ) → ( ∞Met ‘ ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) = ( ∞Met ‘ 𝑌 ) )
48	36 46 47	3eltr4d	⊢ ( ( 𝜑 ∧ 𝑘 = 1_o ) → ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) ∈ ( ∞Met ‘ ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) )
49	35 48	jaodan	⊢ ( ( 𝜑 ∧ ( 𝑘 = ∅ ∨ 𝑘 = 1_o ) ) → ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) ∈ ( ∞Met ‘ ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) )
50	22 49	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 2_o ) → ( ( dist ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) × ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) ∈ ( ∞Met ‘ ( Base ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) )
51	11 12 13 14 15 16 18 19 50	prdsxmet	⊢ ( 𝜑 → ( dist ‘ ( ( Scalar ‘ 𝑅 ) X_s ( 𝑘 ∈ 2_o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) ∈ ( ∞Met ‘ ( Base ‘ ( ( Scalar ‘ 𝑅 ) X_s ( 𝑘 ∈ 2_o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) ) )
52		fnpr2o	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } Fn 2_o )
53	4 5 52	syl2anc	⊢ ( 𝜑 → { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } Fn 2_o )
54		dffn5	⊢ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } Fn 2_o ↔ { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } = ( 𝑘 ∈ 2_o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) )
55	53 54	sylib	⊢ ( 𝜑 → { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } = ( 𝑘 ∈ 2_o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) )
56	55	oveq2d	⊢ ( 𝜑 → ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) = ( ( Scalar ‘ 𝑅 ) X_s ( 𝑘 ∈ 2_o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) )
57	56	fveq2d	⊢ ( 𝜑 → ( dist ‘ ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) = ( dist ‘ ( ( Scalar ‘ 𝑅 ) X_s ( 𝑘 ∈ 2_o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) )
58		eqid	⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } )
59		eqid	⊢ ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑅 )
60		eqid	⊢ ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) = ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } )
61	1 2 3 4 5 58 59 60	xpsrnbas	⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) )
62	56	fveq2d	⊢ ( 𝜑 → ( Base ‘ ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) X_s ( 𝑘 ∈ 2_o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) )
63	61 62	eqtrd	⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) X_s ( 𝑘 ∈ 2_o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) )
64	63	fveq2d	⊢ ( 𝜑 → ( ∞Met ‘ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ) = ( ∞Met ‘ ( Base ‘ ( ( Scalar ‘ 𝑅 ) X_s ( 𝑘 ∈ 2_o ↦ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ‘ 𝑘 ) ) ) ) ) )
65	51 57 64	3eltr4d	⊢ ( 𝜑 → ( dist ‘ ( ( Scalar ‘ 𝑅 ) X_s { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1_o , 𝑆 ⟩ } ) ) ∈ ( ∞Met ‘ ran ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1_o , 𝑦 ⟩ } ) ) )

Metamath Proof Explorer

Theorem xpsxmetlem

Proof