P. 175 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 17401-17500   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-pws 17401*	Define a structure power, which is just a structure product where all the factors are the same. (Contributed by Mario Carneiro, 11-Jan-2015.)
⊢ ↑s = (𝑟 ∈ V, 𝑖 ∈ V ↦ ((Scalar‘𝑟)Xs(𝑖 × {𝑟})))
Theorem	prdsbasex 17402*	Lemma for structure products. (Contributed by Mario Carneiro, 3-Jan-2015.)
⊢ 𝐵 = X𝑥 ∈ dom 𝑅(Base‘(𝑅‘𝑥))    ⇒   ⊢ 𝐵 ∈ V
Theorem	imasvalstr 17403	An image structure value is a structure. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 30-Apr-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
⊢ 𝑈 = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩}) ∪ {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), 𝐿⟩, ⟨(dist‘ndx), 𝐷⟩})    ⇒   ⊢ 𝑈 Struct ⟨1, ;12⟩
Theorem	prdsvalstr 17404	Structure product value is a structure. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 30-Apr-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
⊢ (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩}) ∪ ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), 𝐿⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩})) Struct ⟨1, ;15⟩
Theorem	prdsbaslem 17405	Lemma for prdsbas 17409 and similar theorems. (Contributed by Mario Carneiro, 7-Jan-2017.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 12-Jul-2024.)
⊢ (𝜑 → 𝑈 = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩}) ∪ ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), 𝐿⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩})))    &   ⊢ 𝐴 = (𝐸‘𝑈)    &   ⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑉)    &   ⊢ {⟨(𝐸‘ndx), 𝑇⟩} ⊆ (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩}) ∪ ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), 𝐿⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩}))    ⇒   ⊢ (𝜑 → 𝐴 = 𝑇)
Theorem	prdsvallem 17406*	Lemma for prdsval 17407. (Contributed by Stefan O'Rear, 3-Jan-2015.) Extracted from the former proof of prdsval 17407, dependency on df-hom 17233 removed. (Revised by AV, 13-Oct-2024.)
⊢ (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥))) ∈ V
Theorem	prdsval 17407*	Value of the structure product. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 7-Jan-2017.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
⊢ 𝑃 = (𝑆Xs𝑅)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ (𝜑 → dom 𝑅 = 𝐼)    &   ⊢ (𝜑 → 𝐵 = X𝑥 ∈ 𝐼 (Base‘(𝑅‘𝑥)))    &   ⊢ (𝜑 → + = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥)))))    &   ⊢ (𝜑 → × = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥)))))    &   ⊢ (𝜑 → · = (𝑓 ∈ 𝐾, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥)))))    &   ⊢ (𝜑 → , = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥))))))    &   ⊢ (𝜑 → 𝑂 = (∏t‘(TopOpen ∘ 𝑅)))    &   ⊢ (𝜑 → ≤ = {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))})    &   ⊢ (𝜑 → 𝐷 = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < )))    &   ⊢ (𝜑 → 𝐻 = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥))))    &   ⊢ (𝜑 → ∙ = (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ ((2nd ‘𝑎)𝐻𝑐), 𝑒 ∈ (𝐻‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))))))    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    ⇒   ⊢ (𝜑 → 𝑃 = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩}) ∪ ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ∙ ⟩})))
Theorem	prdssca 17408	Scalar ring of a structure product. (Contributed by Stefan O'Rear, 5-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
⊢ 𝑃 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝑆 = (Scalar‘𝑃))
Theorem	prdsbas 17409*	Base set of a structure product. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
⊢ 𝑃 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → dom 𝑅 = 𝐼)    ⇒   ⊢ (𝜑 → 𝐵 = X𝑥 ∈ 𝐼 (Base‘(𝑅‘𝑥)))
Theorem	prdsplusg 17410*	Addition in a structure product. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
⊢ 𝑃 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → dom 𝑅 = 𝐼)    &   ⊢ + = (+g‘𝑃)    ⇒   ⊢ (𝜑 → + = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(+g‘(𝑅‘𝑥))(𝑔‘𝑥)))))
Theorem	prdsmulr 17411*	Multiplication in a structure product. (Contributed by Mario Carneiro, 11-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
⊢ 𝑃 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → dom 𝑅 = 𝐼)    &   ⊢ · = (.r‘𝑃)    ⇒   ⊢ (𝜑 → · = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(.r‘(𝑅‘𝑥))(𝑔‘𝑥)))))
Theorem	prdsvsca 17412*	Scalar multiplication in a structure product. (Contributed by Stefan O'Rear, 5-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
⊢ 𝑃 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → dom 𝑅 = 𝐼)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ · = ( ·𝑠 ‘𝑃)    ⇒   ⊢ (𝜑 → · = (𝑓 ∈ 𝐾, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ (𝑓( ·𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥)))))
Theorem	prdsip 17413*	Inner product in a structure product. (Contributed by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
⊢ 𝑃 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → dom 𝑅 = 𝐼)    &   ⊢ , = (·𝑖‘𝑃)    ⇒   ⊢ (𝜑 → , = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑅‘𝑥))(𝑔‘𝑥))))))
Theorem	prdsle 17414*	Structure product weak ordering. (Contributed by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
⊢ 𝑃 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → dom 𝑅 = 𝐼)    &   ⊢ ≤ = (le‘𝑃)    ⇒   ⊢ (𝜑 → ≤ = {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))})
Theorem	prdsless 17415	Closure of the order relation on a structure product. (Contributed by Mario Carneiro, 16-Aug-2015.)
⊢ 𝑃 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → dom 𝑅 = 𝐼)    &   ⊢ ≤ = (le‘𝑃)    ⇒   ⊢ (𝜑 → ≤ ⊆ (𝐵 × 𝐵))
Theorem	prdsds 17416*	Structure product distance function. (Contributed by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
⊢ 𝑃 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → dom 𝑅 = 𝐼)    &   ⊢ 𝐷 = (dist‘𝑃)    ⇒   ⊢ (𝜑 → 𝐷 = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < )))
Theorem	prdsdsfn 17417	Structure product distance function. (Contributed by Mario Carneiro, 15-Sep-2015.)
⊢ 𝑃 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → dom 𝑅 = 𝐼)    &   ⊢ 𝐷 = (dist‘𝑃)    ⇒   ⊢ (𝜑 → 𝐷 Fn (𝐵 × 𝐵))
Theorem	prdstset 17418	Structure product topology. (Contributed by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
⊢ 𝑃 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → dom 𝑅 = 𝐼)    &   ⊢ 𝑂 = (TopSet‘𝑃)    ⇒   ⊢ (𝜑 → 𝑂 = (∏t‘(TopOpen ∘ 𝑅)))
Theorem	prdshom 17419*	Structure product hom-sets. (Contributed by Mario Carneiro, 7-Jan-2017.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
⊢ 𝑃 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → dom 𝑅 = 𝐼)    &   ⊢ 𝐻 = (Hom ‘𝑃)    ⇒   ⊢ (𝜑 → 𝐻 = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥))))
Theorem	prdsco 17420*	Structure product composition operation. (Contributed by Mario Carneiro, 7-Jan-2017.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.)
⊢ 𝑃 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ (𝜑 → dom 𝑅 = 𝐼)    &   ⊢ 𝐻 = (Hom ‘𝑃)    &   ⊢ ∙ = (comp‘𝑃)    ⇒   ⊢ (𝜑 → ∙ = (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ ((2nd ‘𝑎)𝐻𝑐), 𝑒 ∈ (𝐻‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))))))
Theorem	prdsbas2 17421*	The base set of a structure product is an indexed set product. (Contributed by Stefan O'Rear, 10-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 Fn 𝐼)    ⇒   ⊢ (𝜑 → 𝐵 = X𝑥 ∈ 𝐼 (Base‘(𝑅‘𝑥)))
Theorem	prdsbasmpt 17422*	A constructed tuple is a point in a structure product iff each coordinate is in the proper base set. (Contributed by Stefan O'Rear, 10-Jan-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 Fn 𝐼)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐼 ↦ 𝑈) ∈ 𝐵 ↔ ∀𝑥 ∈ 𝐼 𝑈 ∈ (Base‘(𝑅‘𝑥))))
Theorem	prdsbasfn 17423	Points in the structure product are functions; use this with dffn5 6890 to establish equalities. (Contributed by Stefan O'Rear, 10-Jan-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 Fn 𝐼)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑇 Fn 𝐼)
Theorem	prdsbasprj 17424	Each point in a structure product restricts on each coordinate to the relevant base set. (Contributed by Stefan O'Rear, 10-Jan-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 Fn 𝐼)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝑇‘𝐽) ∈ (Base‘(𝑅‘𝐽)))
Theorem	prdsplusgval 17425*	Value of a componentwise sum in a structure product. (Contributed by Stefan O'Rear, 10-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 Fn 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ + = (+g‘𝑌)    ⇒   ⊢ (𝜑 → (𝐹 + 𝐺) = (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥)(+g‘(𝑅‘𝑥))(𝐺‘𝑥))))
Theorem	prdsplusgfval 17426	Value of a structure product sum at a single coordinate. (Contributed by Stefan O'Rear, 10-Jan-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 Fn 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ + = (+g‘𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐼)    ⇒   ⊢ (𝜑 → ((𝐹 + 𝐺)‘𝐽) = ((𝐹‘𝐽)(+g‘(𝑅‘𝐽))(𝐺‘𝐽)))
Theorem	prdsmulrval 17427*	Value of a componentwise ring product in a structure product. (Contributed by Mario Carneiro, 11-Jan-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 Fn 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ · = (.r‘𝑌)    ⇒   ⊢ (𝜑 → (𝐹 · 𝐺) = (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥)(.r‘(𝑅‘𝑥))(𝐺‘𝑥))))
Theorem	prdsmulrfval 17428	Value of a structure product's ring product at a single coordinate. (Contributed by Mario Carneiro, 11-Jan-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 Fn 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ · = (.r‘𝑌)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐼)    ⇒   ⊢ (𝜑 → ((𝐹 · 𝐺)‘𝐽) = ((𝐹‘𝐽)(.r‘(𝑅‘𝐽))(𝐺‘𝐽)))
Theorem	prdsleval 17429*	Value of the product ordering in a structure product. (Contributed by Mario Carneiro, 15-Aug-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 Fn 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ ≤ = (le‘𝑌)    ⇒   ⊢ (𝜑 → (𝐹 ≤ 𝐺 ↔ ∀𝑥 ∈ 𝐼 (𝐹‘𝑥)(le‘(𝑅‘𝑥))(𝐺‘𝑥)))
Theorem	prdsdsval 17430*	Value of the metric in a structure product. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 Fn 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ 𝐷 = (dist‘𝑌)    ⇒   ⊢ (𝜑 → (𝐹𝐷𝐺) = sup((ran (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥)(dist‘(𝑅‘𝑥))(𝐺‘𝑥))) ∪ {0}), ℝ*, < ))
Theorem	prdsvscaval 17431*	Scalar multiplication in a structure product is pointwise. (Contributed by Stefan O'Rear, 10-Jan-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ · = ( ·𝑠 ‘𝑌)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 Fn 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 · 𝐺) = (𝑥 ∈ 𝐼 ↦ (𝐹( ·𝑠 ‘(𝑅‘𝑥))(𝐺‘𝑥))))
Theorem	prdsvscafval 17432	Scalar multiplication of a single coordinate in a structure product. (Contributed by Stefan O'Rear, 10-Jan-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ · = ( ·𝑠 ‘𝑌)    &   ⊢ 𝐾 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 Fn 𝐼)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐼)    ⇒   ⊢ (𝜑 → ((𝐹 · 𝐺)‘𝐽) = (𝐹( ·𝑠 ‘(𝑅‘𝐽))(𝐺‘𝐽)))
Theorem	prdsbas3 17433*	The base set of an indexed structure product. (Contributed by Mario Carneiro, 13-Sep-2015.)
⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅))    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝑅 ∈ 𝑋)    &   ⊢ 𝐾 = (Base‘𝑅)    ⇒   ⊢ (𝜑 → 𝐵 = X𝑥 ∈ 𝐼 𝐾)
Theorem	prdsbasmpt2 17434*	A constructed tuple is a point in a structure product iff each coordinate is in the proper base set. (Contributed by Mario Carneiro, 3-Jul-2015.) (Revised by Mario Carneiro, 13-Sep-2015.)
⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅))    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝑅 ∈ 𝑋)    &   ⊢ 𝐾 = (Base‘𝑅)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐼 ↦ 𝑈) ∈ 𝐵 ↔ ∀𝑥 ∈ 𝐼 𝑈 ∈ 𝐾))
Theorem	prdsbascl 17435*	An element of the base has projections closed in the factors. (Contributed by Mario Carneiro, 27-Aug-2015.)
⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅))    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝑅 ∈ 𝑋)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 (𝐹‘𝑥) ∈ 𝐾)
Theorem	prdsdsval2 17436*	Value of the metric in a structure product. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅))    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝑅 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ 𝐸 = (dist‘𝑅)    &   ⊢ 𝐷 = (dist‘𝑌)    ⇒   ⊢ (𝜑 → (𝐹𝐷𝐺) = sup((ran (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥)𝐸(𝐺‘𝑥))) ∪ {0}), ℝ*, < ))
Theorem	prdsdsval3 17437*	Value of the metric in a structure product. (Contributed by Mario Carneiro, 27-Aug-2015.)
⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅))    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝑅 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐸 = ((dist‘𝑅) ↾ (𝐾 × 𝐾))    &   ⊢ 𝐷 = (dist‘𝑌)    ⇒   ⊢ (𝜑 → (𝐹𝐷𝐺) = sup((ran (𝑥 ∈ 𝐼 ↦ ((𝐹‘𝑥)𝐸(𝐺‘𝑥))) ∪ {0}), ℝ*, < ))
Theorem	pwsval 17438	Value of a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐹 = (Scalar‘𝑅)    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝑌 = (𝐹Xs(𝐼 × {𝑅})))
Theorem	pwsbas 17439	Base set of a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (𝐵 ↑m 𝐼) = (Base‘𝑌))
Theorem	pwselbasb 17440	Membership in the base set of a structure product. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑉 = (Base‘𝑌)    ⇒   ⊢ ((𝑅 ∈ 𝑊 ∧ 𝐼 ∈ 𝑍) → (𝑋 ∈ 𝑉 ↔ 𝑋:𝐼⟶𝐵))
Theorem	pwselbas 17441	An element of a structure power is a function from the index set to the base set of the structure. (Contributed by Mario Carneiro, 11-Jan-2015.) (Revised by Mario Carneiro, 5-Jun-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑉 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑍)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝑋:𝐼⟶𝐵)
Theorem	pwselbasr 17442	The reverse direction of pwselbasb 17440: a function between the index and base set of a structure is an element of the structure power. (Contributed by SN, 29-Jul-2024.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑉 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑍)    &   ⊢ (𝜑 → 𝑋:𝐼⟶𝐵)    ⇒   ⊢ (𝜑 → 𝑋 ∈ 𝑉)
Theorem	pwsplusgval 17443	Value of addition in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ✚ = (+g‘𝑌)    ⇒   ⊢ (𝜑 → (𝐹 ✚ 𝐺) = (𝐹 ∘f + 𝐺))
Theorem	pwsmulrval 17444	Value of multiplication in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∙ = (.r‘𝑌)    ⇒   ⊢ (𝜑 → (𝐹 ∙ 𝐺) = (𝐹 ∘f · 𝐺))
Theorem	pwsle 17445	Ordering in a structure power. (Contributed by Mario Carneiro, 16-Aug-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝑂 = (le‘𝑅)    &   ⊢ ≤ = (le‘𝑌)    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → ≤ = ( ∘r 𝑂 ∩ (𝐵 × 𝐵)))
Theorem	pwsleval 17446*	Ordering in a structure power. (Contributed by Mario Carneiro, 16-Aug-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝑂 = (le‘𝑅)    &   ⊢ ≤ = (le‘𝑌)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ≤ 𝐺 ↔ ∀𝑥 ∈ 𝐼 (𝐹‘𝑥)𝑂(𝐺‘𝑥)))
Theorem	pwsvscafval 17447	Scalar multiplication in a structure power is pointwise. (Contributed by Mario Carneiro, 11-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ · = ( ·𝑠 ‘𝑅)    &   ⊢ ∙ = ( ·𝑠 ‘𝑌)    &   ⊢ 𝐹 = (Scalar‘𝑅)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ∙ 𝑋) = ((𝐼 × {𝐴}) ∘f · 𝑋))
Theorem	pwsvscaval 17448	Scalar multiplication of a single coordinate in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ · = ( ·𝑠 ‘𝑅)    &   ⊢ ∙ = ( ·𝑠 ‘𝑌)    &   ⊢ 𝐹 = (Scalar‘𝑅)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐼)    ⇒   ⊢ (𝜑 → ((𝐴 ∙ 𝑋)‘𝐽) = (𝐴 · (𝑋‘𝐽)))
Theorem	pwssca 17449	The ring of scalars of a structure power. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝑆 = (Scalar‘𝑅)    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝑆 = (Scalar‘𝑌))
Theorem	pwsdiagel 17450	Membership of diagonal elements in the structure power base set. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑌)    ⇒   ⊢ (((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) ∧ 𝐴 ∈ 𝐵) → (𝐼 × {𝐴}) ∈ 𝐶)
Theorem	pwssnf1o 17451*	Triviality of singleton powers: set equipollence. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s {𝐼})    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ ({𝐼} × {𝑥}))    &   ⊢ 𝐶 = (Base‘𝑌)    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐹:𝐵–1-1-onto→𝐶)
7.1.4  Definition of the structure quotient
Syntax	cordt 17452	Extend class notation with the order topology.
class ordTop
Syntax	cxrs 17453	Extend class notation with the extended real number structure.
class ℝ*𝑠
Definition	df-ordt 17454*	Define the order topology, given an order ≤, written as 𝑟 below. A closed subbasis for the order topology is given by the closed rays [𝑦, +∞) = {𝑧 ∈ 𝑋 ∣ 𝑦 ≤ 𝑧} and (-∞, 𝑦] = {𝑧 ∈ 𝑋 ∣ 𝑧 ≤ 𝑦}, along with (-∞, +∞) = 𝑋 itself. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ ordTop = (𝑟 ∈ V ↦ (topGen‘(fi‘({dom 𝑟} ∪ ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}))))))
Definition	df-xrs 17455*	The extended real number structure. Unlike df-cnfld 21343, the extended real numbers do not have good algebraic properties, so this is not actually a group or anything higher, even though it has just as many operations as df-cnfld 21343. The main interest in this structure is in its ordering, which is complete and compact. The metric described here is an extension of the absolute value metric, but it is not itself a metric because +∞ is infinitely far from all other points. The topology is based on the order and not the extended metric (which would make +∞ an isolated point since there is nothing else in the 1 -ball around it). All components of this structure agree with ℂfld when restricted to ℝ. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ℝ*𝑠 = ({⟨(Base‘ndx), ℝ*⟩, ⟨(+g‘ndx), +𝑒 ⟩, ⟨(.r‘ndx), ·e ⟩} ∪ {⟨(TopSet‘ndx), (ordTop‘ ≤ )⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))⟩})
Syntax	cqtop 17456	Extend class notation with the quotient topology function.
class qTop
Syntax	cimas 17457	Image structure function.
class “s
Syntax	cqus 17458	Quotient structure function.
class /s
Syntax	cxps 17459	Binary product structure function.
class ×s
Definition	df-qtop 17460*	Define the quotient topology given a function 𝑓 and topology 𝑗 on the domain of 𝑓. (Contributed by Mario Carneiro, 23-Mar-2015.)
⊢ qTop = (𝑗 ∈ V, 𝑓 ∈ V ↦ {𝑠 ∈ 𝒫 (𝑓 “ ∪ 𝑗) ∣ ((◡𝑓 “ 𝑠) ∩ ∪ 𝑗) ∈ 𝑗})
Definition	df-imas 17461*	Define an image structure, which takes a structure and a function on the base set, and maps all the operations via the function. For this to work properly 𝑓 must either be injective or satisfy the well-definedness condition 𝑓(𝑎) = 𝑓(𝑐) ∧ 𝑓(𝑏) = 𝑓(𝑑) → 𝑓(𝑎 + 𝑏) = 𝑓(𝑐 + 𝑑) for each relevant operation. Note that although we call this an "image" by association to df-ima 5635, in order to keep the definition simple we consider only the case when the domain of 𝐹 is equal to the base set of 𝑅. Other cases can be achieved by restricting 𝐹 (with df-res 5634) and/or 𝑅 ( with df-ress 17190) to their common domain. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by AV, 6-Oct-2020.)
⊢ “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‘𝑟) ∘ 𝑔))), ℝ*, < ))⟩}))
Definition	df-qus 17462*	Define a quotient ring (or quotient group), which is a special case of an image structure df-imas 17461 where the image function is 𝑥 ↦ [𝑥]𝑒. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ /s = (𝑟 ∈ V, 𝑒 ∈ V ↦ ((𝑥 ∈ (Base‘𝑟) ↦ [𝑥]𝑒) “s 𝑟))
Definition	df-xps 17463*	Define a binary product on structures. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Jim Kingdon, 25-Sep-2023.)
⊢ ×s = (𝑟 ∈ V, 𝑠 ∈ V ↦ (◡(𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) “s ((Scalar‘𝑟)Xs{⟨∅, 𝑟⟩, ⟨1o, 𝑠⟩})))
Theorem	imasval 17464*	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.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ + = (+g‘𝑅)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝐺 = (Scalar‘𝑅)    &   ⊢ 𝐾 = (Base‘𝐺)    &   ⊢ · = ( ·𝑠 ‘𝑅)    &   ⊢ , = (·𝑖‘𝑅)    &   ⊢ 𝐽 = (TopOpen‘𝑅)    &   ⊢ 𝐸 = (dist‘𝑅)    &   ⊢ 𝑁 = (le‘𝑅)    &   ⊢ (𝜑 → ✚ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})    &   ⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 × 𝑞))⟩})    &   ⊢ (𝜑 → ⊗ = ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))    &   ⊢ (𝜑 → 𝐼 = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝑝 , 𝑞)⟩})    &   ⊢ (𝜑 → 𝑂 = (𝐽 qTop 𝐹))    &   ⊢ (𝜑 → 𝐷 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ {ℎ ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)) ∣ ((𝐹‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))), ℝ*, < )))    &   ⊢ (𝜑 → ≤ = ((𝐹 ∘ 𝑁) ∘ ◡𝐹))    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    ⇒   ⊢ (𝜑 → 𝑈 = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), ✚ ⟩, ⟨(.r‘ndx), ∙ ⟩} ∪ {⟨(Scalar‘ndx), 𝐺⟩, ⟨( ·𝑠 ‘ndx), ⊗ ⟩, ⟨(·𝑖‘ndx), 𝐼⟩}) ∪ {⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), 𝐷⟩}))
Theorem	imasbas 17465	The base set 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.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    ⇒   ⊢ (𝜑 → 𝐵 = (Base‘𝑈))
Theorem	imasds 17466*	The distance function 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.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ 𝐸 = (dist‘𝑅)    &   ⊢ 𝐷 = (dist‘𝑈)    ⇒   ⊢ (𝜑 → 𝐷 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ {ℎ ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)) ∣ ((𝐹‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))))} ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))), ℝ*, < )))
Theorem	imasdsfn 17467	The distance function is a function on the base set. (Contributed by Mario Carneiro, 20-Aug-2015.) (Proof shortened by AV, 6-Oct-2020.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ 𝐸 = (dist‘𝑅)    &   ⊢ 𝐷 = (dist‘𝑈)    ⇒   ⊢ (𝜑 → 𝐷 Fn (𝐵 × 𝐵))
Theorem	imasdsval 17468*	The distance function of an image structure. (Contributed by Mario Carneiro, 20-Aug-2015.) (Revised by AV, 6-Oct-2020.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ 𝐸 = (dist‘𝑅)    &   ⊢ 𝐷 = (dist‘𝑈)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑆 = {ℎ ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)) ∣ ((𝐹‘(1st ‘(ℎ‘1))) = 𝑋 ∧ (𝐹‘(2nd ‘(ℎ‘𝑛))) = 𝑌 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))))}    ⇒   ⊢ (𝜑 → (𝑋𝐷𝑌) = inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔))), ℝ*, < ))
Theorem	imasdsval2 17469*	The distance function of an image structure. (Contributed by Mario Carneiro, 20-Aug-2015.) (Revised by AV, 6-Oct-2020.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ 𝐸 = (dist‘𝑅)    &   ⊢ 𝐷 = (dist‘𝑈)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ 𝑆 = {ℎ ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)) ∣ ((𝐹‘(1st ‘(ℎ‘1))) = 𝑋 ∧ (𝐹‘(2nd ‘(ℎ‘𝑛))) = 𝑌 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))))}    &   ⊢ 𝑇 = (𝐸 ↾ (𝑉 × 𝑉))    ⇒   ⊢ (𝜑 → (𝑋𝐷𝑌) = inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝑇 ∘ 𝑔))), ℝ*, < ))
Theorem	imasplusg 17470*	The group operation in an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 11-Jul-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ✚ = (+g‘𝑈)    ⇒   ⊢ (𝜑 → ✚ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 + 𝑞))⟩})
Theorem	imasmulr 17471*	The ring multiplication in an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 11-Jul-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∙ = (.r‘𝑈)    ⇒   ⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})
Theorem	imassca 17472	The scalar field of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ 𝐺 = (Scalar‘𝑅)    ⇒   ⊢ (𝜑 → 𝐺 = (Scalar‘𝑈))
Theorem	imasvsca 17473*	The scalar multiplication operation of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ 𝐺 = (Scalar‘𝑅)    &   ⊢ 𝐾 = (Base‘𝐺)    &   ⊢ · = ( ·𝑠 ‘𝑅)    &   ⊢ ∙ = ( ·𝑠 ‘𝑈)    ⇒   ⊢ (𝜑 → ∙ = ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ 𝐾, 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝 · 𝑞))))
Theorem	imasip 17474*	The inner product of an image structure. (Contributed by Thierry Arnoux, 16-Jun-2019.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ , = (·𝑖‘𝑅)    &   ⊢ 𝐼 = (·𝑖‘𝑈)    ⇒   ⊢ (𝜑 → 𝐼 = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝑝 , 𝑞)⟩})
Theorem	imastset 17475	The topology of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ 𝐽 = (TopOpen‘𝑅)    &   ⊢ 𝑂 = (TopSet‘𝑈)    ⇒   ⊢ (𝜑 → 𝑂 = (𝐽 qTop 𝐹))
Theorem	imasle 17476	The ordering of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ 𝑁 = (le‘𝑅)    &   ⊢ ≤ = (le‘𝑈)    ⇒   ⊢ (𝜑 → ≤ = ((𝐹 ∘ 𝑁) ∘ ◡𝐹))
Theorem	f1ocpbllem 17477	Lemma for f1ocpbl 17478. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝑋)    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → (((𝐹‘𝐴) = (𝐹‘𝐶) ∧ (𝐹‘𝐵) = (𝐹‘𝐷)) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	f1ocpbl 17478	An injection is compatible with any operations on the base set. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝑋)    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → (((𝐹‘𝐴) = (𝐹‘𝐶) ∧ (𝐹‘𝐵) = (𝐹‘𝐷)) → (𝐹‘(𝐴 + 𝐵)) = (𝐹‘(𝐶 + 𝐷))))
Theorem	f1ovscpbl 17479	An injection is compatible with any operations on the base set. (Contributed by Mario Carneiro, 15-Aug-2015.)
⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝑋)    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐹‘𝐵) = (𝐹‘𝐶) → (𝐹‘(𝐴 + 𝐵)) = (𝐹‘(𝐴 + 𝐶))))
Theorem	f1olecpbl 17480	An injection is compatible with any relations on the base set. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝑋)    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → (((𝐹‘𝐴) = (𝐹‘𝐶) ∧ (𝐹‘𝐵) = (𝐹‘𝐷)) → (𝐴𝑁𝐵 ↔ 𝐶𝑁𝐷)))
Theorem	imasaddfnlem 17481*	The image structure operation is a function if the original operation is compatible with the function. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))    &   ⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})    ⇒   ⊢ (𝜑 → ∙ Fn (𝐵 × 𝐵))
Theorem	imasaddvallem 17482*	The operation of an image structure is defined to distribute over the mapping function. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))    &   ⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝐹‘𝑋) ∙ (𝐹‘𝑌)) = (𝐹‘(𝑋 · 𝑌)))
Theorem	imasaddflem 17483*	The image set operations are closed if the original operation is. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))    &   ⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {⟨⟨(𝐹‘𝑝), (𝐹‘𝑞)⟩, (𝐹‘(𝑝 · 𝑞))⟩})    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∙ :(𝐵 × 𝐵)⟶𝐵)
Theorem	imasaddfn 17484*	The image structure's group operation is a function. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 10-Jul-2015.)
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))    &   ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ · = (+g‘𝑅)    &   ⊢ ∙ = (+g‘𝑈)    ⇒   ⊢ (𝜑 → ∙ Fn (𝐵 × 𝐵))
Theorem	imasaddval 17485*	The value of an image structure's group operation. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))    &   ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ · = (+g‘𝑅)    &   ⊢ ∙ = (+g‘𝑈)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝐹‘𝑋) ∙ (𝐹‘𝑌)) = (𝐹‘(𝑋 · 𝑌)))
Theorem	imasaddf 17486*	The image structure's group operation is closed in the base set. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))    &   ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ · = (+g‘𝑅)    &   ⊢ ∙ = (+g‘𝑈)    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∙ :(𝐵 × 𝐵)⟶𝐵)
Theorem	imasmulfn 17487*	The image structure's ring multiplication is a function. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))    &   ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∙ = (.r‘𝑈)    ⇒   ⊢ (𝜑 → ∙ Fn (𝐵 × 𝐵))
Theorem	imasmulval 17488*	The value of an image structure's ring multiplication. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))    &   ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∙ = (.r‘𝑈)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝐹‘𝑋) ∙ (𝐹‘𝑌)) = (𝐹‘(𝑋 · 𝑌)))
Theorem	imasmulf 17489*	The image structure's ring multiplication is closed in the base set. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞))))    &   ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∙ = (.r‘𝑈)    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∙ :(𝐵 × 𝐵)⟶𝐵)
Theorem	imasvscafn 17490*	The image structure's scalar multiplication is a function. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ 𝐺 = (Scalar‘𝑅)    &   ⊢ 𝐾 = (Base‘𝐺)    &   ⊢ · = ( ·𝑠 ‘𝑅)    &   ⊢ ∙ = ( ·𝑠 ‘𝑈)    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((𝐹‘𝑎) = (𝐹‘𝑞) → (𝐹‘(𝑝 · 𝑎)) = (𝐹‘(𝑝 · 𝑞))))    ⇒   ⊢ (𝜑 → ∙ Fn (𝐾 × 𝐵))
Theorem	imasvscaval 17491*	The value of an image structure's scalar multiplication. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ 𝐺 = (Scalar‘𝑅)    &   ⊢ 𝐾 = (Base‘𝐺)    &   ⊢ · = ( ·𝑠 ‘𝑅)    &   ⊢ ∙ = ( ·𝑠 ‘𝑈)    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((𝐹‘𝑎) = (𝐹‘𝑞) → (𝐹‘(𝑝 · 𝑎)) = (𝐹‘(𝑝 · 𝑞))))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉) → (𝑋 ∙ (𝐹‘𝑌)) = (𝐹‘(𝑋 · 𝑌)))
Theorem	imasvscaf 17492*	The image structure's scalar multiplication is closed in the base set. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ 𝐺 = (Scalar‘𝑅)    &   ⊢ 𝐾 = (Base‘𝐺)    &   ⊢ · = ( ·𝑠 ‘𝑅)    &   ⊢ ∙ = ( ·𝑠 ‘𝑈)    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((𝐹‘𝑎) = (𝐹‘𝑞) → (𝐹‘(𝑝 · 𝑎)) = (𝐹‘(𝑝 · 𝑞))))    &   ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∙ :(𝐾 × 𝐵)⟶𝐵)
Theorem	imasless 17493	The order relation defined on an image set is a subset of the base set. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ ≤ = (le‘𝑈)    ⇒   ⊢ (𝜑 → ≤ ⊆ (𝐵 × 𝐵))
Theorem	imasleval 17494*	The value of the image structure's ordering when the order is compatible with the mapping function. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ ≤ = (le‘𝑈)    &   ⊢ 𝑁 = (le‘𝑅)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑐) ∧ (𝐹‘𝑏) = (𝐹‘𝑑)) → (𝑎𝑁𝑏 ↔ 𝑐𝑁𝑑)))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝐹‘𝑋) ≤ (𝐹‘𝑌) ↔ 𝑋𝑁𝑌))
Theorem	qusval 17495*	Value of a quotient structure. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ )    &   ⊢ (𝜑 → ∼ ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    ⇒   ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))
Theorem	quslem 17496*	The function in qusval 17495 is a surjection onto a quotient set. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ )    &   ⊢ (𝜑 → ∼ ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    ⇒   ⊢ (𝜑 → 𝐹:𝑉–onto→(𝑉 / ∼ ))
Theorem	qusin 17497	Restrict the equivalence relation in a quotient structure to the base set. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → ∼ ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ (𝜑 → ( ∼ “ 𝑉) ⊆ 𝑉)    ⇒   ⊢ (𝜑 → 𝑈 = (𝑅 /s ( ∼ ∩ (𝑉 × 𝑉))))
Theorem	qusbas 17498	Base set of a quotient structure. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → ∼ ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    ⇒   ⊢ (𝜑 → (𝑉 / ∼ ) = (Base‘𝑈))
Theorem	quss 17499	The scalar field of a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → ∼ ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ 𝐾 = (Scalar‘𝑅)    ⇒   ⊢ (𝜑 → 𝐾 = (Scalar‘𝑈))
Theorem	divsfval 17500*	Value of the function in qusval 17495. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.)
⊢ (𝜑 → ∼ Er 𝑉)    &   ⊢ (𝜑 → 𝑉 ∈ 𝑊)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ )    ⇒   ⊢ (𝜑 → (𝐹‘𝐴) = [𝐴] ∼ )