rlocbas

Description: The base set of a ring localization. (Contributed by Thierry Arnoux, 4-May-2025)

	Ref	Expression
Hypotheses	rlocbas.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	rlocbas.1	⊢ 0 = ( 0_g ‘ 𝑅 )
	rlocbas.2	⊢ · = ( ._r ‘ 𝑅 )
	rlocbas.3	⊢ − = ( -_g ‘ 𝑅 )
	rlocbas.w	⊢ 𝑊 = ( 𝐵 × 𝑆 )
	rlocbas.l	⊢ 𝐿 = ( 𝑅 RLocal 𝑆 )
	rlocbas.4	⊢ ∼ = ( 𝑅 ~_RL 𝑆 )
	rlocbas.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
	rlocbas.s	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
Assertion	rlocbas	⊢ ( 𝜑 → ( 𝑊 / ∼ ) = ( Base ‘ 𝐿 ) )

Proof

Step	Hyp	Ref	Expression
1		rlocbas.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		rlocbas.1	⊢ 0 = ( 0_g ‘ 𝑅 )
3		rlocbas.2	⊢ · = ( ._r ‘ 𝑅 )
4		rlocbas.3	⊢ − = ( -_g ‘ 𝑅 )
5		rlocbas.w	⊢ 𝑊 = ( 𝐵 × 𝑆 )
6		rlocbas.l	⊢ 𝐿 = ( 𝑅 RLocal 𝑆 )
7		rlocbas.4	⊢ ∼ = ( 𝑅 ~_RL 𝑆 )
8		rlocbas.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
9		rlocbas.s	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
10		eqid	⊢ ( +_g ‘ 𝑅 ) = ( +_g ‘ 𝑅 )
11		eqid	⊢ ( le ‘ 𝑅 ) = ( le ‘ 𝑅 )
12		eqid	⊢ ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑅 )
13		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑅 ) ) = ( Base ‘ ( Scalar ‘ 𝑅 ) )
14		eqid	⊢ ( ·_𝑠 ‘ 𝑅 ) = ( ·_𝑠 ‘ 𝑅 )
15		eqid	⊢ ( TopSet ‘ 𝑅 ) = ( TopSet ‘ 𝑅 )
16		eqid	⊢ ( dist ‘ 𝑅 ) = ( dist ‘ 𝑅 )
17		eqid	⊢ ( 𝑎 ∈ 𝑊 , 𝑏 ∈ 𝑊 ↦ ⟨ ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) ( +_g ‘ 𝑅 ) ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) , ( ( 2^nd ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) ⟩ ) = ( 𝑎 ∈ 𝑊 , 𝑏 ∈ 𝑊 ↦ ⟨ ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) ( +_g ‘ 𝑅 ) ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) , ( ( 2^nd ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) ⟩ )
18		eqid	⊢ ( 𝑎 ∈ 𝑊 , 𝑏 ∈ 𝑊 ↦ ⟨ ( ( 1^st ‘ 𝑎 ) · ( 1^st ‘ 𝑏 ) ) , ( ( 2^nd ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) ⟩ ) = ( 𝑎 ∈ 𝑊 , 𝑏 ∈ 𝑊 ↦ ⟨ ( ( 1^st ‘ 𝑎 ) · ( 1^st ‘ 𝑏 ) ) , ( ( 2^nd ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) ⟩ )
19		eqid	⊢ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) , 𝑎 ∈ 𝑊 ↦ ⟨ ( 𝑘 ( ·_𝑠 ‘ 𝑅 ) ( 1^st ‘ 𝑎 ) ) , ( 2^nd ‘ 𝑎 ) ⟩ ) = ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) , 𝑎 ∈ 𝑊 ↦ ⟨ ( 𝑘 ( ·_𝑠 ‘ 𝑅 ) ( 1^st ‘ 𝑎 ) ) , ( 2^nd ‘ 𝑎 ) ⟩ )
20		eqid	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ∧ ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) ( le ‘ 𝑅 ) ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ∧ ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) ( le ‘ 𝑅 ) ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) }
21		eqid	⊢ ( 𝑎 ∈ 𝑊 , 𝑏 ∈ 𝑊 ↦ ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) ( dist ‘ 𝑅 ) ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) ) = ( 𝑎 ∈ 𝑊 , 𝑏 ∈ 𝑊 ↦ ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) ( dist ‘ 𝑅 ) ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) )
22	1 2 3 4 10 11 12 13 14 5 7 15 16 17 18 19 20 21 8 9	rlocval	⊢ ( 𝜑 → ( 𝑅 RLocal 𝑆 ) = ( ( ( { ⟨ ( 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 ∼ ) )
23	6 22	eqtrid	⊢ ( 𝜑 → 𝐿 = ( ( ( { ⟨ ( 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 ∼ ) )
24		eqidd	⊢ ( 𝜑 → ( ( { ⟨ ( 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 ) , ( 𝑎 ∈ 𝑊 , 𝑏 ∈ 𝑊 ↦ ⟨ ( ( ( 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 ‘ 𝑎 ) ) ) ) ⟩ } ) )
25		eqid	⊢ ( ( { ⟨ ( 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 ) , ( 𝑎 ∈ 𝑊 , 𝑏 ∈ 𝑊 ↦ ⟨ ( ( ( 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 ‘ 𝑎 ) ) ) ) ⟩ } )
26	25	imasvalstr	⊢ ( ( { ⟨ ( 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 ‘ 𝑎 ) ) ) ) ⟩ } ) Struct ⟨ 1 , ; 1 2 ⟩
27		baseid	⊢ Base = Slot ( Base ‘ ndx )
28		snsstp1	⊢ { ⟨ ( Base ‘ ndx ) , 𝑊 ⟩ } ⊆ { ⟨ ( 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 ‘ 𝑏 ) ) ⟩ ) ⟩ }
29		ssun1	⊢ { ⟨ ( 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 ) , ( 𝑎 ∈ 𝑊 , 𝑏 ∈ 𝑊 ↦ ⟨ ( ( ( 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 ) , ∅ ⟩ } )
30		ssun1	⊢ ( { ⟨ ( 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 ) , ( 𝑎 ∈ 𝑊 , 𝑏 ∈ 𝑊 ↦ ⟨ ( ( ( 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 ‘ 𝑎 ) ) ) ) ⟩ } )
31	29 30	sstri	⊢ { ⟨ ( 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 ) , ( 𝑎 ∈ 𝑊 , 𝑏 ∈ 𝑊 ↦ ⟨ ( ( ( 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 ‘ 𝑎 ) ) ) ) ⟩ } )
32	28 31	sstri	⊢ { ⟨ ( Base ‘ ndx ) , 𝑊 ⟩ } ⊆ ( ( { ⟨ ( 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 ‘ 𝑎 ) ) ) ) ⟩ } )
33	1	fvexi	⊢ 𝐵 ∈ V
34	33	a1i	⊢ ( 𝜑 → 𝐵 ∈ V )
35	34 9	ssexd	⊢ ( 𝜑 → 𝑆 ∈ V )
36	34 35	xpexd	⊢ ( 𝜑 → ( 𝐵 × 𝑆 ) ∈ V )
37	5 36	eqeltrid	⊢ ( 𝜑 → 𝑊 ∈ V )
38		eqid	⊢ ( 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 ‘ 𝑎 ) ) ) ) ⟩ } ) ) = ( 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 ‘ 𝑎 ) ) ) ) ⟩ } ) )
39	24 26 27 32 37 38	strfv3	⊢ ( 𝜑 → ( 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 ‘ 𝑎 ) ) ) ) ⟩ } ) ) = 𝑊 )
40	39	eqcomd	⊢ ( 𝜑 → 𝑊 = ( 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 ‘ 𝑎 ) ) ) ) ⟩ } ) ) )
41	7	ovexi	⊢ ∼ ∈ V
42	41	a1i	⊢ ( 𝜑 → ∼ ∈ V )
43		tpex	⊢ { ⟨ ( 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 ‘ 𝑏 ) ) ⟩ ) ⟩ } ∈ V
44		tpex	⊢ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑅 ) ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑅 ) ) , 𝑎 ∈ 𝑊 ↦ ⟨ ( 𝑘 ( ·_𝑠 ‘ 𝑅 ) ( 1^st ‘ 𝑎 ) ) , ( 2^nd ‘ 𝑎 ) ⟩ ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ∅ ⟩ } ∈ V
45	43 44	unex	⊢ ( { ⟨ ( 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 ) , ∅ ⟩ } ) ∈ V
46		tpex	⊢ { ⟨ ( 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 ‘ 𝑎 ) ) ) ) ⟩ } ∈ V
47	45 46	unex	⊢ ( ( { ⟨ ( 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 ‘ 𝑎 ) ) ) ) ⟩ } ) ∈ V
48	47	a1i	⊢ ( 𝜑 → ( ( { ⟨ ( 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 ‘ 𝑎 ) ) ) ) ⟩ } ) ∈ V )
49	23 40 42 48	qusbas	⊢ ( 𝜑 → ( 𝑊 / ∼ ) = ( Base ‘ 𝐿 ) )

Metamath Proof Explorer

Theorem rlocbas

Proof