Theorem imassca

Description: The scalar field of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015) (Revised by Thierry Arnoux, 16-Jun-2019)

	Ref	Expression
Hypotheses	imasbas.u	⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
	imasbas.v	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
	imasbas.f	⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
	imasbas.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
	imassca.g	⊢ 𝐺 = ( Scalar ‘ 𝑅 )
Assertion	imassca	⊢ ( 𝜑 → 𝐺 = ( Scalar ‘ 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		imasbas.u	⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
2		imasbas.v	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
3		imasbas.f	⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
4		imasbas.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
5		imassca.g	⊢ 𝐺 = ( Scalar ‘ 𝑅 )
6	5	fvexi	⊢ 𝐺 ∈ V
7		eqid	⊢ ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑈 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( .r ‘ 𝑈 ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝐺 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ ( Base ‘ 𝐺 ) , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 ( ·𝑠 ‘ 𝑅 ) 𝑞 ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝑝 ( ·𝑖 ‘ 𝑅 ) 𝑞 ) ⟩ } ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ⟩ , ⟨ ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( dist ‘ 𝑈 ) ⟩ } ) = ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑈 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( .r ‘ 𝑈 ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝐺 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ ( Base ‘ 𝐺 ) , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 ( ·𝑠 ‘ 𝑅 ) 𝑞 ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝑝 ( ·𝑖 ‘ 𝑅 ) 𝑞 ) ⟩ } ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ⟩ , ⟨ ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( dist ‘ 𝑈 ) ⟩ } )
8	7	imasvalstr	⊢ ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑈 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( .r ‘ 𝑈 ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝐺 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ ( Base ‘ 𝐺 ) , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 ( ·𝑠 ‘ 𝑅 ) 𝑞 ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝑝 ( ·𝑖 ‘ 𝑅 ) 𝑞 ) ⟩ } ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ⟩ , ⟨ ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( dist ‘ 𝑈 ) ⟩ } ) Struct ⟨ 1 , ; 1 2 ⟩
9		scaid	⊢ Scalar = Slot ( Scalar ‘ ndx )
10		snsstp1	⊢ { ⟨ ( Scalar ‘ ndx ) , 𝐺 ⟩ } ⊆ { ⟨ ( Scalar ‘ ndx ) , 𝐺 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ ( Base ‘ 𝐺 ) , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 ( ·𝑠 ‘ 𝑅 ) 𝑞 ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝑝 ( ·𝑖 ‘ 𝑅 ) 𝑞 ) ⟩ } ⟩ }
11		ssun2	⊢ { ⟨ ( Scalar ‘ ndx ) , 𝐺 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ ( Base ‘ 𝐺 ) , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 ( ·𝑠 ‘ 𝑅 ) 𝑞 ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝑝 ( ·𝑖 ‘ 𝑅 ) 𝑞 ) ⟩ } ⟩ } ⊆ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑈 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( .r ‘ 𝑈 ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝐺 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ ( Base ‘ 𝐺 ) , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 ( ·𝑠 ‘ 𝑅 ) 𝑞 ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝑝 ( ·𝑖 ‘ 𝑅 ) 𝑞 ) ⟩ } ⟩ } )
12	10 11	sstri	⊢ { ⟨ ( Scalar ‘ ndx ) , 𝐺 ⟩ } ⊆ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑈 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( .r ‘ 𝑈 ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝐺 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ ( Base ‘ 𝐺 ) , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 ( ·𝑠 ‘ 𝑅 ) 𝑞 ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝑝 ( ·𝑖 ‘ 𝑅 ) 𝑞 ) ⟩ } ⟩ } )
13		ssun1	⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑈 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( .r ‘ 𝑈 ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝐺 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ ( Base ‘ 𝐺 ) , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 ( ·𝑠 ‘ 𝑅 ) 𝑞 ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝑝 ( ·𝑖 ‘ 𝑅 ) 𝑞 ) ⟩ } ⟩ } ) ⊆ ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑈 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( .r ‘ 𝑈 ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝐺 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ ( Base ‘ 𝐺 ) , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 ( ·𝑠 ‘ 𝑅 ) 𝑞 ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝑝 ( ·𝑖 ‘ 𝑅 ) 𝑞 ) ⟩ } ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ⟩ , ⟨ ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( dist ‘ 𝑈 ) ⟩ } )
14	12 13	sstri	⊢ { ⟨ ( Scalar ‘ ndx ) , 𝐺 ⟩ } ⊆ ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑈 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( .r ‘ 𝑈 ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝐺 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ ( Base ‘ 𝐺 ) , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 ( ·𝑠 ‘ 𝑅 ) 𝑞 ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝑝 ( ·𝑖 ‘ 𝑅 ) 𝑞 ) ⟩ } ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ⟩ , ⟨ ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( dist ‘ 𝑈 ) ⟩ } )
15	8 9 14	strfv	⊢ ( 𝐺 ∈ V → 𝐺 = ( Scalar ‘ ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑈 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( .r ‘ 𝑈 ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝐺 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ ( Base ‘ 𝐺 ) , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 ( ·𝑠 ‘ 𝑅 ) 𝑞 ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝑝 ( ·𝑖 ‘ 𝑅 ) 𝑞 ) ⟩ } ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ⟩ , ⟨ ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( dist ‘ 𝑈 ) ⟩ } ) ) )
16	6 15	ax-mp	⊢ 𝐺 = ( Scalar ‘ ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑈 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( .r ‘ 𝑈 ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝐺 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ ( Base ‘ 𝐺 ) , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 ( ·𝑠 ‘ 𝑅 ) 𝑞 ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝑝 ( ·𝑖 ‘ 𝑅 ) 𝑞 ) ⟩ } ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ⟩ , ⟨ ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( dist ‘ 𝑈 ) ⟩ } ) )
17		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
18		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
19		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
20		eqid	⊢ ( ·𝑠 ‘ 𝑅 ) = ( ·𝑠 ‘ 𝑅 )
21		eqid	⊢ ( ·𝑖 ‘ 𝑅 ) = ( ·𝑖 ‘ 𝑅 )
22		eqid	⊢ ( TopOpen ‘ 𝑅 ) = ( TopOpen ‘ 𝑅 )
23		eqid	⊢ ( dist ‘ 𝑅 ) = ( dist ‘ 𝑅 )
24		eqid	⊢ ( le ‘ 𝑅 ) = ( le ‘ 𝑅 )
25		eqid	⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 )
26	1 2 3 4 17 25	imasplusg	⊢ ( 𝜑 → ( +g ‘ 𝑈 ) = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( +g ‘ 𝑅 ) 𝑞 ) ) ⟩ } )
27		eqid	⊢ ( .r ‘ 𝑈 ) = ( .r ‘ 𝑈 )
28	1 2 3 4 18 27	imasmulr	⊢ ( 𝜑 → ( .r ‘ 𝑈 ) = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 ( .r ‘ 𝑅 ) 𝑞 ) ) ⟩ } )
29		eqidd	⊢ ( 𝜑 → ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ ( Base ‘ 𝐺 ) , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 ( ·𝑠 ‘ 𝑅 ) 𝑞 ) ) ) = ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ ( Base ‘ 𝐺 ) , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 ( ·𝑠 ‘ 𝑅 ) 𝑞 ) ) ) )
30		eqidd	⊢ ( 𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝑝 ( ·𝑖 ‘ 𝑅 ) 𝑞 ) ⟩ } = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝑝 ( ·𝑖 ‘ 𝑅 ) 𝑞 ) ⟩ } )
31		eqidd	⊢ ( 𝜑 → ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) = ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) )
32		eqid	⊢ ( dist ‘ 𝑈 ) = ( dist ‘ 𝑈 )
33	1 2 3 4 23 32	imasds	⊢ ( 𝜑 → ( dist ‘ 𝑈 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ*𝑠 Σg ( ( dist ‘ 𝑅 ) ∘ 𝑔 ) ) ) , ℝ* , < ) ) )
34		eqidd	⊢ ( 𝜑 → ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) = ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) )
35	1 2 17 18 5 19 20 21 22 23 24 26 28 29 30 31 33 34 3 4	imasval	⊢ ( 𝜑 → 𝑈 = ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑈 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( .r ‘ 𝑈 ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝐺 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ ( Base ‘ 𝐺 ) , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 ( ·𝑠 ‘ 𝑅 ) 𝑞 ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝑝 ( ·𝑖 ‘ 𝑅 ) 𝑞 ) ⟩ } ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ⟩ , ⟨ ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( dist ‘ 𝑈 ) ⟩ } ) )
36	35	fveq2d	⊢ ( 𝜑 → ( Scalar ‘ 𝑈 ) = ( Scalar ‘ ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑈 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( .r ‘ 𝑈 ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝐺 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ∪ 𝑞 ∈ 𝑉 ( 𝑝 ∈ ( Base ‘ 𝐺 ) , 𝑥 ∈ { ( 𝐹 ‘ 𝑞 ) } ↦ ( 𝐹 ‘ ( 𝑝 ( ·𝑠 ‘ 𝑅 ) 𝑞 ) ) ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝑝 ( ·𝑖 ‘ 𝑅 ) 𝑞 ) ⟩ } ⟩ } ) ∪ { ⟨ ( TopSet ‘ ndx ) , ( ( TopOpen ‘ 𝑅 ) qTop 𝐹 ) ⟩ , ⟨ ( le ‘ ndx ) , ( ( 𝐹 ∘ ( le ‘ 𝑅 ) ) ∘ ◡ 𝐹 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( dist ‘ 𝑈 ) ⟩ } ) ) )
37	16 36	eqtr4id	⊢ ( 𝜑 → 𝐺 = ( Scalar ‘ 𝑈 ) )