MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imasval Structured version   Visualization version   GIF version

Theorem imasval 17456
Description: Value of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 11-Jul-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 6-Oct-2020.)
Hypotheses
Ref Expression
imasval.u (πœ‘ β†’ π‘ˆ = (𝐹 β€œs 𝑅))
imasval.v (πœ‘ β†’ 𝑉 = (Baseβ€˜π‘…))
imasval.p + = (+gβ€˜π‘…)
imasval.m Γ— = (.rβ€˜π‘…)
imasval.g 𝐺 = (Scalarβ€˜π‘…)
imasval.k 𝐾 = (Baseβ€˜πΊ)
imasval.q Β· = ( ·𝑠 β€˜π‘…)
imasval.i , = (Β·π‘–β€˜π‘…)
imasval.j 𝐽 = (TopOpenβ€˜π‘…)
imasval.e 𝐸 = (distβ€˜π‘…)
imasval.n 𝑁 = (leβ€˜π‘…)
imasval.a (πœ‘ β†’ ✚ = βˆͺ 𝑝 ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 + π‘ž))⟩})
imasval.t (πœ‘ β†’ βˆ™ = βˆͺ 𝑝 ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 Γ— π‘ž))⟩})
imasval.s (πœ‘ β†’ βŠ— = βˆͺ π‘ž ∈ 𝑉 (𝑝 ∈ 𝐾, π‘₯ ∈ {(πΉβ€˜π‘ž)} ↦ (πΉβ€˜(𝑝 Β· π‘ž))))
imasval.w (πœ‘ β†’ 𝐼 = βˆͺ 𝑝 ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (𝑝 , π‘ž)⟩})
imasval.o (πœ‘ β†’ 𝑂 = (𝐽 qTop 𝐹))
imasval.d (πœ‘ β†’ 𝐷 = (π‘₯ ∈ 𝐡, 𝑦 ∈ 𝐡 ↦ inf(βˆͺ 𝑛 ∈ β„• ran (𝑔 ∈ {β„Ž ∈ ((𝑉 Γ— 𝑉) ↑m (1...𝑛)) ∣ ((πΉβ€˜(1st β€˜(β„Žβ€˜1))) = π‘₯ ∧ (πΉβ€˜(2nd β€˜(β„Žβ€˜π‘›))) = 𝑦 ∧ βˆ€π‘– ∈ (1...(𝑛 βˆ’ 1))(πΉβ€˜(2nd β€˜(β„Žβ€˜π‘–))) = (πΉβ€˜(1st β€˜(β„Žβ€˜(𝑖 + 1)))))} ↦ (ℝ*𝑠 Ξ£g (𝐸 ∘ 𝑔))), ℝ*, < )))
imasval.l (πœ‘ β†’ ≀ = ((𝐹 ∘ 𝑁) ∘ ◑𝐹))
imasval.f (πœ‘ β†’ 𝐹:𝑉–onto→𝐡)
imasval.r (πœ‘ β†’ 𝑅 ∈ 𝑍)
Assertion
Ref Expression
imasval (πœ‘ β†’ π‘ˆ = (({⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(+gβ€˜ndx), ✚ ⟩, ⟨(.rβ€˜ndx), βˆ™ ⟩} βˆͺ {⟨(Scalarβ€˜ndx), 𝐺⟩, ⟨( ·𝑠 β€˜ndx), βŠ— ⟩, ⟨(Β·π‘–β€˜ndx), 𝐼⟩}) βˆͺ {⟨(TopSetβ€˜ndx), π‘‚βŸ©, ⟨(leβ€˜ndx), ≀ ⟩, ⟨(distβ€˜ndx), 𝐷⟩}))
Distinct variable groups:   𝑔,β„Ž,𝑖,𝑛,𝑝,π‘ž,π‘₯,𝑦,𝐹   𝑅,𝑔,β„Ž,𝑖,𝑛,𝑝,π‘ž,π‘₯,𝑦   β„Ž,𝑉,𝑝,π‘ž   πœ‘,𝑔,β„Ž,𝑖,𝑛,𝑝,π‘ž,π‘₯,𝑦
Allowed substitution hints:   𝐡(π‘₯,𝑦,𝑔,β„Ž,𝑖,𝑛,π‘ž,𝑝)   𝐷(π‘₯,𝑦,𝑔,β„Ž,𝑖,𝑛,π‘ž,𝑝)   + (π‘₯,𝑦,𝑔,β„Ž,𝑖,𝑛,π‘ž,𝑝)   ✚ (π‘₯,𝑦,𝑔,β„Ž,𝑖,𝑛,π‘ž,𝑝)   βˆ™ (π‘₯,𝑦,𝑔,β„Ž,𝑖,𝑛,π‘ž,𝑝)   Β· (π‘₯,𝑦,𝑔,β„Ž,𝑖,𝑛,π‘ž,𝑝)   Γ— (π‘₯,𝑦,𝑔,β„Ž,𝑖,𝑛,π‘ž,𝑝)   βŠ— (π‘₯,𝑦,𝑔,β„Ž,𝑖,𝑛,π‘ž,𝑝)   π‘ˆ(π‘₯,𝑦,𝑔,β„Ž,𝑖,𝑛,π‘ž,𝑝)   𝐸(π‘₯,𝑦,𝑔,β„Ž,𝑖,𝑛,π‘ž,𝑝)   𝐺(π‘₯,𝑦,𝑔,β„Ž,𝑖,𝑛,π‘ž,𝑝)   , (π‘₯,𝑦,𝑔,β„Ž,𝑖,𝑛,π‘ž,𝑝)   𝐼(π‘₯,𝑦,𝑔,β„Ž,𝑖,𝑛,π‘ž,𝑝)   𝐽(π‘₯,𝑦,𝑔,β„Ž,𝑖,𝑛,π‘ž,𝑝)   𝐾(π‘₯,𝑦,𝑔,β„Ž,𝑖,𝑛,π‘ž,𝑝)   ≀ (π‘₯,𝑦,𝑔,β„Ž,𝑖,𝑛,π‘ž,𝑝)   𝑁(π‘₯,𝑦,𝑔,β„Ž,𝑖,𝑛,π‘ž,𝑝)   𝑂(π‘₯,𝑦,𝑔,β„Ž,𝑖,𝑛,π‘ž,𝑝)   𝑉(π‘₯,𝑦,𝑔,𝑖,𝑛)   𝑍(π‘₯,𝑦,𝑔,β„Ž,𝑖,𝑛,π‘ž,𝑝)

Proof of Theorem imasval
Dummy variables 𝑓 π‘Ÿ 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 imasval.u . 2 (πœ‘ β†’ π‘ˆ = (𝐹 β€œs 𝑅))
2 df-imas 17453 . . . 4 β€œs = (𝑓 ∈ V, π‘Ÿ ∈ V ↦ ⦋(Baseβ€˜π‘Ÿ) / π‘£β¦Œ(({⟨(Baseβ€˜ndx), ran π‘“βŸ©, ⟨(+gβ€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(+gβ€˜π‘Ÿ)π‘ž))⟩}⟩, ⟨(.rβ€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(.rβ€˜π‘Ÿ)π‘ž))⟩}⟩} βˆͺ {⟨(Scalarβ€˜ndx), (Scalarβ€˜π‘Ÿ)⟩, ⟨( ·𝑠 β€˜ndx), βˆͺ π‘ž ∈ 𝑣 (𝑝 ∈ (Baseβ€˜(Scalarβ€˜π‘Ÿ)), π‘₯ ∈ {(π‘“β€˜π‘ž)} ↦ (π‘“β€˜(𝑝( ·𝑠 β€˜π‘Ÿ)π‘ž)))⟩, ⟨(Β·π‘–β€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (𝑝(Β·π‘–β€˜π‘Ÿ)π‘ž)⟩}⟩}) βˆͺ {⟨(TopSetβ€˜ndx), ((TopOpenβ€˜π‘Ÿ) qTop 𝑓)⟩, ⟨(leβ€˜ndx), ((𝑓 ∘ (leβ€˜π‘Ÿ)) ∘ ◑𝑓)⟩, ⟨(distβ€˜ndx), (π‘₯ ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf(βˆͺ 𝑛 ∈ β„• ran (𝑔 ∈ {β„Ž ∈ ((𝑣 Γ— 𝑣) ↑m (1...𝑛)) ∣ ((π‘“β€˜(1st β€˜(β„Žβ€˜1))) = π‘₯ ∧ (π‘“β€˜(2nd β€˜(β„Žβ€˜π‘›))) = 𝑦 ∧ βˆ€π‘– ∈ (1...(𝑛 βˆ’ 1))(π‘“β€˜(2nd β€˜(β„Žβ€˜π‘–))) = (π‘“β€˜(1st β€˜(β„Žβ€˜(𝑖 + 1)))))} ↦ (ℝ*𝑠 Ξ£g ((distβ€˜π‘Ÿ) ∘ 𝑔))), ℝ*, < ))⟩}))
32a1i 11 . . 3 (πœ‘ β†’ β€œs = (𝑓 ∈ V, π‘Ÿ ∈ V ↦ ⦋(Baseβ€˜π‘Ÿ) / π‘£β¦Œ(({⟨(Baseβ€˜ndx), ran π‘“βŸ©, ⟨(+gβ€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(+gβ€˜π‘Ÿ)π‘ž))⟩}⟩, ⟨(.rβ€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(.rβ€˜π‘Ÿ)π‘ž))⟩}⟩} βˆͺ {⟨(Scalarβ€˜ndx), (Scalarβ€˜π‘Ÿ)⟩, ⟨( ·𝑠 β€˜ndx), βˆͺ π‘ž ∈ 𝑣 (𝑝 ∈ (Baseβ€˜(Scalarβ€˜π‘Ÿ)), π‘₯ ∈ {(π‘“β€˜π‘ž)} ↦ (π‘“β€˜(𝑝( ·𝑠 β€˜π‘Ÿ)π‘ž)))⟩, ⟨(Β·π‘–β€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (𝑝(Β·π‘–β€˜π‘Ÿ)π‘ž)⟩}⟩}) βˆͺ {⟨(TopSetβ€˜ndx), ((TopOpenβ€˜π‘Ÿ) qTop 𝑓)⟩, ⟨(leβ€˜ndx), ((𝑓 ∘ (leβ€˜π‘Ÿ)) ∘ ◑𝑓)⟩, ⟨(distβ€˜ndx), (π‘₯ ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf(βˆͺ 𝑛 ∈ β„• ran (𝑔 ∈ {β„Ž ∈ ((𝑣 Γ— 𝑣) ↑m (1...𝑛)) ∣ ((π‘“β€˜(1st β€˜(β„Žβ€˜1))) = π‘₯ ∧ (π‘“β€˜(2nd β€˜(β„Žβ€˜π‘›))) = 𝑦 ∧ βˆ€π‘– ∈ (1...(𝑛 βˆ’ 1))(π‘“β€˜(2nd β€˜(β„Žβ€˜π‘–))) = (π‘“β€˜(1st β€˜(β„Žβ€˜(𝑖 + 1)))))} ↦ (ℝ*𝑠 Ξ£g ((distβ€˜π‘Ÿ) ∘ 𝑔))), ℝ*, < ))⟩})))
4 fvexd 6906 . . . 4 ((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) β†’ (Baseβ€˜π‘Ÿ) ∈ V)
5 simplrl 775 . . . . . . . . . 10 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ 𝑓 = 𝐹)
65rneqd 5937 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ran 𝑓 = ran 𝐹)
7 imasval.f . . . . . . . . . . 11 (πœ‘ β†’ 𝐹:𝑉–onto→𝐡)
8 forn 6808 . . . . . . . . . . 11 (𝐹:𝑉–onto→𝐡 β†’ ran 𝐹 = 𝐡)
97, 8syl 17 . . . . . . . . . 10 (πœ‘ β†’ ran 𝐹 = 𝐡)
109ad2antrr 724 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ran 𝐹 = 𝐡)
116, 10eqtrd 2772 . . . . . . . 8 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ran 𝑓 = 𝐡)
1211opeq2d 4880 . . . . . . 7 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ⟨(Baseβ€˜ndx), ran π‘“βŸ© = ⟨(Baseβ€˜ndx), 𝐡⟩)
13 simplrr 776 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ π‘Ÿ = 𝑅)
1413fveq2d 6895 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (Baseβ€˜π‘Ÿ) = (Baseβ€˜π‘…))
15 simpr 485 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ 𝑣 = (Baseβ€˜π‘Ÿ))
16 imasval.v . . . . . . . . . . . 12 (πœ‘ β†’ 𝑉 = (Baseβ€˜π‘…))
1716ad2antrr 724 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ 𝑉 = (Baseβ€˜π‘…))
1814, 15, 173eqtr4d 2782 . . . . . . . . . 10 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ 𝑣 = 𝑉)
195fveq1d 6893 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (π‘“β€˜π‘) = (πΉβ€˜π‘))
205fveq1d 6893 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (π‘“β€˜π‘ž) = (πΉβ€˜π‘ž))
2119, 20opeq12d 4881 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩ = ⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩)
2213fveq2d 6895 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (+gβ€˜π‘Ÿ) = (+gβ€˜π‘…))
23 imasval.p . . . . . . . . . . . . . . . 16 + = (+gβ€˜π‘…)
2422, 23eqtr4di 2790 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (+gβ€˜π‘Ÿ) = + )
2524oveqd 7425 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (𝑝(+gβ€˜π‘Ÿ)π‘ž) = (𝑝 + π‘ž))
265, 25fveq12d 6898 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (π‘“β€˜(𝑝(+gβ€˜π‘Ÿ)π‘ž)) = (πΉβ€˜(𝑝 + π‘ž)))
2721, 26opeq12d 4881 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(+gβ€˜π‘Ÿ)π‘ž))⟩ = ⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 + π‘ž))⟩)
2827sneqd 4640 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(+gβ€˜π‘Ÿ)π‘ž))⟩} = {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 + π‘ž))⟩})
2918, 28iuneq12d 5025 . . . . . . . . . 10 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(+gβ€˜π‘Ÿ)π‘ž))⟩} = βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 + π‘ž))⟩})
3018, 29iuneq12d 5025 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(+gβ€˜π‘Ÿ)π‘ž))⟩} = βˆͺ 𝑝 ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 + π‘ž))⟩})
31 imasval.a . . . . . . . . . 10 (πœ‘ β†’ ✚ = βˆͺ 𝑝 ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 + π‘ž))⟩})
3231ad2antrr 724 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ✚ = βˆͺ 𝑝 ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 + π‘ž))⟩})
3330, 32eqtr4d 2775 . . . . . . . 8 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(+gβ€˜π‘Ÿ)π‘ž))⟩} = ✚ )
3433opeq2d 4880 . . . . . . 7 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ⟨(+gβ€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(+gβ€˜π‘Ÿ)π‘ž))⟩}⟩ = ⟨(+gβ€˜ndx), ✚ ⟩)
3513fveq2d 6895 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (.rβ€˜π‘Ÿ) = (.rβ€˜π‘…))
36 imasval.m . . . . . . . . . . . . . . . 16 Γ— = (.rβ€˜π‘…)
3735, 36eqtr4di 2790 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (.rβ€˜π‘Ÿ) = Γ— )
3837oveqd 7425 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (𝑝(.rβ€˜π‘Ÿ)π‘ž) = (𝑝 Γ— π‘ž))
395, 38fveq12d 6898 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (π‘“β€˜(𝑝(.rβ€˜π‘Ÿ)π‘ž)) = (πΉβ€˜(𝑝 Γ— π‘ž)))
4021, 39opeq12d 4881 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(.rβ€˜π‘Ÿ)π‘ž))⟩ = ⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 Γ— π‘ž))⟩)
4140sneqd 4640 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(.rβ€˜π‘Ÿ)π‘ž))⟩} = {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 Γ— π‘ž))⟩})
4218, 41iuneq12d 5025 . . . . . . . . . 10 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(.rβ€˜π‘Ÿ)π‘ž))⟩} = βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 Γ— π‘ž))⟩})
4318, 42iuneq12d 5025 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(.rβ€˜π‘Ÿ)π‘ž))⟩} = βˆͺ 𝑝 ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 Γ— π‘ž))⟩})
44 imasval.t . . . . . . . . . 10 (πœ‘ β†’ βˆ™ = βˆͺ 𝑝 ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 Γ— π‘ž))⟩})
4544ad2antrr 724 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ βˆ™ = βˆͺ 𝑝 ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 Γ— π‘ž))⟩})
4643, 45eqtr4d 2775 . . . . . . . 8 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(.rβ€˜π‘Ÿ)π‘ž))⟩} = βˆ™ )
4746opeq2d 4880 . . . . . . 7 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ⟨(.rβ€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(.rβ€˜π‘Ÿ)π‘ž))⟩}⟩ = ⟨(.rβ€˜ndx), βˆ™ ⟩)
4812, 34, 47tpeq123d 4752 . . . . . 6 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ {⟨(Baseβ€˜ndx), ran π‘“βŸ©, ⟨(+gβ€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(+gβ€˜π‘Ÿ)π‘ž))⟩}⟩, ⟨(.rβ€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(.rβ€˜π‘Ÿ)π‘ž))⟩}⟩} = {⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(+gβ€˜ndx), ✚ ⟩, ⟨(.rβ€˜ndx), βˆ™ ⟩})
4913fveq2d 6895 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (Scalarβ€˜π‘Ÿ) = (Scalarβ€˜π‘…))
50 imasval.g . . . . . . . . 9 𝐺 = (Scalarβ€˜π‘…)
5149, 50eqtr4di 2790 . . . . . . . 8 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (Scalarβ€˜π‘Ÿ) = 𝐺)
5251opeq2d 4880 . . . . . . 7 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ⟨(Scalarβ€˜ndx), (Scalarβ€˜π‘Ÿ)⟩ = ⟨(Scalarβ€˜ndx), 𝐺⟩)
5351fveq2d 6895 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (Baseβ€˜(Scalarβ€˜π‘Ÿ)) = (Baseβ€˜πΊ))
54 imasval.k . . . . . . . . . . . 12 𝐾 = (Baseβ€˜πΊ)
5553, 54eqtr4di 2790 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (Baseβ€˜(Scalarβ€˜π‘Ÿ)) = 𝐾)
5620sneqd 4640 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ {(π‘“β€˜π‘ž)} = {(πΉβ€˜π‘ž)})
5713fveq2d 6895 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ( ·𝑠 β€˜π‘Ÿ) = ( ·𝑠 β€˜π‘…))
58 imasval.q . . . . . . . . . . . . . 14 Β· = ( ·𝑠 β€˜π‘…)
5957, 58eqtr4di 2790 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ( ·𝑠 β€˜π‘Ÿ) = Β· )
6059oveqd 7425 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (𝑝( ·𝑠 β€˜π‘Ÿ)π‘ž) = (𝑝 Β· π‘ž))
615, 60fveq12d 6898 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (π‘“β€˜(𝑝( ·𝑠 β€˜π‘Ÿ)π‘ž)) = (πΉβ€˜(𝑝 Β· π‘ž)))
6255, 56, 61mpoeq123dv 7483 . . . . . . . . . 10 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (𝑝 ∈ (Baseβ€˜(Scalarβ€˜π‘Ÿ)), π‘₯ ∈ {(π‘“β€˜π‘ž)} ↦ (π‘“β€˜(𝑝( ·𝑠 β€˜π‘Ÿ)π‘ž))) = (𝑝 ∈ 𝐾, π‘₯ ∈ {(πΉβ€˜π‘ž)} ↦ (πΉβ€˜(𝑝 Β· π‘ž))))
6362iuneq2d 5026 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ βˆͺ π‘ž ∈ 𝑉 (𝑝 ∈ (Baseβ€˜(Scalarβ€˜π‘Ÿ)), π‘₯ ∈ {(π‘“β€˜π‘ž)} ↦ (π‘“β€˜(𝑝( ·𝑠 β€˜π‘Ÿ)π‘ž))) = βˆͺ π‘ž ∈ 𝑉 (𝑝 ∈ 𝐾, π‘₯ ∈ {(πΉβ€˜π‘ž)} ↦ (πΉβ€˜(𝑝 Β· π‘ž))))
6418iuneq1d 5024 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ βˆͺ π‘ž ∈ 𝑣 (𝑝 ∈ (Baseβ€˜(Scalarβ€˜π‘Ÿ)), π‘₯ ∈ {(π‘“β€˜π‘ž)} ↦ (π‘“β€˜(𝑝( ·𝑠 β€˜π‘Ÿ)π‘ž))) = βˆͺ π‘ž ∈ 𝑉 (𝑝 ∈ (Baseβ€˜(Scalarβ€˜π‘Ÿ)), π‘₯ ∈ {(π‘“β€˜π‘ž)} ↦ (π‘“β€˜(𝑝( ·𝑠 β€˜π‘Ÿ)π‘ž))))
65 imasval.s . . . . . . . . . 10 (πœ‘ β†’ βŠ— = βˆͺ π‘ž ∈ 𝑉 (𝑝 ∈ 𝐾, π‘₯ ∈ {(πΉβ€˜π‘ž)} ↦ (πΉβ€˜(𝑝 Β· π‘ž))))
6665ad2antrr 724 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ βŠ— = βˆͺ π‘ž ∈ 𝑉 (𝑝 ∈ 𝐾, π‘₯ ∈ {(πΉβ€˜π‘ž)} ↦ (πΉβ€˜(𝑝 Β· π‘ž))))
6763, 64, 663eqtr4d 2782 . . . . . . . 8 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ βˆͺ π‘ž ∈ 𝑣 (𝑝 ∈ (Baseβ€˜(Scalarβ€˜π‘Ÿ)), π‘₯ ∈ {(π‘“β€˜π‘ž)} ↦ (π‘“β€˜(𝑝( ·𝑠 β€˜π‘Ÿ)π‘ž))) = βŠ— )
6867opeq2d 4880 . . . . . . 7 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ⟨( ·𝑠 β€˜ndx), βˆͺ π‘ž ∈ 𝑣 (𝑝 ∈ (Baseβ€˜(Scalarβ€˜π‘Ÿ)), π‘₯ ∈ {(π‘“β€˜π‘ž)} ↦ (π‘“β€˜(𝑝( ·𝑠 β€˜π‘Ÿ)π‘ž)))⟩ = ⟨( ·𝑠 β€˜ndx), βŠ— ⟩)
6913fveq2d 6895 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (Β·π‘–β€˜π‘Ÿ) = (Β·π‘–β€˜π‘…))
70 imasval.i . . . . . . . . . . . . . . 15 , = (Β·π‘–β€˜π‘…)
7169, 70eqtr4di 2790 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (Β·π‘–β€˜π‘Ÿ) = , )
7271oveqd 7425 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (𝑝(Β·π‘–β€˜π‘Ÿ)π‘ž) = (𝑝 , π‘ž))
7321, 72opeq12d 4881 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (𝑝(Β·π‘–β€˜π‘Ÿ)π‘ž)⟩ = ⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (𝑝 , π‘ž)⟩)
7473sneqd 4640 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (𝑝(Β·π‘–β€˜π‘Ÿ)π‘ž)⟩} = {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (𝑝 , π‘ž)⟩})
7518, 74iuneq12d 5025 . . . . . . . . . 10 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (𝑝(Β·π‘–β€˜π‘Ÿ)π‘ž)⟩} = βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (𝑝 , π‘ž)⟩})
7618, 75iuneq12d 5025 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (𝑝(Β·π‘–β€˜π‘Ÿ)π‘ž)⟩} = βˆͺ 𝑝 ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (𝑝 , π‘ž)⟩})
77 imasval.w . . . . . . . . . 10 (πœ‘ β†’ 𝐼 = βˆͺ 𝑝 ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (𝑝 , π‘ž)⟩})
7877ad2antrr 724 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ 𝐼 = βˆͺ 𝑝 ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (𝑝 , π‘ž)⟩})
7976, 78eqtr4d 2775 . . . . . . . 8 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (𝑝(Β·π‘–β€˜π‘Ÿ)π‘ž)⟩} = 𝐼)
8079opeq2d 4880 . . . . . . 7 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ⟨(Β·π‘–β€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (𝑝(Β·π‘–β€˜π‘Ÿ)π‘ž)⟩}⟩ = ⟨(Β·π‘–β€˜ndx), 𝐼⟩)
8152, 68, 80tpeq123d 4752 . . . . . 6 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ {⟨(Scalarβ€˜ndx), (Scalarβ€˜π‘Ÿ)⟩, ⟨( ·𝑠 β€˜ndx), βˆͺ π‘ž ∈ 𝑣 (𝑝 ∈ (Baseβ€˜(Scalarβ€˜π‘Ÿ)), π‘₯ ∈ {(π‘“β€˜π‘ž)} ↦ (π‘“β€˜(𝑝( ·𝑠 β€˜π‘Ÿ)π‘ž)))⟩, ⟨(Β·π‘–β€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (𝑝(Β·π‘–β€˜π‘Ÿ)π‘ž)⟩}⟩} = {⟨(Scalarβ€˜ndx), 𝐺⟩, ⟨( ·𝑠 β€˜ndx), βŠ— ⟩, ⟨(Β·π‘–β€˜ndx), 𝐼⟩})
8248, 81uneq12d 4164 . . . . 5 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ({⟨(Baseβ€˜ndx), ran π‘“βŸ©, ⟨(+gβ€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(+gβ€˜π‘Ÿ)π‘ž))⟩}⟩, ⟨(.rβ€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(.rβ€˜π‘Ÿ)π‘ž))⟩}⟩} βˆͺ {⟨(Scalarβ€˜ndx), (Scalarβ€˜π‘Ÿ)⟩, ⟨( ·𝑠 β€˜ndx), βˆͺ π‘ž ∈ 𝑣 (𝑝 ∈ (Baseβ€˜(Scalarβ€˜π‘Ÿ)), π‘₯ ∈ {(π‘“β€˜π‘ž)} ↦ (π‘“β€˜(𝑝( ·𝑠 β€˜π‘Ÿ)π‘ž)))⟩, ⟨(Β·π‘–β€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (𝑝(Β·π‘–β€˜π‘Ÿ)π‘ž)⟩}⟩}) = ({⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(+gβ€˜ndx), ✚ ⟩, ⟨(.rβ€˜ndx), βˆ™ ⟩} βˆͺ {⟨(Scalarβ€˜ndx), 𝐺⟩, ⟨( ·𝑠 β€˜ndx), βŠ— ⟩, ⟨(Β·π‘–β€˜ndx), 𝐼⟩}))
8313fveq2d 6895 . . . . . . . . . 10 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (TopOpenβ€˜π‘Ÿ) = (TopOpenβ€˜π‘…))
84 imasval.j . . . . . . . . . 10 𝐽 = (TopOpenβ€˜π‘…)
8583, 84eqtr4di 2790 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (TopOpenβ€˜π‘Ÿ) = 𝐽)
8685, 5oveq12d 7426 . . . . . . . 8 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ((TopOpenβ€˜π‘Ÿ) qTop 𝑓) = (𝐽 qTop 𝐹))
87 imasval.o . . . . . . . . 9 (πœ‘ β†’ 𝑂 = (𝐽 qTop 𝐹))
8887ad2antrr 724 . . . . . . . 8 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ 𝑂 = (𝐽 qTop 𝐹))
8986, 88eqtr4d 2775 . . . . . . 7 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ((TopOpenβ€˜π‘Ÿ) qTop 𝑓) = 𝑂)
9089opeq2d 4880 . . . . . 6 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ⟨(TopSetβ€˜ndx), ((TopOpenβ€˜π‘Ÿ) qTop 𝑓)⟩ = ⟨(TopSetβ€˜ndx), π‘‚βŸ©)
9113fveq2d 6895 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (leβ€˜π‘Ÿ) = (leβ€˜π‘…))
92 imasval.n . . . . . . . . . . 11 𝑁 = (leβ€˜π‘…)
9391, 92eqtr4di 2790 . . . . . . . . . 10 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (leβ€˜π‘Ÿ) = 𝑁)
945, 93coeq12d 5864 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (𝑓 ∘ (leβ€˜π‘Ÿ)) = (𝐹 ∘ 𝑁))
955cnveqd 5875 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ◑𝑓 = ◑𝐹)
9694, 95coeq12d 5864 . . . . . . . 8 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ((𝑓 ∘ (leβ€˜π‘Ÿ)) ∘ ◑𝑓) = ((𝐹 ∘ 𝑁) ∘ ◑𝐹))
97 imasval.l . . . . . . . . 9 (πœ‘ β†’ ≀ = ((𝐹 ∘ 𝑁) ∘ ◑𝐹))
9897ad2antrr 724 . . . . . . . 8 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ≀ = ((𝐹 ∘ 𝑁) ∘ ◑𝐹))
9996, 98eqtr4d 2775 . . . . . . 7 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ((𝑓 ∘ (leβ€˜π‘Ÿ)) ∘ ◑𝑓) = ≀ )
10099opeq2d 4880 . . . . . 6 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ⟨(leβ€˜ndx), ((𝑓 ∘ (leβ€˜π‘Ÿ)) ∘ ◑𝑓)⟩ = ⟨(leβ€˜ndx), ≀ ⟩)
10118sqxpeqd 5708 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (𝑣 Γ— 𝑣) = (𝑉 Γ— 𝑉))
102101oveq1d 7423 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ((𝑣 Γ— 𝑣) ↑m (1...𝑛)) = ((𝑉 Γ— 𝑉) ↑m (1...𝑛)))
1035fveq1d 6893 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (π‘“β€˜(1st β€˜(β„Žβ€˜1))) = (πΉβ€˜(1st β€˜(β„Žβ€˜1))))
104103eqeq1d 2734 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ((π‘“β€˜(1st β€˜(β„Žβ€˜1))) = π‘₯ ↔ (πΉβ€˜(1st β€˜(β„Žβ€˜1))) = π‘₯))
1055fveq1d 6893 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (π‘“β€˜(2nd β€˜(β„Žβ€˜π‘›))) = (πΉβ€˜(2nd β€˜(β„Žβ€˜π‘›))))
106105eqeq1d 2734 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ((π‘“β€˜(2nd β€˜(β„Žβ€˜π‘›))) = 𝑦 ↔ (πΉβ€˜(2nd β€˜(β„Žβ€˜π‘›))) = 𝑦))
1075fveq1d 6893 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (π‘“β€˜(2nd β€˜(β„Žβ€˜π‘–))) = (πΉβ€˜(2nd β€˜(β„Žβ€˜π‘–))))
1085fveq1d 6893 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (π‘“β€˜(1st β€˜(β„Žβ€˜(𝑖 + 1)))) = (πΉβ€˜(1st β€˜(β„Žβ€˜(𝑖 + 1)))))
109107, 108eqeq12d 2748 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ((π‘“β€˜(2nd β€˜(β„Žβ€˜π‘–))) = (π‘“β€˜(1st β€˜(β„Žβ€˜(𝑖 + 1)))) ↔ (πΉβ€˜(2nd β€˜(β„Žβ€˜π‘–))) = (πΉβ€˜(1st β€˜(β„Žβ€˜(𝑖 + 1))))))
110109ralbidv 3177 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (βˆ€π‘– ∈ (1...(𝑛 βˆ’ 1))(π‘“β€˜(2nd β€˜(β„Žβ€˜π‘–))) = (π‘“β€˜(1st β€˜(β„Žβ€˜(𝑖 + 1)))) ↔ βˆ€π‘– ∈ (1...(𝑛 βˆ’ 1))(πΉβ€˜(2nd β€˜(β„Žβ€˜π‘–))) = (πΉβ€˜(1st β€˜(β„Žβ€˜(𝑖 + 1))))))
111104, 106, 1103anbi123d 1436 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (((π‘“β€˜(1st β€˜(β„Žβ€˜1))) = π‘₯ ∧ (π‘“β€˜(2nd β€˜(β„Žβ€˜π‘›))) = 𝑦 ∧ βˆ€π‘– ∈ (1...(𝑛 βˆ’ 1))(π‘“β€˜(2nd β€˜(β„Žβ€˜π‘–))) = (π‘“β€˜(1st β€˜(β„Žβ€˜(𝑖 + 1))))) ↔ ((πΉβ€˜(1st β€˜(β„Žβ€˜1))) = π‘₯ ∧ (πΉβ€˜(2nd β€˜(β„Žβ€˜π‘›))) = 𝑦 ∧ βˆ€π‘– ∈ (1...(𝑛 βˆ’ 1))(πΉβ€˜(2nd β€˜(β„Žβ€˜π‘–))) = (πΉβ€˜(1st β€˜(β„Žβ€˜(𝑖 + 1)))))))
112102, 111rabeqbidv 3449 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ {β„Ž ∈ ((𝑣 Γ— 𝑣) ↑m (1...𝑛)) ∣ ((π‘“β€˜(1st β€˜(β„Žβ€˜1))) = π‘₯ ∧ (π‘“β€˜(2nd β€˜(β„Žβ€˜π‘›))) = 𝑦 ∧ βˆ€π‘– ∈ (1...(𝑛 βˆ’ 1))(π‘“β€˜(2nd β€˜(β„Žβ€˜π‘–))) = (π‘“β€˜(1st β€˜(β„Žβ€˜(𝑖 + 1)))))} = {β„Ž ∈ ((𝑉 Γ— 𝑉) ↑m (1...𝑛)) ∣ ((πΉβ€˜(1st β€˜(β„Žβ€˜1))) = π‘₯ ∧ (πΉβ€˜(2nd β€˜(β„Žβ€˜π‘›))) = 𝑦 ∧ βˆ€π‘– ∈ (1...(𝑛 βˆ’ 1))(πΉβ€˜(2nd β€˜(β„Žβ€˜π‘–))) = (πΉβ€˜(1st β€˜(β„Žβ€˜(𝑖 + 1)))))})
11313fveq2d 6895 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (distβ€˜π‘Ÿ) = (distβ€˜π‘…))
114 imasval.e . . . . . . . . . . . . . . . 16 𝐸 = (distβ€˜π‘…)
115113, 114eqtr4di 2790 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (distβ€˜π‘Ÿ) = 𝐸)
116115coeq1d 5861 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ((distβ€˜π‘Ÿ) ∘ 𝑔) = (𝐸 ∘ 𝑔))
117116oveq2d 7424 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (ℝ*𝑠 Ξ£g ((distβ€˜π‘Ÿ) ∘ 𝑔)) = (ℝ*𝑠 Ξ£g (𝐸 ∘ 𝑔)))
118112, 117mpteq12dv 5239 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (𝑔 ∈ {β„Ž ∈ ((𝑣 Γ— 𝑣) ↑m (1...𝑛)) ∣ ((π‘“β€˜(1st β€˜(β„Žβ€˜1))) = π‘₯ ∧ (π‘“β€˜(2nd β€˜(β„Žβ€˜π‘›))) = 𝑦 ∧ βˆ€π‘– ∈ (1...(𝑛 βˆ’ 1))(π‘“β€˜(2nd β€˜(β„Žβ€˜π‘–))) = (π‘“β€˜(1st β€˜(β„Žβ€˜(𝑖 + 1)))))} ↦ (ℝ*𝑠 Ξ£g ((distβ€˜π‘Ÿ) ∘ 𝑔))) = (𝑔 ∈ {β„Ž ∈ ((𝑉 Γ— 𝑉) ↑m (1...𝑛)) ∣ ((πΉβ€˜(1st β€˜(β„Žβ€˜1))) = π‘₯ ∧ (πΉβ€˜(2nd β€˜(β„Žβ€˜π‘›))) = 𝑦 ∧ βˆ€π‘– ∈ (1...(𝑛 βˆ’ 1))(πΉβ€˜(2nd β€˜(β„Žβ€˜π‘–))) = (πΉβ€˜(1st β€˜(β„Žβ€˜(𝑖 + 1)))))} ↦ (ℝ*𝑠 Ξ£g (𝐸 ∘ 𝑔))))
119118rneqd 5937 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ran (𝑔 ∈ {β„Ž ∈ ((𝑣 Γ— 𝑣) ↑m (1...𝑛)) ∣ ((π‘“β€˜(1st β€˜(β„Žβ€˜1))) = π‘₯ ∧ (π‘“β€˜(2nd β€˜(β„Žβ€˜π‘›))) = 𝑦 ∧ βˆ€π‘– ∈ (1...(𝑛 βˆ’ 1))(π‘“β€˜(2nd β€˜(β„Žβ€˜π‘–))) = (π‘“β€˜(1st β€˜(β„Žβ€˜(𝑖 + 1)))))} ↦ (ℝ*𝑠 Ξ£g ((distβ€˜π‘Ÿ) ∘ 𝑔))) = ran (𝑔 ∈ {β„Ž ∈ ((𝑉 Γ— 𝑉) ↑m (1...𝑛)) ∣ ((πΉβ€˜(1st β€˜(β„Žβ€˜1))) = π‘₯ ∧ (πΉβ€˜(2nd β€˜(β„Žβ€˜π‘›))) = 𝑦 ∧ βˆ€π‘– ∈ (1...(𝑛 βˆ’ 1))(πΉβ€˜(2nd β€˜(β„Žβ€˜π‘–))) = (πΉβ€˜(1st β€˜(β„Žβ€˜(𝑖 + 1)))))} ↦ (ℝ*𝑠 Ξ£g (𝐸 ∘ 𝑔))))
120119iuneq2d 5026 . . . . . . . . . 10 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ βˆͺ 𝑛 ∈ β„• ran (𝑔 ∈ {β„Ž ∈ ((𝑣 Γ— 𝑣) ↑m (1...𝑛)) ∣ ((π‘“β€˜(1st β€˜(β„Žβ€˜1))) = π‘₯ ∧ (π‘“β€˜(2nd β€˜(β„Žβ€˜π‘›))) = 𝑦 ∧ βˆ€π‘– ∈ (1...(𝑛 βˆ’ 1))(π‘“β€˜(2nd β€˜(β„Žβ€˜π‘–))) = (π‘“β€˜(1st β€˜(β„Žβ€˜(𝑖 + 1)))))} ↦ (ℝ*𝑠 Ξ£g ((distβ€˜π‘Ÿ) ∘ 𝑔))) = βˆͺ 𝑛 ∈ β„• ran (𝑔 ∈ {β„Ž ∈ ((𝑉 Γ— 𝑉) ↑m (1...𝑛)) ∣ ((πΉβ€˜(1st β€˜(β„Žβ€˜1))) = π‘₯ ∧ (πΉβ€˜(2nd β€˜(β„Žβ€˜π‘›))) = 𝑦 ∧ βˆ€π‘– ∈ (1...(𝑛 βˆ’ 1))(πΉβ€˜(2nd β€˜(β„Žβ€˜π‘–))) = (πΉβ€˜(1st β€˜(β„Žβ€˜(𝑖 + 1)))))} ↦ (ℝ*𝑠 Ξ£g (𝐸 ∘ 𝑔))))
121120infeq1d 9471 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ inf(βˆͺ 𝑛 ∈ β„• ran (𝑔 ∈ {β„Ž ∈ ((𝑣 Γ— 𝑣) ↑m (1...𝑛)) ∣ ((π‘“β€˜(1st β€˜(β„Žβ€˜1))) = π‘₯ ∧ (π‘“β€˜(2nd β€˜(β„Žβ€˜π‘›))) = 𝑦 ∧ βˆ€π‘– ∈ (1...(𝑛 βˆ’ 1))(π‘“β€˜(2nd β€˜(β„Žβ€˜π‘–))) = (π‘“β€˜(1st β€˜(β„Žβ€˜(𝑖 + 1)))))} ↦ (ℝ*𝑠 Ξ£g ((distβ€˜π‘Ÿ) ∘ 𝑔))), ℝ*, < ) = inf(βˆͺ 𝑛 ∈ β„• ran (𝑔 ∈ {β„Ž ∈ ((𝑉 Γ— 𝑉) ↑m (1...𝑛)) ∣ ((πΉβ€˜(1st β€˜(β„Žβ€˜1))) = π‘₯ ∧ (πΉβ€˜(2nd β€˜(β„Žβ€˜π‘›))) = 𝑦 ∧ βˆ€π‘– ∈ (1...(𝑛 βˆ’ 1))(πΉβ€˜(2nd β€˜(β„Žβ€˜π‘–))) = (πΉβ€˜(1st β€˜(β„Žβ€˜(𝑖 + 1)))))} ↦ (ℝ*𝑠 Ξ£g (𝐸 ∘ 𝑔))), ℝ*, < ))
12211, 11, 121mpoeq123dv 7483 . . . . . . . 8 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (π‘₯ ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf(βˆͺ 𝑛 ∈ β„• ran (𝑔 ∈ {β„Ž ∈ ((𝑣 Γ— 𝑣) ↑m (1...𝑛)) ∣ ((π‘“β€˜(1st β€˜(β„Žβ€˜1))) = π‘₯ ∧ (π‘“β€˜(2nd β€˜(β„Žβ€˜π‘›))) = 𝑦 ∧ βˆ€π‘– ∈ (1...(𝑛 βˆ’ 1))(π‘“β€˜(2nd β€˜(β„Žβ€˜π‘–))) = (π‘“β€˜(1st β€˜(β„Žβ€˜(𝑖 + 1)))))} ↦ (ℝ*𝑠 Ξ£g ((distβ€˜π‘Ÿ) ∘ 𝑔))), ℝ*, < )) = (π‘₯ ∈ 𝐡, 𝑦 ∈ 𝐡 ↦ inf(βˆͺ 𝑛 ∈ β„• ran (𝑔 ∈ {β„Ž ∈ ((𝑉 Γ— 𝑉) ↑m (1...𝑛)) ∣ ((πΉβ€˜(1st β€˜(β„Žβ€˜1))) = π‘₯ ∧ (πΉβ€˜(2nd β€˜(β„Žβ€˜π‘›))) = 𝑦 ∧ βˆ€π‘– ∈ (1...(𝑛 βˆ’ 1))(πΉβ€˜(2nd β€˜(β„Žβ€˜π‘–))) = (πΉβ€˜(1st β€˜(β„Žβ€˜(𝑖 + 1)))))} ↦ (ℝ*𝑠 Ξ£g (𝐸 ∘ 𝑔))), ℝ*, < )))
123 imasval.d . . . . . . . . 9 (πœ‘ β†’ 𝐷 = (π‘₯ ∈ 𝐡, 𝑦 ∈ 𝐡 ↦ inf(βˆͺ 𝑛 ∈ β„• ran (𝑔 ∈ {β„Ž ∈ ((𝑉 Γ— 𝑉) ↑m (1...𝑛)) ∣ ((πΉβ€˜(1st β€˜(β„Žβ€˜1))) = π‘₯ ∧ (πΉβ€˜(2nd β€˜(β„Žβ€˜π‘›))) = 𝑦 ∧ βˆ€π‘– ∈ (1...(𝑛 βˆ’ 1))(πΉβ€˜(2nd β€˜(β„Žβ€˜π‘–))) = (πΉβ€˜(1st β€˜(β„Žβ€˜(𝑖 + 1)))))} ↦ (ℝ*𝑠 Ξ£g (𝐸 ∘ 𝑔))), ℝ*, < )))
124123ad2antrr 724 . . . . . . . 8 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ 𝐷 = (π‘₯ ∈ 𝐡, 𝑦 ∈ 𝐡 ↦ inf(βˆͺ 𝑛 ∈ β„• ran (𝑔 ∈ {β„Ž ∈ ((𝑉 Γ— 𝑉) ↑m (1...𝑛)) ∣ ((πΉβ€˜(1st β€˜(β„Žβ€˜1))) = π‘₯ ∧ (πΉβ€˜(2nd β€˜(β„Žβ€˜π‘›))) = 𝑦 ∧ βˆ€π‘– ∈ (1...(𝑛 βˆ’ 1))(πΉβ€˜(2nd β€˜(β„Žβ€˜π‘–))) = (πΉβ€˜(1st β€˜(β„Žβ€˜(𝑖 + 1)))))} ↦ (ℝ*𝑠 Ξ£g (𝐸 ∘ 𝑔))), ℝ*, < )))
125122, 124eqtr4d 2775 . . . . . . 7 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (π‘₯ ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf(βˆͺ 𝑛 ∈ β„• ran (𝑔 ∈ {β„Ž ∈ ((𝑣 Γ— 𝑣) ↑m (1...𝑛)) ∣ ((π‘“β€˜(1st β€˜(β„Žβ€˜1))) = π‘₯ ∧ (π‘“β€˜(2nd β€˜(β„Žβ€˜π‘›))) = 𝑦 ∧ βˆ€π‘– ∈ (1...(𝑛 βˆ’ 1))(π‘“β€˜(2nd β€˜(β„Žβ€˜π‘–))) = (π‘“β€˜(1st β€˜(β„Žβ€˜(𝑖 + 1)))))} ↦ (ℝ*𝑠 Ξ£g ((distβ€˜π‘Ÿ) ∘ 𝑔))), ℝ*, < )) = 𝐷)
126125opeq2d 4880 . . . . . 6 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ⟨(distβ€˜ndx), (π‘₯ ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf(βˆͺ 𝑛 ∈ β„• ran (𝑔 ∈ {β„Ž ∈ ((𝑣 Γ— 𝑣) ↑m (1...𝑛)) ∣ ((π‘“β€˜(1st β€˜(β„Žβ€˜1))) = π‘₯ ∧ (π‘“β€˜(2nd β€˜(β„Žβ€˜π‘›))) = 𝑦 ∧ βˆ€π‘– ∈ (1...(𝑛 βˆ’ 1))(π‘“β€˜(2nd β€˜(β„Žβ€˜π‘–))) = (π‘“β€˜(1st β€˜(β„Žβ€˜(𝑖 + 1)))))} ↦ (ℝ*𝑠 Ξ£g ((distβ€˜π‘Ÿ) ∘ 𝑔))), ℝ*, < ))⟩ = ⟨(distβ€˜ndx), 𝐷⟩)
12790, 100, 126tpeq123d 4752 . . . . 5 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ {⟨(TopSetβ€˜ndx), ((TopOpenβ€˜π‘Ÿ) qTop 𝑓)⟩, ⟨(leβ€˜ndx), ((𝑓 ∘ (leβ€˜π‘Ÿ)) ∘ ◑𝑓)⟩, ⟨(distβ€˜ndx), (π‘₯ ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf(βˆͺ 𝑛 ∈ β„• ran (𝑔 ∈ {β„Ž ∈ ((𝑣 Γ— 𝑣) ↑m (1...𝑛)) ∣ ((π‘“β€˜(1st β€˜(β„Žβ€˜1))) = π‘₯ ∧ (π‘“β€˜(2nd β€˜(β„Žβ€˜π‘›))) = 𝑦 ∧ βˆ€π‘– ∈ (1...(𝑛 βˆ’ 1))(π‘“β€˜(2nd β€˜(β„Žβ€˜π‘–))) = (π‘“β€˜(1st β€˜(β„Žβ€˜(𝑖 + 1)))))} ↦ (ℝ*𝑠 Ξ£g ((distβ€˜π‘Ÿ) ∘ 𝑔))), ℝ*, < ))⟩} = {⟨(TopSetβ€˜ndx), π‘‚βŸ©, ⟨(leβ€˜ndx), ≀ ⟩, ⟨(distβ€˜ndx), 𝐷⟩})
12882, 127uneq12d 4164 . . . 4 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (({⟨(Baseβ€˜ndx), ran π‘“βŸ©, ⟨(+gβ€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(+gβ€˜π‘Ÿ)π‘ž))⟩}⟩, ⟨(.rβ€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(.rβ€˜π‘Ÿ)π‘ž))⟩}⟩} βˆͺ {⟨(Scalarβ€˜ndx), (Scalarβ€˜π‘Ÿ)⟩, ⟨( ·𝑠 β€˜ndx), βˆͺ π‘ž ∈ 𝑣 (𝑝 ∈ (Baseβ€˜(Scalarβ€˜π‘Ÿ)), π‘₯ ∈ {(π‘“β€˜π‘ž)} ↦ (π‘“β€˜(𝑝( ·𝑠 β€˜π‘Ÿ)π‘ž)))⟩, ⟨(Β·π‘–β€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (𝑝(Β·π‘–β€˜π‘Ÿ)π‘ž)⟩}⟩}) βˆͺ {⟨(TopSetβ€˜ndx), ((TopOpenβ€˜π‘Ÿ) qTop 𝑓)⟩, ⟨(leβ€˜ndx), ((𝑓 ∘ (leβ€˜π‘Ÿ)) ∘ ◑𝑓)⟩, ⟨(distβ€˜ndx), (π‘₯ ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf(βˆͺ 𝑛 ∈ β„• ran (𝑔 ∈ {β„Ž ∈ ((𝑣 Γ— 𝑣) ↑m (1...𝑛)) ∣ ((π‘“β€˜(1st β€˜(β„Žβ€˜1))) = π‘₯ ∧ (π‘“β€˜(2nd β€˜(β„Žβ€˜π‘›))) = 𝑦 ∧ βˆ€π‘– ∈ (1...(𝑛 βˆ’ 1))(π‘“β€˜(2nd β€˜(β„Žβ€˜π‘–))) = (π‘“β€˜(1st β€˜(β„Žβ€˜(𝑖 + 1)))))} ↦ (ℝ*𝑠 Ξ£g ((distβ€˜π‘Ÿ) ∘ 𝑔))), ℝ*, < ))⟩}) = (({⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(+gβ€˜ndx), ✚ ⟩, ⟨(.rβ€˜ndx), βˆ™ ⟩} βˆͺ {⟨(Scalarβ€˜ndx), 𝐺⟩, ⟨( ·𝑠 β€˜ndx), βŠ— ⟩, ⟨(Β·π‘–β€˜ndx), 𝐼⟩}) βˆͺ {⟨(TopSetβ€˜ndx), π‘‚βŸ©, ⟨(leβ€˜ndx), ≀ ⟩, ⟨(distβ€˜ndx), 𝐷⟩}))
1294, 128csbied 3931 . . 3 ((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) β†’ ⦋(Baseβ€˜π‘Ÿ) / π‘£β¦Œ(({⟨(Baseβ€˜ndx), ran π‘“βŸ©, ⟨(+gβ€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(+gβ€˜π‘Ÿ)π‘ž))⟩}⟩, ⟨(.rβ€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(.rβ€˜π‘Ÿ)π‘ž))⟩}⟩} βˆͺ {⟨(Scalarβ€˜ndx), (Scalarβ€˜π‘Ÿ)⟩, ⟨( ·𝑠 β€˜ndx), βˆͺ π‘ž ∈ 𝑣 (𝑝 ∈ (Baseβ€˜(Scalarβ€˜π‘Ÿ)), π‘₯ ∈ {(π‘“β€˜π‘ž)} ↦ (π‘“β€˜(𝑝( ·𝑠 β€˜π‘Ÿ)π‘ž)))⟩, ⟨(Β·π‘–β€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (𝑝(Β·π‘–β€˜π‘Ÿ)π‘ž)⟩}⟩}) βˆͺ {⟨(TopSetβ€˜ndx), ((TopOpenβ€˜π‘Ÿ) qTop 𝑓)⟩, ⟨(leβ€˜ndx), ((𝑓 ∘ (leβ€˜π‘Ÿ)) ∘ ◑𝑓)⟩, ⟨(distβ€˜ndx), (π‘₯ ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf(βˆͺ 𝑛 ∈ β„• ran (𝑔 ∈ {β„Ž ∈ ((𝑣 Γ— 𝑣) ↑m (1...𝑛)) ∣ ((π‘“β€˜(1st β€˜(β„Žβ€˜1))) = π‘₯ ∧ (π‘“β€˜(2nd β€˜(β„Žβ€˜π‘›))) = 𝑦 ∧ βˆ€π‘– ∈ (1...(𝑛 βˆ’ 1))(π‘“β€˜(2nd β€˜(β„Žβ€˜π‘–))) = (π‘“β€˜(1st β€˜(β„Žβ€˜(𝑖 + 1)))))} ↦ (ℝ*𝑠 Ξ£g ((distβ€˜π‘Ÿ) ∘ 𝑔))), ℝ*, < ))⟩}) = (({⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(+gβ€˜ndx), ✚ ⟩, ⟨(.rβ€˜ndx), βˆ™ ⟩} βˆͺ {⟨(Scalarβ€˜ndx), 𝐺⟩, ⟨( ·𝑠 β€˜ndx), βŠ— ⟩, ⟨(Β·π‘–β€˜ndx), 𝐼⟩}) βˆͺ {⟨(TopSetβ€˜ndx), π‘‚βŸ©, ⟨(leβ€˜ndx), ≀ ⟩, ⟨(distβ€˜ndx), 𝐷⟩}))
130 fof 6805 . . . . 5 (𝐹:𝑉–onto→𝐡 β†’ 𝐹:π‘‰βŸΆπ΅)
1317, 130syl 17 . . . 4 (πœ‘ β†’ 𝐹:π‘‰βŸΆπ΅)
132 fvex 6904 . . . . 5 (Baseβ€˜π‘…) ∈ V
13316, 132eqeltrdi 2841 . . . 4 (πœ‘ β†’ 𝑉 ∈ V)
134131, 133fexd 7228 . . 3 (πœ‘ β†’ 𝐹 ∈ V)
135 imasval.r . . . 4 (πœ‘ β†’ 𝑅 ∈ 𝑍)
136135elexd 3494 . . 3 (πœ‘ β†’ 𝑅 ∈ V)
137 tpex 7733 . . . . . 6 {⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(+gβ€˜ndx), ✚ ⟩, ⟨(.rβ€˜ndx), βˆ™ ⟩} ∈ V
138 tpex 7733 . . . . . 6 {⟨(Scalarβ€˜ndx), 𝐺⟩, ⟨( ·𝑠 β€˜ndx), βŠ— ⟩, ⟨(Β·π‘–β€˜ndx), 𝐼⟩} ∈ V
139137, 138unex 7732 . . . . 5 ({⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(+gβ€˜ndx), ✚ ⟩, ⟨(.rβ€˜ndx), βˆ™ ⟩} βˆͺ {⟨(Scalarβ€˜ndx), 𝐺⟩, ⟨( ·𝑠 β€˜ndx), βŠ— ⟩, ⟨(Β·π‘–β€˜ndx), 𝐼⟩}) ∈ V
140 tpex 7733 . . . . 5 {⟨(TopSetβ€˜ndx), π‘‚βŸ©, ⟨(leβ€˜ndx), ≀ ⟩, ⟨(distβ€˜ndx), 𝐷⟩} ∈ V
141139, 140unex 7732 . . . 4 (({⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(+gβ€˜ndx), ✚ ⟩, ⟨(.rβ€˜ndx), βˆ™ ⟩} βˆͺ {⟨(Scalarβ€˜ndx), 𝐺⟩, ⟨( ·𝑠 β€˜ndx), βŠ— ⟩, ⟨(Β·π‘–β€˜ndx), 𝐼⟩}) βˆͺ {⟨(TopSetβ€˜ndx), π‘‚βŸ©, ⟨(leβ€˜ndx), ≀ ⟩, ⟨(distβ€˜ndx), 𝐷⟩}) ∈ V
142141a1i 11 . . 3 (πœ‘ β†’ (({⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(+gβ€˜ndx), ✚ ⟩, ⟨(.rβ€˜ndx), βˆ™ ⟩} βˆͺ {⟨(Scalarβ€˜ndx), 𝐺⟩, ⟨( ·𝑠 β€˜ndx), βŠ— ⟩, ⟨(Β·π‘–β€˜ndx), 𝐼⟩}) βˆͺ {⟨(TopSetβ€˜ndx), π‘‚βŸ©, ⟨(leβ€˜ndx), ≀ ⟩, ⟨(distβ€˜ndx), 𝐷⟩}) ∈ V)
1433, 129, 134, 136, 142ovmpod 7559 . 2 (πœ‘ β†’ (𝐹 β€œs 𝑅) = (({⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(+gβ€˜ndx), ✚ ⟩, ⟨(.rβ€˜ndx), βˆ™ ⟩} βˆͺ {⟨(Scalarβ€˜ndx), 𝐺⟩, ⟨( ·𝑠 β€˜ndx), βŠ— ⟩, ⟨(Β·π‘–β€˜ndx), 𝐼⟩}) βˆͺ {⟨(TopSetβ€˜ndx), π‘‚βŸ©, ⟨(leβ€˜ndx), ≀ ⟩, ⟨(distβ€˜ndx), 𝐷⟩}))
1441, 143eqtrd 2772 1 (πœ‘ β†’ π‘ˆ = (({⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(+gβ€˜ndx), ✚ ⟩, ⟨(.rβ€˜ndx), βˆ™ ⟩} βˆͺ {⟨(Scalarβ€˜ndx), 𝐺⟩, ⟨( ·𝑠 β€˜ndx), βŠ— ⟩, ⟨(Β·π‘–β€˜ndx), 𝐼⟩}) βˆͺ {⟨(TopSetβ€˜ndx), π‘‚βŸ©, ⟨(leβ€˜ndx), ≀ ⟩, ⟨(distβ€˜ndx), 𝐷⟩}))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  βˆ€wral 3061  {crab 3432  Vcvv 3474  β¦‹csb 3893   βˆͺ cun 3946  {csn 4628  {ctp 4632  βŸ¨cop 4634  βˆͺ ciun 4997   ↦ cmpt 5231   Γ— cxp 5674  β—‘ccnv 5675  ran crn 5677   ∘ ccom 5680  βŸΆwf 6539  β€“ontoβ†’wfo 6541  β€˜cfv 6543  (class class class)co 7408   ∈ cmpo 7410  1st c1st 7972  2nd c2nd 7973   ↑m cmap 8819  infcinf 9435  1c1 11110   + caddc 11112  β„*cxr 11246   < clt 11247   βˆ’ cmin 11443  β„•cn 12211  ...cfz 13483  ndxcnx 17125  Basecbs 17143  +gcplusg 17196  .rcmulr 17197  Scalarcsca 17199   ·𝑠 cvsca 17200  Β·π‘–cip 17201  TopSetcts 17202  lecple 17203  distcds 17205  TopOpenctopn 17366   Ξ£g cgsu 17385  β„*𝑠cxrs 17445   qTop cqtop 17448   β€œs cimas 17449
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7724
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7411  df-oprab 7412  df-mpo 7413  df-sup 9436  df-inf 9437  df-imas 17453
This theorem is referenced by:  imasbas  17457  imasds  17458  imasplusg  17462  imasmulr  17463  imassca  17464  imasvsca  17465  imasip  17466  imastset  17467  imasle  17468
  Copyright terms: Public domain W3C validator