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

Theorem imasval 17466
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 17463 . . . 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 6900 . . . 4 ((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) β†’ (Baseβ€˜π‘Ÿ) ∈ V)
5 simplrl 774 . . . . . . . . . 10 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ 𝑓 = 𝐹)
65rneqd 5931 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ran 𝑓 = ran 𝐹)
7 imasval.f . . . . . . . . . . 11 (πœ‘ β†’ 𝐹:𝑉–onto→𝐡)
8 forn 6802 . . . . . . . . . . 11 (𝐹:𝑉–onto→𝐡 β†’ ran 𝐹 = 𝐡)
97, 8syl 17 . . . . . . . . . 10 (πœ‘ β†’ ran 𝐹 = 𝐡)
109ad2antrr 723 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ran 𝐹 = 𝐡)
116, 10eqtrd 2766 . . . . . . . 8 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ran 𝑓 = 𝐡)
1211opeq2d 4875 . . . . . . 7 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ⟨(Baseβ€˜ndx), ran π‘“βŸ© = ⟨(Baseβ€˜ndx), 𝐡⟩)
13 simplrr 775 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ π‘Ÿ = 𝑅)
1413fveq2d 6889 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (Baseβ€˜π‘Ÿ) = (Baseβ€˜π‘…))
15 simpr 484 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ 𝑣 = (Baseβ€˜π‘Ÿ))
16 imasval.v . . . . . . . . . . . 12 (πœ‘ β†’ 𝑉 = (Baseβ€˜π‘…))
1716ad2antrr 723 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ 𝑉 = (Baseβ€˜π‘…))
1814, 15, 173eqtr4d 2776 . . . . . . . . . 10 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ 𝑣 = 𝑉)
195fveq1d 6887 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (π‘“β€˜π‘) = (πΉβ€˜π‘))
205fveq1d 6887 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (π‘“β€˜π‘ž) = (πΉβ€˜π‘ž))
2119, 20opeq12d 4876 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩ = ⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩)
2213fveq2d 6889 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (+gβ€˜π‘Ÿ) = (+gβ€˜π‘…))
23 imasval.p . . . . . . . . . . . . . . . 16 + = (+gβ€˜π‘…)
2422, 23eqtr4di 2784 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (+gβ€˜π‘Ÿ) = + )
2524oveqd 7422 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (𝑝(+gβ€˜π‘Ÿ)π‘ž) = (𝑝 + π‘ž))
265, 25fveq12d 6892 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (π‘“β€˜(𝑝(+gβ€˜π‘Ÿ)π‘ž)) = (πΉβ€˜(𝑝 + π‘ž)))
2721, 26opeq12d 4876 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(+gβ€˜π‘Ÿ)π‘ž))⟩ = ⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 + π‘ž))⟩)
2827sneqd 4635 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(+gβ€˜π‘Ÿ)π‘ž))⟩} = {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 + π‘ž))⟩})
2918, 28iuneq12d 5018 . . . . . . . . . 10 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(+gβ€˜π‘Ÿ)π‘ž))⟩} = βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 + π‘ž))⟩})
3018, 29iuneq12d 5018 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(+gβ€˜π‘Ÿ)π‘ž))⟩} = βˆͺ 𝑝 ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 + π‘ž))⟩})
31 imasval.a . . . . . . . . . 10 (πœ‘ β†’ ✚ = βˆͺ 𝑝 ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 + π‘ž))⟩})
3231ad2antrr 723 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ✚ = βˆͺ 𝑝 ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 + π‘ž))⟩})
3330, 32eqtr4d 2769 . . . . . . . 8 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(+gβ€˜π‘Ÿ)π‘ž))⟩} = ✚ )
3433opeq2d 4875 . . . . . . 7 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ⟨(+gβ€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(+gβ€˜π‘Ÿ)π‘ž))⟩}⟩ = ⟨(+gβ€˜ndx), ✚ ⟩)
3513fveq2d 6889 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (.rβ€˜π‘Ÿ) = (.rβ€˜π‘…))
36 imasval.m . . . . . . . . . . . . . . . 16 Γ— = (.rβ€˜π‘…)
3735, 36eqtr4di 2784 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (.rβ€˜π‘Ÿ) = Γ— )
3837oveqd 7422 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (𝑝(.rβ€˜π‘Ÿ)π‘ž) = (𝑝 Γ— π‘ž))
395, 38fveq12d 6892 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (π‘“β€˜(𝑝(.rβ€˜π‘Ÿ)π‘ž)) = (πΉβ€˜(𝑝 Γ— π‘ž)))
4021, 39opeq12d 4876 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(.rβ€˜π‘Ÿ)π‘ž))⟩ = ⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 Γ— π‘ž))⟩)
4140sneqd 4635 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(.rβ€˜π‘Ÿ)π‘ž))⟩} = {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 Γ— π‘ž))⟩})
4218, 41iuneq12d 5018 . . . . . . . . . 10 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(.rβ€˜π‘Ÿ)π‘ž))⟩} = βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 Γ— π‘ž))⟩})
4318, 42iuneq12d 5018 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(.rβ€˜π‘Ÿ)π‘ž))⟩} = βˆͺ 𝑝 ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 Γ— π‘ž))⟩})
44 imasval.t . . . . . . . . . 10 (πœ‘ β†’ βˆ™ = βˆͺ 𝑝 ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 Γ— π‘ž))⟩})
4544ad2antrr 723 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ βˆ™ = βˆͺ 𝑝 ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 Γ— π‘ž))⟩})
4643, 45eqtr4d 2769 . . . . . . . 8 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(.rβ€˜π‘Ÿ)π‘ž))⟩} = βˆ™ )
4746opeq2d 4875 . . . . . . 7 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ⟨(.rβ€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(.rβ€˜π‘Ÿ)π‘ž))⟩}⟩ = ⟨(.rβ€˜ndx), βˆ™ ⟩)
4812, 34, 47tpeq123d 4747 . . . . . 6 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ {⟨(Baseβ€˜ndx), ran π‘“βŸ©, ⟨(+gβ€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(+gβ€˜π‘Ÿ)π‘ž))⟩}⟩, ⟨(.rβ€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(.rβ€˜π‘Ÿ)π‘ž))⟩}⟩} = {⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(+gβ€˜ndx), ✚ ⟩, ⟨(.rβ€˜ndx), βˆ™ ⟩})
4913fveq2d 6889 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (Scalarβ€˜π‘Ÿ) = (Scalarβ€˜π‘…))
50 imasval.g . . . . . . . . 9 𝐺 = (Scalarβ€˜π‘…)
5149, 50eqtr4di 2784 . . . . . . . 8 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (Scalarβ€˜π‘Ÿ) = 𝐺)
5251opeq2d 4875 . . . . . . 7 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ⟨(Scalarβ€˜ndx), (Scalarβ€˜π‘Ÿ)⟩ = ⟨(Scalarβ€˜ndx), 𝐺⟩)
5351fveq2d 6889 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (Baseβ€˜(Scalarβ€˜π‘Ÿ)) = (Baseβ€˜πΊ))
54 imasval.k . . . . . . . . . . . 12 𝐾 = (Baseβ€˜πΊ)
5553, 54eqtr4di 2784 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (Baseβ€˜(Scalarβ€˜π‘Ÿ)) = 𝐾)
5620sneqd 4635 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ {(π‘“β€˜π‘ž)} = {(πΉβ€˜π‘ž)})
5713fveq2d 6889 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ( ·𝑠 β€˜π‘Ÿ) = ( ·𝑠 β€˜π‘…))
58 imasval.q . . . . . . . . . . . . . 14 Β· = ( ·𝑠 β€˜π‘…)
5957, 58eqtr4di 2784 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ( ·𝑠 β€˜π‘Ÿ) = Β· )
6059oveqd 7422 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (𝑝( ·𝑠 β€˜π‘Ÿ)π‘ž) = (𝑝 Β· π‘ž))
615, 60fveq12d 6892 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (π‘“β€˜(𝑝( ·𝑠 β€˜π‘Ÿ)π‘ž)) = (πΉβ€˜(𝑝 Β· π‘ž)))
6255, 56, 61mpoeq123dv 7480 . . . . . . . . . 10 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (𝑝 ∈ (Baseβ€˜(Scalarβ€˜π‘Ÿ)), π‘₯ ∈ {(π‘“β€˜π‘ž)} ↦ (π‘“β€˜(𝑝( ·𝑠 β€˜π‘Ÿ)π‘ž))) = (𝑝 ∈ 𝐾, π‘₯ ∈ {(πΉβ€˜π‘ž)} ↦ (πΉβ€˜(𝑝 Β· π‘ž))))
6362iuneq2d 5019 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ βˆͺ π‘ž ∈ 𝑉 (𝑝 ∈ (Baseβ€˜(Scalarβ€˜π‘Ÿ)), π‘₯ ∈ {(π‘“β€˜π‘ž)} ↦ (π‘“β€˜(𝑝( ·𝑠 β€˜π‘Ÿ)π‘ž))) = βˆͺ π‘ž ∈ 𝑉 (𝑝 ∈ 𝐾, π‘₯ ∈ {(πΉβ€˜π‘ž)} ↦ (πΉβ€˜(𝑝 Β· π‘ž))))
6418iuneq1d 5017 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ βˆͺ π‘ž ∈ 𝑣 (𝑝 ∈ (Baseβ€˜(Scalarβ€˜π‘Ÿ)), π‘₯ ∈ {(π‘“β€˜π‘ž)} ↦ (π‘“β€˜(𝑝( ·𝑠 β€˜π‘Ÿ)π‘ž))) = βˆͺ π‘ž ∈ 𝑉 (𝑝 ∈ (Baseβ€˜(Scalarβ€˜π‘Ÿ)), π‘₯ ∈ {(π‘“β€˜π‘ž)} ↦ (π‘“β€˜(𝑝( ·𝑠 β€˜π‘Ÿ)π‘ž))))
65 imasval.s . . . . . . . . . 10 (πœ‘ β†’ βŠ— = βˆͺ π‘ž ∈ 𝑉 (𝑝 ∈ 𝐾, π‘₯ ∈ {(πΉβ€˜π‘ž)} ↦ (πΉβ€˜(𝑝 Β· π‘ž))))
6665ad2antrr 723 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ βŠ— = βˆͺ π‘ž ∈ 𝑉 (𝑝 ∈ 𝐾, π‘₯ ∈ {(πΉβ€˜π‘ž)} ↦ (πΉβ€˜(𝑝 Β· π‘ž))))
6763, 64, 663eqtr4d 2776 . . . . . . . 8 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ βˆͺ π‘ž ∈ 𝑣 (𝑝 ∈ (Baseβ€˜(Scalarβ€˜π‘Ÿ)), π‘₯ ∈ {(π‘“β€˜π‘ž)} ↦ (π‘“β€˜(𝑝( ·𝑠 β€˜π‘Ÿ)π‘ž))) = βŠ— )
6867opeq2d 4875 . . . . . . 7 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ⟨( ·𝑠 β€˜ndx), βˆͺ π‘ž ∈ 𝑣 (𝑝 ∈ (Baseβ€˜(Scalarβ€˜π‘Ÿ)), π‘₯ ∈ {(π‘“β€˜π‘ž)} ↦ (π‘“β€˜(𝑝( ·𝑠 β€˜π‘Ÿ)π‘ž)))⟩ = ⟨( ·𝑠 β€˜ndx), βŠ— ⟩)
6913fveq2d 6889 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (Β·π‘–β€˜π‘Ÿ) = (Β·π‘–β€˜π‘…))
70 imasval.i . . . . . . . . . . . . . . 15 , = (Β·π‘–β€˜π‘…)
7169, 70eqtr4di 2784 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (Β·π‘–β€˜π‘Ÿ) = , )
7271oveqd 7422 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (𝑝(Β·π‘–β€˜π‘Ÿ)π‘ž) = (𝑝 , π‘ž))
7321, 72opeq12d 4876 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (𝑝(Β·π‘–β€˜π‘Ÿ)π‘ž)⟩ = ⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (𝑝 , π‘ž)⟩)
7473sneqd 4635 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (𝑝(Β·π‘–β€˜π‘Ÿ)π‘ž)⟩} = {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (𝑝 , π‘ž)⟩})
7518, 74iuneq12d 5018 . . . . . . . . . 10 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (𝑝(Β·π‘–β€˜π‘Ÿ)π‘ž)⟩} = βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (𝑝 , π‘ž)⟩})
7618, 75iuneq12d 5018 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (𝑝(Β·π‘–β€˜π‘Ÿ)π‘ž)⟩} = βˆͺ 𝑝 ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (𝑝 , π‘ž)⟩})
77 imasval.w . . . . . . . . . 10 (πœ‘ β†’ 𝐼 = βˆͺ 𝑝 ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (𝑝 , π‘ž)⟩})
7877ad2antrr 723 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ 𝐼 = βˆͺ 𝑝 ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (𝑝 , π‘ž)⟩})
7976, 78eqtr4d 2769 . . . . . . . 8 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (𝑝(Β·π‘–β€˜π‘Ÿ)π‘ž)⟩} = 𝐼)
8079opeq2d 4875 . . . . . . 7 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ⟨(Β·π‘–β€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (𝑝(Β·π‘–β€˜π‘Ÿ)π‘ž)⟩}⟩ = ⟨(Β·π‘–β€˜ndx), 𝐼⟩)
8152, 68, 80tpeq123d 4747 . . . . . 6 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ {⟨(Scalarβ€˜ndx), (Scalarβ€˜π‘Ÿ)⟩, ⟨( ·𝑠 β€˜ndx), βˆͺ π‘ž ∈ 𝑣 (𝑝 ∈ (Baseβ€˜(Scalarβ€˜π‘Ÿ)), π‘₯ ∈ {(π‘“β€˜π‘ž)} ↦ (π‘“β€˜(𝑝( ·𝑠 β€˜π‘Ÿ)π‘ž)))⟩, ⟨(Β·π‘–β€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (𝑝(Β·π‘–β€˜π‘Ÿ)π‘ž)⟩}⟩} = {⟨(Scalarβ€˜ndx), 𝐺⟩, ⟨( ·𝑠 β€˜ndx), βŠ— ⟩, ⟨(Β·π‘–β€˜ndx), 𝐼⟩})
8248, 81uneq12d 4159 . . . . 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 6889 . . . . . . . . . 10 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (TopOpenβ€˜π‘Ÿ) = (TopOpenβ€˜π‘…))
84 imasval.j . . . . . . . . . 10 𝐽 = (TopOpenβ€˜π‘…)
8583, 84eqtr4di 2784 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (TopOpenβ€˜π‘Ÿ) = 𝐽)
8685, 5oveq12d 7423 . . . . . . . 8 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ((TopOpenβ€˜π‘Ÿ) qTop 𝑓) = (𝐽 qTop 𝐹))
87 imasval.o . . . . . . . . 9 (πœ‘ β†’ 𝑂 = (𝐽 qTop 𝐹))
8887ad2antrr 723 . . . . . . . 8 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ 𝑂 = (𝐽 qTop 𝐹))
8986, 88eqtr4d 2769 . . . . . . 7 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ((TopOpenβ€˜π‘Ÿ) qTop 𝑓) = 𝑂)
9089opeq2d 4875 . . . . . 6 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ⟨(TopSetβ€˜ndx), ((TopOpenβ€˜π‘Ÿ) qTop 𝑓)⟩ = ⟨(TopSetβ€˜ndx), π‘‚βŸ©)
9113fveq2d 6889 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (leβ€˜π‘Ÿ) = (leβ€˜π‘…))
92 imasval.n . . . . . . . . . . 11 𝑁 = (leβ€˜π‘…)
9391, 92eqtr4di 2784 . . . . . . . . . 10 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (leβ€˜π‘Ÿ) = 𝑁)
945, 93coeq12d 5858 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (𝑓 ∘ (leβ€˜π‘Ÿ)) = (𝐹 ∘ 𝑁))
955cnveqd 5869 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ◑𝑓 = ◑𝐹)
9694, 95coeq12d 5858 . . . . . . . 8 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ((𝑓 ∘ (leβ€˜π‘Ÿ)) ∘ ◑𝑓) = ((𝐹 ∘ 𝑁) ∘ ◑𝐹))
97 imasval.l . . . . . . . . 9 (πœ‘ β†’ ≀ = ((𝐹 ∘ 𝑁) ∘ ◑𝐹))
9897ad2antrr 723 . . . . . . . 8 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ≀ = ((𝐹 ∘ 𝑁) ∘ ◑𝐹))
9996, 98eqtr4d 2769 . . . . . . 7 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ((𝑓 ∘ (leβ€˜π‘Ÿ)) ∘ ◑𝑓) = ≀ )
10099opeq2d 4875 . . . . . 6 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ⟨(leβ€˜ndx), ((𝑓 ∘ (leβ€˜π‘Ÿ)) ∘ ◑𝑓)⟩ = ⟨(leβ€˜ndx), ≀ ⟩)
10118sqxpeqd 5701 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (𝑣 Γ— 𝑣) = (𝑉 Γ— 𝑉))
102101oveq1d 7420 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ((𝑣 Γ— 𝑣) ↑m (1...𝑛)) = ((𝑉 Γ— 𝑉) ↑m (1...𝑛)))
1035fveq1d 6887 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (π‘“β€˜(1st β€˜(β„Žβ€˜1))) = (πΉβ€˜(1st β€˜(β„Žβ€˜1))))
104103eqeq1d 2728 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ((π‘“β€˜(1st β€˜(β„Žβ€˜1))) = π‘₯ ↔ (πΉβ€˜(1st β€˜(β„Žβ€˜1))) = π‘₯))
1055fveq1d 6887 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (π‘“β€˜(2nd β€˜(β„Žβ€˜π‘›))) = (πΉβ€˜(2nd β€˜(β„Žβ€˜π‘›))))
106105eqeq1d 2728 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ((π‘“β€˜(2nd β€˜(β„Žβ€˜π‘›))) = 𝑦 ↔ (πΉβ€˜(2nd β€˜(β„Žβ€˜π‘›))) = 𝑦))
1075fveq1d 6887 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (π‘“β€˜(2nd β€˜(β„Žβ€˜π‘–))) = (πΉβ€˜(2nd β€˜(β„Žβ€˜π‘–))))
1085fveq1d 6887 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (π‘“β€˜(1st β€˜(β„Žβ€˜(𝑖 + 1)))) = (πΉβ€˜(1st β€˜(β„Žβ€˜(𝑖 + 1)))))
109107, 108eqeq12d 2742 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ((π‘“β€˜(2nd β€˜(β„Žβ€˜π‘–))) = (π‘“β€˜(1st β€˜(β„Žβ€˜(𝑖 + 1)))) ↔ (πΉβ€˜(2nd β€˜(β„Žβ€˜π‘–))) = (πΉβ€˜(1st β€˜(β„Žβ€˜(𝑖 + 1))))))
110109ralbidv 3171 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (βˆ€π‘– ∈ (1...(𝑛 βˆ’ 1))(π‘“β€˜(2nd β€˜(β„Žβ€˜π‘–))) = (π‘“β€˜(1st β€˜(β„Žβ€˜(𝑖 + 1)))) ↔ βˆ€π‘– ∈ (1...(𝑛 βˆ’ 1))(πΉβ€˜(2nd β€˜(β„Žβ€˜π‘–))) = (πΉβ€˜(1st β€˜(β„Žβ€˜(𝑖 + 1))))))
111104, 106, 1103anbi123d 1432 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (((π‘“β€˜(1st β€˜(β„Žβ€˜1))) = π‘₯ ∧ (π‘“β€˜(2nd β€˜(β„Žβ€˜π‘›))) = 𝑦 ∧ βˆ€π‘– ∈ (1...(𝑛 βˆ’ 1))(π‘“β€˜(2nd β€˜(β„Žβ€˜π‘–))) = (π‘“β€˜(1st β€˜(β„Žβ€˜(𝑖 + 1))))) ↔ ((πΉβ€˜(1st β€˜(β„Žβ€˜1))) = π‘₯ ∧ (πΉβ€˜(2nd β€˜(β„Žβ€˜π‘›))) = 𝑦 ∧ βˆ€π‘– ∈ (1...(𝑛 βˆ’ 1))(πΉβ€˜(2nd β€˜(β„Žβ€˜π‘–))) = (πΉβ€˜(1st β€˜(β„Žβ€˜(𝑖 + 1)))))))
112102, 111rabeqbidv 3443 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ {β„Ž ∈ ((𝑣 Γ— 𝑣) ↑m (1...𝑛)) ∣ ((π‘“β€˜(1st β€˜(β„Žβ€˜1))) = π‘₯ ∧ (π‘“β€˜(2nd β€˜(β„Žβ€˜π‘›))) = 𝑦 ∧ βˆ€π‘– ∈ (1...(𝑛 βˆ’ 1))(π‘“β€˜(2nd β€˜(β„Žβ€˜π‘–))) = (π‘“β€˜(1st β€˜(β„Žβ€˜(𝑖 + 1)))))} = {β„Ž ∈ ((𝑉 Γ— 𝑉) ↑m (1...𝑛)) ∣ ((πΉβ€˜(1st β€˜(β„Žβ€˜1))) = π‘₯ ∧ (πΉβ€˜(2nd β€˜(β„Žβ€˜π‘›))) = 𝑦 ∧ βˆ€π‘– ∈ (1...(𝑛 βˆ’ 1))(πΉβ€˜(2nd β€˜(β„Žβ€˜π‘–))) = (πΉβ€˜(1st β€˜(β„Žβ€˜(𝑖 + 1)))))})
11313fveq2d 6889 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (distβ€˜π‘Ÿ) = (distβ€˜π‘…))
114 imasval.e . . . . . . . . . . . . . . . 16 𝐸 = (distβ€˜π‘…)
115113, 114eqtr4di 2784 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (distβ€˜π‘Ÿ) = 𝐸)
116115coeq1d 5855 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ((distβ€˜π‘Ÿ) ∘ 𝑔) = (𝐸 ∘ 𝑔))
117116oveq2d 7421 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (ℝ*𝑠 Ξ£g ((distβ€˜π‘Ÿ) ∘ 𝑔)) = (ℝ*𝑠 Ξ£g (𝐸 ∘ 𝑔)))
118112, 117mpteq12dv 5232 . . . . . . . . . . . 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 5931 . . . . . . . . . . 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 5019 . . . . . . . . . 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 9474 . . . . . . . . 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 7480 . . . . . . . 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 723 . . . . . . . 8 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ 𝐷 = (π‘₯ ∈ 𝐡, 𝑦 ∈ 𝐡 ↦ inf(βˆͺ 𝑛 ∈ β„• ran (𝑔 ∈ {β„Ž ∈ ((𝑉 Γ— 𝑉) ↑m (1...𝑛)) ∣ ((πΉβ€˜(1st β€˜(β„Žβ€˜1))) = π‘₯ ∧ (πΉβ€˜(2nd β€˜(β„Žβ€˜π‘›))) = 𝑦 ∧ βˆ€π‘– ∈ (1...(𝑛 βˆ’ 1))(πΉβ€˜(2nd β€˜(β„Žβ€˜π‘–))) = (πΉβ€˜(1st β€˜(β„Žβ€˜(𝑖 + 1)))))} ↦ (ℝ*𝑠 Ξ£g (𝐸 ∘ 𝑔))), ℝ*, < )))
125122, 124eqtr4d 2769 . . . . . . 7 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (π‘₯ ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf(βˆͺ 𝑛 ∈ β„• ran (𝑔 ∈ {β„Ž ∈ ((𝑣 Γ— 𝑣) ↑m (1...𝑛)) ∣ ((π‘“β€˜(1st β€˜(β„Žβ€˜1))) = π‘₯ ∧ (π‘“β€˜(2nd β€˜(β„Žβ€˜π‘›))) = 𝑦 ∧ βˆ€π‘– ∈ (1...(𝑛 βˆ’ 1))(π‘“β€˜(2nd β€˜(β„Žβ€˜π‘–))) = (π‘“β€˜(1st β€˜(β„Žβ€˜(𝑖 + 1)))))} ↦ (ℝ*𝑠 Ξ£g ((distβ€˜π‘Ÿ) ∘ 𝑔))), ℝ*, < )) = 𝐷)
126125opeq2d 4875 . . . . . 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 4747 . . . . 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 4159 . . . 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 3926 . . 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 6799 . . . . 5 (𝐹:𝑉–onto→𝐡 β†’ 𝐹:π‘‰βŸΆπ΅)
1317, 130syl 17 . . . 4 (πœ‘ β†’ 𝐹:π‘‰βŸΆπ΅)
132 fvex 6898 . . . . 5 (Baseβ€˜π‘…) ∈ V
13316, 132eqeltrdi 2835 . . . 4 (πœ‘ β†’ 𝑉 ∈ V)
134131, 133fexd 7224 . . 3 (πœ‘ β†’ 𝐹 ∈ V)
135 imasval.r . . . 4 (πœ‘ β†’ 𝑅 ∈ 𝑍)
136135elexd 3489 . . 3 (πœ‘ β†’ 𝑅 ∈ V)
137 tpex 7731 . . . . . 6 {⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(+gβ€˜ndx), ✚ ⟩, ⟨(.rβ€˜ndx), βˆ™ ⟩} ∈ V
138 tpex 7731 . . . . . 6 {⟨(Scalarβ€˜ndx), 𝐺⟩, ⟨( ·𝑠 β€˜ndx), βŠ— ⟩, ⟨(Β·π‘–β€˜ndx), 𝐼⟩} ∈ V
139137, 138unex 7730 . . . . 5 ({⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(+gβ€˜ndx), ✚ ⟩, ⟨(.rβ€˜ndx), βˆ™ ⟩} βˆͺ {⟨(Scalarβ€˜ndx), 𝐺⟩, ⟨( ·𝑠 β€˜ndx), βŠ— ⟩, ⟨(Β·π‘–β€˜ndx), 𝐼⟩}) ∈ V
140 tpex 7731 . . . . 5 {⟨(TopSetβ€˜ndx), π‘‚βŸ©, ⟨(leβ€˜ndx), ≀ ⟩, ⟨(distβ€˜ndx), 𝐷⟩} ∈ V
141139, 140unex 7730 . . . 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 7556 . 2 (πœ‘ β†’ (𝐹 β€œs 𝑅) = (({⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(+gβ€˜ndx), ✚ ⟩, ⟨(.rβ€˜ndx), βˆ™ ⟩} βˆͺ {⟨(Scalarβ€˜ndx), 𝐺⟩, ⟨( ·𝑠 β€˜ndx), βŠ— ⟩, ⟨(Β·π‘–β€˜ndx), 𝐼⟩}) βˆͺ {⟨(TopSetβ€˜ndx), π‘‚βŸ©, ⟨(leβ€˜ndx), ≀ ⟩, ⟨(distβ€˜ndx), 𝐷⟩}))
1441, 143eqtrd 2766 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 395   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  βˆ€wral 3055  {crab 3426  Vcvv 3468  β¦‹csb 3888   βˆͺ cun 3941  {csn 4623  {ctp 4627  βŸ¨cop 4629  βˆͺ ciun 4990   ↦ cmpt 5224   Γ— cxp 5667  β—‘ccnv 5668  ran crn 5670   ∘ ccom 5673  βŸΆwf 6533  β€“ontoβ†’wfo 6535  β€˜cfv 6537  (class class class)co 7405   ∈ cmpo 7407  1st c1st 7972  2nd c2nd 7973   ↑m cmap 8822  infcinf 9438  1c1 11113   + caddc 11115  β„*cxr 11251   < clt 11252   βˆ’ cmin 11448  β„•cn 12216  ...cfz 13490  ndxcnx 17135  Basecbs 17153  +gcplusg 17206  .rcmulr 17207  Scalarcsca 17209   ·𝑠 cvsca 17210  Β·π‘–cip 17211  TopSetcts 17212  lecple 17213  distcds 17215  TopOpenctopn 17376   Ξ£g cgsu 17395  β„*𝑠cxrs 17455   qTop cqtop 17458   β€œs cimas 17459
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pr 5420  ax-un 7722
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-ral 3056  df-rex 3065  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4903  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7408  df-oprab 7409  df-mpo 7410  df-sup 9439  df-inf 9440  df-imas 17463
This theorem is referenced by:  imasbas  17467  imasds  17468  imasplusg  17472  imasmulr  17473  imassca  17474  imasvsca  17475  imasip  17476  imastset  17477  imasle  17478
  Copyright terms: Public domain W3C validator