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

Theorem imasval 16092
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 (𝑔 ∈ { ∈ ((𝑉 × 𝑉) ↑𝑚 (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 16089 . . . 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 (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (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 (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩})))
4 fvex 6158 . . . . 5 (Base‘𝑟) ∈ V
54a1i 11 . . . 4 ((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) → (Base‘𝑟) ∈ V)
6 simplrl 799 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑓 = 𝐹)
76rneqd 5313 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ran 𝑓 = ran 𝐹)
8 imasval.f . . . . . . . . . . 11 (𝜑𝐹:𝑉onto𝐵)
9 forn 6075 . . . . . . . . . . 11 (𝐹:𝑉onto𝐵 → ran 𝐹 = 𝐵)
108, 9syl 17 . . . . . . . . . 10 (𝜑 → ran 𝐹 = 𝐵)
1110ad2antrr 761 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ran 𝐹 = 𝐵)
127, 11eqtrd 2655 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ran 𝑓 = 𝐵)
1312opeq2d 4377 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(Base‘ndx), ran 𝑓⟩ = ⟨(Base‘ndx), 𝐵⟩)
14 simplrr 800 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑟 = 𝑅)
1514fveq2d 6152 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Base‘𝑟) = (Base‘𝑅))
16 simpr 477 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑣 = (Base‘𝑟))
17 imasval.v . . . . . . . . . . . 12 (𝜑𝑉 = (Base‘𝑅))
1817ad2antrr 761 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑉 = (Base‘𝑅))
1915, 16, 183eqtr4d 2665 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑣 = 𝑉)
206fveq1d 6150 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓𝑝) = (𝐹𝑝))
216fveq1d 6150 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓𝑞) = (𝐹𝑞))
2220, 21opeq12d 4378 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(𝑓𝑝), (𝑓𝑞)⟩ = ⟨(𝐹𝑝), (𝐹𝑞)⟩)
2314fveq2d 6152 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (+g𝑟) = (+g𝑅))
24 imasval.p . . . . . . . . . . . . . . . 16 + = (+g𝑅)
2523, 24syl6eqr 2673 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (+g𝑟) = + )
2625oveqd 6621 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝(+g𝑟)𝑞) = (𝑝 + 𝑞))
276, 26fveq12d 6154 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(𝑝(+g𝑟)𝑞)) = (𝐹‘(𝑝 + 𝑞)))
2822, 27opeq12d 4378 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩ = ⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩)
2928sneqd 4160 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩} = {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
3019, 29iuneq12d 4512 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩} = 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
3119, 30iuneq12d 4512 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩} = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
32 imasval.a . . . . . . . . . 10 (𝜑 = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
3332ad2antrr 761 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
3431, 33eqtr4d 2658 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩} = )
3534opeq2d 4377 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(+g‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩}⟩ = ⟨(+g‘ndx), ⟩)
3614fveq2d 6152 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (.r𝑟) = (.r𝑅))
37 imasval.m . . . . . . . . . . . . . . . 16 × = (.r𝑅)
3836, 37syl6eqr 2673 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (.r𝑟) = × )
3938oveqd 6621 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝(.r𝑟)𝑞) = (𝑝 × 𝑞))
406, 39fveq12d 6154 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(𝑝(.r𝑟)𝑞)) = (𝐹‘(𝑝 × 𝑞)))
4122, 40opeq12d 4378 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩ = ⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩)
4241sneqd 4160 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩} = {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
4319, 42iuneq12d 4512 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩} = 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
4419, 43iuneq12d 4512 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩} = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
45 imasval.t . . . . . . . . . 10 (𝜑 = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
4645ad2antrr 761 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})
4744, 46eqtr4d 2658 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩} = )
4847opeq2d 4377 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(.r‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩}⟩ = ⟨(.r‘ndx), ⟩)
4913, 35, 48tpeq123d 4253 . . . . . 6 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨(Base‘ndx), ran 𝑓⟩, ⟨(+g‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(+g𝑟)𝑞))⟩}⟩, ⟨(.r‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑓‘(𝑝(.r𝑟)𝑞))⟩}⟩} = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩})
5014fveq2d 6152 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Scalar‘𝑟) = (Scalar‘𝑅))
51 imasval.g . . . . . . . . 9 𝐺 = (Scalar‘𝑅)
5250, 51syl6eqr 2673 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Scalar‘𝑟) = 𝐺)
5352opeq2d 4377 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(Scalar‘ndx), (Scalar‘𝑟)⟩ = ⟨(Scalar‘ndx), 𝐺⟩)
5452fveq2d 6152 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Base‘(Scalar‘𝑟)) = (Base‘𝐺))
55 imasval.k . . . . . . . . . . . 12 𝐾 = (Base‘𝐺)
5654, 55syl6eqr 2673 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (Base‘(Scalar‘𝑟)) = 𝐾)
5721sneqd 4160 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {(𝑓𝑞)} = {(𝐹𝑞)})
5814fveq2d 6152 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ( ·𝑠𝑟) = ( ·𝑠𝑅))
59 imasval.q . . . . . . . . . . . . . 14 · = ( ·𝑠𝑅)
6058, 59syl6eqr 2673 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ( ·𝑠𝑟) = · )
6160oveqd 6621 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝( ·𝑠𝑟)𝑞) = (𝑝 · 𝑞))
626, 61fveq12d 6154 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(𝑝( ·𝑠𝑟)𝑞)) = (𝐹‘(𝑝 · 𝑞)))
6356, 57, 62mpt2eq123dv 6670 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞))) = (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
6463iuneq2d 4513 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑞𝑉 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞))) = 𝑞𝑉 (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
6519iuneq1d 4511 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑞𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞))) = 𝑞𝑉 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞))))
66 imasval.s . . . . . . . . . 10 (𝜑 = 𝑞𝑉 (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
6766ad2antrr 761 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → = 𝑞𝑉 (𝑝𝐾, 𝑥 ∈ {(𝐹𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
6864, 65, 673eqtr4d 2665 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑞𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞))) = )
6968opeq2d 4377 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨( ·𝑠 ‘ndx), 𝑞𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞)))⟩ = ⟨( ·𝑠 ‘ndx), ⟩)
7014fveq2d 6152 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (·𝑖𝑟) = (·𝑖𝑅))
71 imasval.i . . . . . . . . . . . . . . 15 , = (·𝑖𝑅)
7270, 71syl6eqr 2673 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (·𝑖𝑟) = , )
7372oveqd 6621 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑝(·𝑖𝑟)𝑞) = (𝑝 , 𝑞))
7422, 73opeq12d 4378 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩ = ⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝑝 , 𝑞)⟩)
7574sneqd 4160 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩} = {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝑝 , 𝑞)⟩})
7619, 75iuneq12d 4512 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩} = 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝑝 , 𝑞)⟩})
7719, 76iuneq12d 4512 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩} = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝑝 , 𝑞)⟩})
78 imasval.w . . . . . . . . . 10 (𝜑𝐼 = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝑝 , 𝑞)⟩})
7978ad2antrr 761 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝐼 = 𝑝𝑉 𝑞𝑉 {⟨⟨(𝐹𝑝), (𝐹𝑞)⟩, (𝑝 , 𝑞)⟩})
8077, 79eqtr4d 2658 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩} = 𝐼)
8180opeq2d 4377 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(·𝑖‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩}⟩ = ⟨(·𝑖‘ndx), 𝐼⟩)
8253, 69, 81tpeq123d 4253 . . . . . 6 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), 𝑞𝑣 (𝑝 ∈ (Base‘(Scalar‘𝑟)), 𝑥 ∈ {(𝑓𝑞)} ↦ (𝑓‘(𝑝( ·𝑠𝑟)𝑞)))⟩, ⟨(·𝑖‘ndx), 𝑝𝑣 𝑞𝑣 {⟨⟨(𝑓𝑝), (𝑓𝑞)⟩, (𝑝(·𝑖𝑟)𝑞)⟩}⟩} = {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⟩, ⟨(·𝑖‘ndx), 𝐼⟩})
8349, 82uneq12d 3746 . . . . 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), 𝐼⟩}))
8414fveq2d 6152 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (TopOpen‘𝑟) = (TopOpen‘𝑅))
85 imasval.j . . . . . . . . . 10 𝐽 = (TopOpen‘𝑅)
8684, 85syl6eqr 2673 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (TopOpen‘𝑟) = 𝐽)
8786, 6oveq12d 6622 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((TopOpen‘𝑟) qTop 𝑓) = (𝐽 qTop 𝐹))
88 imasval.o . . . . . . . . 9 (𝜑𝑂 = (𝐽 qTop 𝐹))
8988ad2antrr 761 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑂 = (𝐽 qTop 𝐹))
9087, 89eqtr4d 2658 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((TopOpen‘𝑟) qTop 𝑓) = 𝑂)
9190opeq2d 4377 . . . . . 6 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(TopSet‘ndx), ((TopOpen‘𝑟) qTop 𝑓)⟩ = ⟨(TopSet‘ndx), 𝑂⟩)
9214fveq2d 6152 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (le‘𝑟) = (le‘𝑅))
93 imasval.n . . . . . . . . . . 11 𝑁 = (le‘𝑅)
9492, 93syl6eqr 2673 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (le‘𝑟) = 𝑁)
956, 94coeq12d 5246 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓 ∘ (le‘𝑟)) = (𝐹𝑁))
966cnveqd 5258 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑓 = 𝐹)
9795, 96coeq12d 5246 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓 ∘ (le‘𝑟)) ∘ 𝑓) = ((𝐹𝑁) ∘ 𝐹))
98 imasval.l . . . . . . . . 9 (𝜑 = ((𝐹𝑁) ∘ 𝐹))
9998ad2antrr 761 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → = ((𝐹𝑁) ∘ 𝐹))
10097, 99eqtr4d 2658 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓 ∘ (le‘𝑟)) ∘ 𝑓) = )
101100opeq2d 4377 . . . . . 6 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(le‘ndx), ((𝑓 ∘ (le‘𝑟)) ∘ 𝑓)⟩ = ⟨(le‘ndx), ⟩)
10219sqxpeqd 5101 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑣 × 𝑣) = (𝑉 × 𝑉))
103102oveq1d 6619 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) = ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)))
1046fveq1d 6150 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(1st ‘(‘1))) = (𝐹‘(1st ‘(‘1))))
105104eqeq1d 2623 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓‘(1st ‘(‘1))) = 𝑥 ↔ (𝐹‘(1st ‘(‘1))) = 𝑥))
1066fveq1d 6150 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(2nd ‘(𝑛))) = (𝐹‘(2nd ‘(𝑛))))
107106eqeq1d 2623 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓‘(2nd ‘(𝑛))) = 𝑦 ↔ (𝐹‘(2nd ‘(𝑛))) = 𝑦))
1086fveq1d 6150 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(2nd ‘(𝑖))) = (𝐹‘(2nd ‘(𝑖))))
1096fveq1d 6150 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑓‘(1st ‘(‘(𝑖 + 1)))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))
110108, 109eqeq12d 2636 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))) ↔ (𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1))))))
111110ralbidv 2980 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))) ↔ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1))))))
112105, 107, 1113anbi123d 1396 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1))))) ↔ ((𝐹‘(1st ‘(‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))))
113103, 112rabeqbidv 3181 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} = { ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))})
11414fveq2d 6152 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (dist‘𝑟) = (dist‘𝑅))
115 imasval.e . . . . . . . . . . . . . . . 16 𝐸 = (dist‘𝑅)
116114, 115syl6eqr 2673 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (dist‘𝑟) = 𝐸)
117116coeq1d 5243 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ((dist‘𝑟) ∘ 𝑔) = (𝐸𝑔))
118117oveq2d 6620 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔)) = (ℝ*𝑠 Σg (𝐸𝑔)))
119113, 118mpteq12dv 4693 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))) = (𝑔 ∈ { ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
120119rneqd 5313 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))) = ran (𝑔 ∈ { ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
121120iuneq2d 4513 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))) = 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
122121infeq1d 8327 . . . . . . . . 9 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ) = inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg (𝐸𝑔))), ℝ*, < ))
12312, 12, 122mpt2eq123dv 6670 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < )) = (𝑥𝐵, 𝑦𝐵 ↦ inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg (𝐸𝑔))), ℝ*, < )))
124 imasval.d . . . . . . . . 9 (𝜑𝐷 = (𝑥𝐵, 𝑦𝐵 ↦ inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg (𝐸𝑔))), ℝ*, < )))
125124ad2antrr 761 . . . . . . . 8 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → 𝐷 = (𝑥𝐵, 𝑦𝐵 ↦ inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg (𝐸𝑔))), ℝ*, < )))
126123, 125eqtr4d 2658 . . . . . . 7 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < )) = 𝐷)
127126opeq2d 4377 . . . . . 6 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → ⟨(dist‘ndx), (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩ = ⟨(dist‘ndx), 𝐷⟩)
12891, 101, 127tpeq123d 4253 . . . . 5 (((𝜑 ∧ (𝑓 = 𝐹𝑟 = 𝑅)) ∧ 𝑣 = (Base‘𝑟)) → {⟨(TopSet‘ndx), ((TopOpen‘𝑟) qTop 𝑓)⟩, ⟨(le‘ndx), ((𝑓 ∘ (le‘𝑟)) ∘ 𝑓)⟩, ⟨(dist‘ndx), (𝑥 ∈ ran 𝑓, 𝑦 ∈ ran 𝑓 ↦ inf( 𝑛 ∈ ℕ ran (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (1...𝑛)) ∣ ((𝑓‘(1st ‘(‘1))) = 𝑥 ∧ (𝑓‘(2nd ‘(𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝑓‘(2nd ‘(𝑖))) = (𝑓‘(1st ‘(‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg ((dist‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩} = {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐷⟩})
12983, 128uneq12d 3746 . . . 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 (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (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), 𝐷⟩}))
1305, 129csbied 3541 . . 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 (𝑔 ∈ { ∈ ((𝑣 × 𝑣) ↑𝑚 (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), 𝐷⟩}))
131 fof 6072 . . . . 5 (𝐹:𝑉onto𝐵𝐹:𝑉𝐵)
1328, 131syl 17 . . . 4 (𝜑𝐹:𝑉𝐵)
133 fvex 6158 . . . . 5 (Base‘𝑅) ∈ V
13417, 133syl6eqel 2706 . . . 4 (𝜑𝑉 ∈ V)
135 fex 6444 . . . 4 ((𝐹:𝑉𝐵𝑉 ∈ V) → 𝐹 ∈ V)
136132, 134, 135syl2anc 692 . . 3 (𝜑𝐹 ∈ V)
137 imasval.r . . . 4 (𝜑𝑅𝑍)
138 elex 3198 . . . 4 (𝑅𝑍𝑅 ∈ V)
139137, 138syl 17 . . 3 (𝜑𝑅 ∈ V)
140 tpex 6910 . . . . . 6 {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩} ∈ V
141 tpex 6910 . . . . . 6 {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⟩, ⟨(·𝑖‘ndx), 𝐼⟩} ∈ V
142140, 141unex 6909 . . . . 5 ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩} ∪ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⟩, ⟨(·𝑖‘ndx), 𝐼⟩}) ∈ V
143 tpex 6910 . . . . 5 {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐷⟩} ∈ V
144142, 143unex 6909 . . . 4 (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩} ∪ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⟩, ⟨(·𝑖‘ndx), 𝐼⟩}) ∪ {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐷⟩}) ∈ V
145144a1i 11 . . 3 (𝜑 → (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩} ∪ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⟩, ⟨(·𝑖‘ndx), 𝐼⟩}) ∪ {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐷⟩}) ∈ V)
1463, 130, 136, 139, 145ovmpt2d 6741 . 2 (𝜑 → (𝐹s 𝑅) = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩} ∪ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⟩, ⟨(·𝑖‘ndx), 𝐼⟩}) ∪ {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐷⟩}))
1471, 146eqtrd 2655 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 384  w3a 1036   = wceq 1480  wcel 1987  wral 2907  {crab 2911  Vcvv 3186  csb 3514  cun 3553  {csn 4148  {ctp 4152  cop 4154   ciun 4485  cmpt 4673   × cxp 5072  ccnv 5073  ran crn 5075  ccom 5078  wf 5843  ontowfo 5845  cfv 5847  (class class class)co 6604  cmpt2 6606  1st c1st 7111  2nd c2nd 7112  𝑚 cmap 7802  infcinf 8291  1c1 9881   + caddc 9883  *cxr 10017   < clt 10018  cmin 10210  cn 10964  ...cfz 12268  ndxcnx 15778  Basecbs 15781  +gcplusg 15862  .rcmulr 15863  Scalarcsca 15865   ·𝑠 cvsca 15866  ·𝑖cip 15867  TopSetcts 15868  lecple 15869  distcds 15871  TopOpenctopn 16003   Σg cgsu 16022  *𝑠cxrs 16081   qTop cqtop 16084  s cimas 16085
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pr 4867  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-sup 8292  df-inf 8293  df-imas 16089
This theorem is referenced by:  imasbas  16093  imasds  16094  imasplusg  16098  imasmulr  16099  imassca  16100  imasvsca  16101  imasip  16102  imastset  16103  imasle  16104
  Copyright terms: Public domain W3C validator