rlocval

Description: Expand the value of the ring localization operation. (Contributed by Thierry Arnoux, 4-May-2025)

	Ref	Expression
Hypotheses	rlocval.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
	rlocval.2	⊢ 0 = ( 0_g ‘ 𝑅 )
	rlocval.3	⊢ · = ( ._r ‘ 𝑅 )
	rlocval.4	⊢ − = ( -_g ‘ 𝑅 )
	rlocval.5	⊢ + = ( +_g ‘ 𝑅 )
	rlocval.6	⊢ ≤ = ( le ‘ 𝑅 )
	rlocval.7	⊢ 𝐹 = ( Scalar ‘ 𝑅 )
	rlocval.8	⊢ 𝐾 = ( Base ‘ 𝐹 )
	rlocval.9	⊢ 𝐶 = ( ·_𝑠 ‘ 𝑅 )
	rlocval.10	⊢ 𝑊 = ( 𝐵 × 𝑆 )
	rlocval.11	⊢ ∼ = ( 𝑅 ~_RL 𝑆 )
	rlocval.12	⊢ 𝐽 = ( TopSet ‘ 𝑅 )
	rlocval.13	⊢ 𝐷 = ( dist ‘ 𝑅 )
	rlocval.14	⊢ ⊕ = ( 𝑎 ∈ 𝑊 , 𝑏 ∈ 𝑊 ↦ ⟨ ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) + ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) , ( ( 2^nd ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) ⟩ )
	rlocval.15	⊢ ⊗ = ( 𝑎 ∈ 𝑊 , 𝑏 ∈ 𝑊 ↦ ⟨ ( ( 1^st ‘ 𝑎 ) · ( 1^st ‘ 𝑏 ) ) , ( ( 2^nd ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) ⟩ )
	rlocval.16	⊢ × = ( 𝑘 ∈ 𝐾 , 𝑎 ∈ 𝑊 ↦ ⟨ ( 𝑘 𝐶 ( 1^st ‘ 𝑎 ) ) , ( 2^nd ‘ 𝑎 ) ⟩ )
	rlocval.17	⊢ ≲ = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ∧ ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) ≤ ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) }
	rlocval.18	⊢ 𝐸 = ( 𝑎 ∈ 𝑊 , 𝑏 ∈ 𝑊 ↦ ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) 𝐷 ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) )
	rlocval.19	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
	rlocval.20	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
Assertion	rlocval	⊢ ( 𝜑 → ( 𝑅 RLocal 𝑆 ) = ( ( ( { ⟨ ( Base ‘ ndx ) , 𝑊 ⟩ , ⟨ ( +_g ‘ ndx ) , ⊕ ⟩ , ⟨ ( ._r ‘ ndx ) , ⊗ ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝐹 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , × ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ∅ ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( 𝐽 ×_t ( 𝐽 ↾_t 𝑆 ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≲ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐸 ⟩ } ) /_s ∼ ) )

Proof

Step	Hyp	Ref	Expression
1		rlocval.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		rlocval.2	⊢ 0 = ( 0_g ‘ 𝑅 )
3		rlocval.3	⊢ · = ( ._r ‘ 𝑅 )
4		rlocval.4	⊢ − = ( -_g ‘ 𝑅 )
5		rlocval.5	⊢ + = ( +_g ‘ 𝑅 )
6		rlocval.6	⊢ ≤ = ( le ‘ 𝑅 )
7		rlocval.7	⊢ 𝐹 = ( Scalar ‘ 𝑅 )
8		rlocval.8	⊢ 𝐾 = ( Base ‘ 𝐹 )
9		rlocval.9	⊢ 𝐶 = ( ·_𝑠 ‘ 𝑅 )
10		rlocval.10	⊢ 𝑊 = ( 𝐵 × 𝑆 )
11		rlocval.11	⊢ ∼ = ( 𝑅 ~_RL 𝑆 )
12		rlocval.12	⊢ 𝐽 = ( TopSet ‘ 𝑅 )
13		rlocval.13	⊢ 𝐷 = ( dist ‘ 𝑅 )
14		rlocval.14	⊢ ⊕ = ( 𝑎 ∈ 𝑊 , 𝑏 ∈ 𝑊 ↦ ⟨ ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) + ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) , ( ( 2^nd ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) ⟩ )
15		rlocval.15	⊢ ⊗ = ( 𝑎 ∈ 𝑊 , 𝑏 ∈ 𝑊 ↦ ⟨ ( ( 1^st ‘ 𝑎 ) · ( 1^st ‘ 𝑏 ) ) , ( ( 2^nd ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) ⟩ )
16		rlocval.16	⊢ × = ( 𝑘 ∈ 𝐾 , 𝑎 ∈ 𝑊 ↦ ⟨ ( 𝑘 𝐶 ( 1^st ‘ 𝑎 ) ) , ( 2^nd ‘ 𝑎 ) ⟩ )
17		rlocval.17	⊢ ≲ = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ∧ ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) ≤ ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) }
18		rlocval.18	⊢ 𝐸 = ( 𝑎 ∈ 𝑊 , 𝑏 ∈ 𝑊 ↦ ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) 𝐷 ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) )
19		rlocval.19	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
20		rlocval.20	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
21	19	elexd	⊢ ( 𝜑 → 𝑅 ∈ V )
22	1	fvexi	⊢ 𝐵 ∈ V
23	22	a1i	⊢ ( 𝜑 → 𝐵 ∈ V )
24	23 20	ssexd	⊢ ( 𝜑 → 𝑆 ∈ V )
25		ovexd	⊢ ( 𝜑 → ( ( ( { ⟨ ( Base ‘ ndx ) , 𝑊 ⟩ , ⟨ ( +_g ‘ ndx ) , ⊕ ⟩ , ⟨ ( ._r ‘ ndx ) , ⊗ ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝐹 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , × ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ∅ ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( 𝐽 ×_t ( 𝐽 ↾_t 𝑆 ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≲ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐸 ⟩ } ) /_s ∼ ) ∈ V )
26		fvexd	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( ._r ‘ 𝑟 ) ∈ V )
27		fveq2	⊢ ( 𝑟 = 𝑅 → ( ._r ‘ 𝑟 ) = ( ._r ‘ 𝑅 ) )
28	27	adantr	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( ._r ‘ 𝑟 ) = ( ._r ‘ 𝑅 ) )
29	28 3	eqtr4di	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( ._r ‘ 𝑟 ) = · )
30		fvexd	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) → ( Base ‘ 𝑟 ) ∈ V )
31		vex	⊢ 𝑠 ∈ V
32	31	a1i	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) → 𝑠 ∈ V )
33	30 32	xpexd	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) → ( ( Base ‘ 𝑟 ) × 𝑠 ) ∈ V )
34		fveq2	⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
35	34	ad2antrr	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
36	35 1	eqtr4di	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) → ( Base ‘ 𝑟 ) = 𝐵 )
37		simplr	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) → 𝑠 = 𝑆 )
38	36 37	xpeq12d	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) → ( ( Base ‘ 𝑟 ) × 𝑠 ) = ( 𝐵 × 𝑆 ) )
39	38 10	eqtr4di	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) → ( ( Base ‘ 𝑟 ) × 𝑠 ) = 𝑊 )
40		simpr	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → 𝑤 = 𝑊 )
41	40	opeq2d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ⟨ ( Base ‘ ndx ) , 𝑤 ⟩ = ⟨ ( Base ‘ ndx ) , 𝑊 ⟩ )
42		simplll	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → 𝑟 = 𝑅 )
43	42	fveq2d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( +_g ‘ 𝑟 ) = ( +_g ‘ 𝑅 ) )
44	43 5	eqtr4di	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( +_g ‘ 𝑟 ) = + )
45		simplr	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → 𝑥 = · )
46	45	oveqd	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) = ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) )
47	45	oveqd	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) = ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) )
48	44 46 47	oveq123d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( +_g ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) = ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) + ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) )
49	45	oveqd	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) = ( ( 2^nd ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) )
50	48 49	opeq12d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ⟨ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( +_g ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ = ⟨ ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) + ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) , ( ( 2^nd ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) ⟩ )
51	40 40 50	mpoeq123dv	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( +_g ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) = ( 𝑎 ∈ 𝑊 , 𝑏 ∈ 𝑊 ↦ ⟨ ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) + ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) , ( ( 2^nd ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) ⟩ ) )
52	51 14	eqtr4di	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( +_g ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) = ⊕ )
53	52	opeq2d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ⟨ ( +_g ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( +_g ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) ⟩ = ⟨ ( +_g ‘ ndx ) , ⊕ ⟩ )
54	45	oveqd	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( ( 1^st ‘ 𝑎 ) 𝑥 ( 1^st ‘ 𝑏 ) ) = ( ( 1^st ‘ 𝑎 ) · ( 1^st ‘ 𝑏 ) ) )
55	54 49	opeq12d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ⟨ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 1^st ‘ 𝑏 ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ = ⟨ ( ( 1^st ‘ 𝑎 ) · ( 1^st ‘ 𝑏 ) ) , ( ( 2^nd ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) ⟩ )
56	40 40 55	mpoeq123dv	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 1^st ‘ 𝑏 ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) = ( 𝑎 ∈ 𝑊 , 𝑏 ∈ 𝑊 ↦ ⟨ ( ( 1^st ‘ 𝑎 ) · ( 1^st ‘ 𝑏 ) ) , ( ( 2^nd ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) ⟩ ) )
57	56 15	eqtr4di	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 1^st ‘ 𝑏 ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) = ⊗ )
58	57	opeq2d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ⟨ ( ._r ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 1^st ‘ 𝑏 ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) ⟩ = ⟨ ( ._r ‘ ndx ) , ⊗ ⟩ )
59	41 53 58	tpeq123d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → { ⟨ ( Base ‘ ndx ) , 𝑤 ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( +_g ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) ⟩ , ⟨ ( ._r ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 1^st ‘ 𝑏 ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝑊 ⟩ , ⟨ ( +_g ‘ ndx ) , ⊕ ⟩ , ⟨ ( ._r ‘ ndx ) , ⊗ ⟩ } )
60	42	fveq2d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( Scalar ‘ 𝑟 ) = ( Scalar ‘ 𝑅 ) )
61	60 7	eqtr4di	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( Scalar ‘ 𝑟 ) = 𝐹 )
62	61	opeq2d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑟 ) ⟩ = ⟨ ( Scalar ‘ ndx ) , 𝐹 ⟩ )
63	60	fveq2d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( Base ‘ ( Scalar ‘ 𝑟 ) ) = ( Base ‘ ( Scalar ‘ 𝑅 ) ) )
64	7	fveq2i	⊢ ( Base ‘ 𝐹 ) = ( Base ‘ ( Scalar ‘ 𝑅 ) )
65	8 64	eqtri	⊢ 𝐾 = ( Base ‘ ( Scalar ‘ 𝑅 ) )
66	63 65	eqtr4di	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( Base ‘ ( Scalar ‘ 𝑟 ) ) = 𝐾 )
67	42	fveq2d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( ·_𝑠 ‘ 𝑟 ) = ( ·_𝑠 ‘ 𝑅 ) )
68	67 9	eqtr4di	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( ·_𝑠 ‘ 𝑟 ) = 𝐶 )
69	68	oveqd	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( 𝑘 ( ·_𝑠 ‘ 𝑟 ) ( 1^st ‘ 𝑎 ) ) = ( 𝑘 𝐶 ( 1^st ‘ 𝑎 ) ) )
70	69	opeq1d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ⟨ ( 𝑘 ( ·_𝑠 ‘ 𝑟 ) ( 1^st ‘ 𝑎 ) ) , ( 2^nd ‘ 𝑎 ) ⟩ = ⟨ ( 𝑘 𝐶 ( 1^st ‘ 𝑎 ) ) , ( 2^nd ‘ 𝑎 ) ⟩ )
71	66 40 70	mpoeq123dv	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑟 ) ) , 𝑎 ∈ 𝑤 ↦ ⟨ ( 𝑘 ( ·_𝑠 ‘ 𝑟 ) ( 1^st ‘ 𝑎 ) ) , ( 2^nd ‘ 𝑎 ) ⟩ ) = ( 𝑘 ∈ 𝐾 , 𝑎 ∈ 𝑊 ↦ ⟨ ( 𝑘 𝐶 ( 1^st ‘ 𝑎 ) ) , ( 2^nd ‘ 𝑎 ) ⟩ ) )
72	71 16	eqtr4di	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑟 ) ) , 𝑎 ∈ 𝑤 ↦ ⟨ ( 𝑘 ( ·_𝑠 ‘ 𝑟 ) ( 1^st ‘ 𝑎 ) ) , ( 2^nd ‘ 𝑎 ) ⟩ ) = × )
73	72	opeq2d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ⟨ ( ·_𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑟 ) ) , 𝑎 ∈ 𝑤 ↦ ⟨ ( 𝑘 ( ·_𝑠 ‘ 𝑟 ) ( 1^st ‘ 𝑎 ) ) , ( 2^nd ‘ 𝑎 ) ⟩ ) ⟩ = ⟨ ( ·_𝑠 ‘ ndx ) , × ⟩ )
74		eqidd	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ⟨ ( ·_𝑖 ‘ ndx ) , ∅ ⟩ = ⟨ ( ·_𝑖 ‘ ndx ) , ∅ ⟩ )
75	62 73 74	tpeq123d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑟 ) ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑟 ) ) , 𝑎 ∈ 𝑤 ↦ ⟨ ( 𝑘 ( ·_𝑠 ‘ 𝑟 ) ( 1^st ‘ 𝑎 ) ) , ( 2^nd ‘ 𝑎 ) ⟩ ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ∅ ⟩ } = { ⟨ ( Scalar ‘ ndx ) , 𝐹 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , × ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ∅ ⟩ } )
76	59 75	uneq12d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( { ⟨ ( Base ‘ ndx ) , 𝑤 ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( +_g ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) ⟩ , ⟨ ( ._r ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 1^st ‘ 𝑏 ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑟 ) ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑟 ) ) , 𝑎 ∈ 𝑤 ↦ ⟨ ( 𝑘 ( ·_𝑠 ‘ 𝑟 ) ( 1^st ‘ 𝑎 ) ) , ( 2^nd ‘ 𝑎 ) ⟩ ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ∅ ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , 𝑊 ⟩ , ⟨ ( +_g ‘ ndx ) , ⊕ ⟩ , ⟨ ( ._r ‘ ndx ) , ⊗ ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝐹 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , × ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ∅ ⟩ } ) )
77	42	fveq2d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( TopSet ‘ 𝑟 ) = ( TopSet ‘ 𝑅 ) )
78	77 12	eqtr4di	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( TopSet ‘ 𝑟 ) = 𝐽 )
79	37	adantr	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → 𝑠 = 𝑆 )
80	78 79	oveq12d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( ( TopSet ‘ 𝑟 ) ↾_t 𝑠 ) = ( 𝐽 ↾_t 𝑆 ) )
81	78 80	oveq12d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( ( TopSet ‘ 𝑟 ) ×_t ( ( TopSet ‘ 𝑟 ) ↾_t 𝑠 ) ) = ( 𝐽 ×_t ( 𝐽 ↾_t 𝑆 ) ) )
82	81	opeq2d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ⟨ ( TopSet ‘ ndx ) , ( ( TopSet ‘ 𝑟 ) ×_t ( ( TopSet ‘ 𝑟 ) ↾_t 𝑠 ) ) ⟩ = ⟨ ( TopSet ‘ ndx ) , ( 𝐽 ×_t ( 𝐽 ↾_t 𝑆 ) ) ⟩ )
83	40	eleq2d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( 𝑎 ∈ 𝑤 ↔ 𝑎 ∈ 𝑊 ) )
84	40	eleq2d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( 𝑏 ∈ 𝑤 ↔ 𝑏 ∈ 𝑊 ) )
85	83 84	anbi12d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( ( 𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤 ) ↔ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) )
86	42	fveq2d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( le ‘ 𝑟 ) = ( le ‘ 𝑅 ) )
87	86 6	eqtr4di	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( le ‘ 𝑟 ) = ≤ )
88	46 87 47	breq123d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( le ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ↔ ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) ≤ ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) )
89	85 88	anbi12d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( ( ( 𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤 ) ∧ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( le ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) ↔ ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ∧ ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) ≤ ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) ) )
90	89	opabbidv	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤 ) ∧ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( le ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ∧ ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) ≤ ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) } )
91	90 17	eqtr4di	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤 ) ∧ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( le ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) } = ≲ )
92	91	opeq2d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ⟨ ( le ‘ ndx ) , { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤 ) ∧ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( le ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) } ⟩ = ⟨ ( le ‘ ndx ) , ≲ ⟩ )
93	42	fveq2d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( dist ‘ 𝑟 ) = ( dist ‘ 𝑅 ) )
94	93 13	eqtr4di	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( dist ‘ 𝑟 ) = 𝐷 )
95	94 46 47	oveq123d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( dist ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) = ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) 𝐷 ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) )
96	40 40 95	mpoeq123dv	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( dist ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) ) = ( 𝑎 ∈ 𝑊 , 𝑏 ∈ 𝑊 ↦ ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) 𝐷 ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) ) )
97	96 18	eqtr4di	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( dist ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) ) = 𝐸 )
98	97	opeq2d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ⟨ ( dist ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( dist ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) ) ⟩ = ⟨ ( dist ‘ ndx ) , 𝐸 ⟩ )
99	82 92 98	tpeq123d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → { ⟨ ( TopSet ‘ ndx ) , ( ( TopSet ‘ 𝑟 ) ×_t ( ( TopSet ‘ 𝑟 ) ↾_t 𝑠 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤 ) ∧ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( le ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( dist ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) ) ⟩ } = { ⟨ ( TopSet ‘ ndx ) , ( 𝐽 ×_t ( 𝐽 ↾_t 𝑆 ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≲ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐸 ⟩ } )
100	76 99	uneq12d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( ( { ⟨ ( Base ‘ ndx ) , 𝑤 ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( +_g ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) ⟩ , ⟨ ( ._r ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 1^st ‘ 𝑏 ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑟 ) ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑟 ) ) , 𝑎 ∈ 𝑤 ↦ ⟨ ( 𝑘 ( ·_𝑠 ‘ 𝑟 ) ( 1^st ‘ 𝑎 ) ) , ( 2^nd ‘ 𝑎 ) ⟩ ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ∅ ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopSet ‘ 𝑟 ) ×_t ( ( TopSet ‘ 𝑟 ) ↾_t 𝑠 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤 ) ∧ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( le ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( dist ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) ) ⟩ } ) = ( ( { ⟨ ( Base ‘ ndx ) , 𝑊 ⟩ , ⟨ ( +_g ‘ ndx ) , ⊕ ⟩ , ⟨ ( ._r ‘ ndx ) , ⊗ ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝐹 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , × ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ∅ ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( 𝐽 ×_t ( 𝐽 ↾_t 𝑆 ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≲ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐸 ⟩ } ) )
101	42 79	oveq12d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( 𝑟 ~_RL 𝑠 ) = ( 𝑅 ~_RL 𝑆 ) )
102	101 11	eqtr4di	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( 𝑟 ~_RL 𝑠 ) = ∼ )
103	100 102	oveq12d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( ( ( { ⟨ ( Base ‘ ndx ) , 𝑤 ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( +_g ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) ⟩ , ⟨ ( ._r ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 1^st ‘ 𝑏 ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑟 ) ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑟 ) ) , 𝑎 ∈ 𝑤 ↦ ⟨ ( 𝑘 ( ·_𝑠 ‘ 𝑟 ) ( 1^st ‘ 𝑎 ) ) , ( 2^nd ‘ 𝑎 ) ⟩ ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ∅ ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopSet ‘ 𝑟 ) ×_t ( ( TopSet ‘ 𝑟 ) ↾_t 𝑠 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤 ) ∧ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( le ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( dist ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) ) ⟩ } ) /_s ( 𝑟 ~_RL 𝑠 ) ) = ( ( ( { ⟨ ( Base ‘ ndx ) , 𝑊 ⟩ , ⟨ ( +_g ‘ ndx ) , ⊕ ⟩ , ⟨ ( ._r ‘ ndx ) , ⊗ ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝐹 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , × ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ∅ ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( 𝐽 ×_t ( 𝐽 ↾_t 𝑆 ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≲ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐸 ⟩ } ) /_s ∼ ) )
104	33 39 103	csbied2	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) → ⦋ ( ( Base ‘ 𝑟 ) × 𝑠 ) / 𝑤 ⦌ ( ( ( { ⟨ ( Base ‘ ndx ) , 𝑤 ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( +_g ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) ⟩ , ⟨ ( ._r ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 1^st ‘ 𝑏 ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑟 ) ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑟 ) ) , 𝑎 ∈ 𝑤 ↦ ⟨ ( 𝑘 ( ·_𝑠 ‘ 𝑟 ) ( 1^st ‘ 𝑎 ) ) , ( 2^nd ‘ 𝑎 ) ⟩ ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ∅ ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopSet ‘ 𝑟 ) ×_t ( ( TopSet ‘ 𝑟 ) ↾_t 𝑠 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤 ) ∧ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( le ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( dist ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) ) ⟩ } ) /_s ( 𝑟 ~_RL 𝑠 ) ) = ( ( ( { ⟨ ( Base ‘ ndx ) , 𝑊 ⟩ , ⟨ ( +_g ‘ ndx ) , ⊕ ⟩ , ⟨ ( ._r ‘ ndx ) , ⊗ ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝐹 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , × ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ∅ ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( 𝐽 ×_t ( 𝐽 ↾_t 𝑆 ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≲ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐸 ⟩ } ) /_s ∼ ) )
105	26 29 104	csbied2	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ⦋ ( ._r ‘ 𝑟 ) / 𝑥 ⦌ ⦋ ( ( Base ‘ 𝑟 ) × 𝑠 ) / 𝑤 ⦌ ( ( ( { ⟨ ( Base ‘ ndx ) , 𝑤 ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( +_g ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) ⟩ , ⟨ ( ._r ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 1^st ‘ 𝑏 ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑟 ) ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑟 ) ) , 𝑎 ∈ 𝑤 ↦ ⟨ ( 𝑘 ( ·_𝑠 ‘ 𝑟 ) ( 1^st ‘ 𝑎 ) ) , ( 2^nd ‘ 𝑎 ) ⟩ ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ∅ ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopSet ‘ 𝑟 ) ×_t ( ( TopSet ‘ 𝑟 ) ↾_t 𝑠 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤 ) ∧ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( le ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( dist ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) ) ⟩ } ) /_s ( 𝑟 ~_RL 𝑠 ) ) = ( ( ( { ⟨ ( Base ‘ ndx ) , 𝑊 ⟩ , ⟨ ( +_g ‘ ndx ) , ⊕ ⟩ , ⟨ ( ._r ‘ ndx ) , ⊗ ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝐹 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , × ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ∅ ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( 𝐽 ×_t ( 𝐽 ↾_t 𝑆 ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≲ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐸 ⟩ } ) /_s ∼ ) )
106		df-rloc	⊢ RLocal = ( 𝑟 ∈ V , 𝑠 ∈ V ↦ ⦋ ( ._r ‘ 𝑟 ) / 𝑥 ⦌ ⦋ ( ( Base ‘ 𝑟 ) × 𝑠 ) / 𝑤 ⦌ ( ( ( { ⟨ ( Base ‘ ndx ) , 𝑤 ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( +_g ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) ⟩ , ⟨ ( ._r ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ⟨ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 1^st ‘ 𝑏 ) ) , ( ( 2^nd ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ⟩ ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑟 ) ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑟 ) ) , 𝑎 ∈ 𝑤 ↦ ⟨ ( 𝑘 ( ·_𝑠 ‘ 𝑟 ) ( 1^st ‘ 𝑎 ) ) , ( 2^nd ‘ 𝑎 ) ⟩ ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ∅ ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopSet ‘ 𝑟 ) ×_t ( ( TopSet ‘ 𝑟 ) ↾_t 𝑠 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤 ) ∧ ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( le ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑎 ∈ 𝑤 , 𝑏 ∈ 𝑤 ↦ ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( dist ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) ) ⟩ } ) /_s ( 𝑟 ~_RL 𝑠 ) ) )
107	105 106	ovmpoga	⊢ ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ∧ ( ( ( { ⟨ ( Base ‘ ndx ) , 𝑊 ⟩ , ⟨ ( +_g ‘ ndx ) , ⊕ ⟩ , ⟨ ( ._r ‘ ndx ) , ⊗ ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝐹 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , × ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ∅ ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( 𝐽 ×_t ( 𝐽 ↾_t 𝑆 ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≲ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐸 ⟩ } ) /_s ∼ ) ∈ V ) → ( 𝑅 RLocal 𝑆 ) = ( ( ( { ⟨ ( Base ‘ ndx ) , 𝑊 ⟩ , ⟨ ( +_g ‘ ndx ) , ⊕ ⟩ , ⟨ ( ._r ‘ ndx ) , ⊗ ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝐹 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , × ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ∅ ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( 𝐽 ×_t ( 𝐽 ↾_t 𝑆 ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≲ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐸 ⟩ } ) /_s ∼ ) )
108	21 24 25 107	syl3anc	⊢ ( 𝜑 → ( 𝑅 RLocal 𝑆 ) = ( ( ( { ⟨ ( Base ‘ ndx ) , 𝑊 ⟩ , ⟨ ( +_g ‘ ndx ) , ⊕ ⟩ , ⟨ ( ._r ‘ ndx ) , ⊗ ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝐹 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , × ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ∅ ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( 𝐽 ×_t ( 𝐽 ↾_t 𝑆 ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≲ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐸 ⟩ } ) /_s ∼ ) )

Metamath Proof Explorer

Theorem rlocval

Proof