![]() |
Metamath
Proof Explorer Theorem List (p. 169 of 454) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | imasmulf 16801* | 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 16802* | The image structure's scalar multiplication is a function. (Contributed by Mario Carneiro, 24-Feb-2015.) |
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) & ⊢ (𝜑 → 𝑅 ∈ 𝑍) & ⊢ 𝐺 = (Scalar‘𝑅) & ⊢ 𝐾 = (Base‘𝐺) & ⊢ · = ( ·𝑠 ‘𝑅) & ⊢ ∙ = ( ·𝑠 ‘𝑈) & ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((𝐹‘𝑎) = (𝐹‘𝑞) → (𝐹‘(𝑝 · 𝑎)) = (𝐹‘(𝑝 · 𝑞)))) ⇒ ⊢ (𝜑 → ∙ Fn (𝐾 × 𝐵)) | ||
Theorem | imasvscaval 16803* | The value of an image structure's scalar multiplication. (Contributed by Mario Carneiro, 24-Feb-2015.) |
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) & ⊢ (𝜑 → 𝑅 ∈ 𝑍) & ⊢ 𝐺 = (Scalar‘𝑅) & ⊢ 𝐾 = (Base‘𝐺) & ⊢ · = ( ·𝑠 ‘𝑅) & ⊢ ∙ = ( ·𝑠 ‘𝑈) & ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐾 ∧ 𝑎 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((𝐹‘𝑎) = (𝐹‘𝑞) → (𝐹‘(𝑝 · 𝑎)) = (𝐹‘(𝑝 · 𝑞)))) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉) → (𝑋 ∙ (𝐹‘𝑌)) = (𝐹‘(𝑋 · 𝑌))) | ||
Theorem | imasvscaf 16804* | 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 16805 | 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 16806* | 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 16807* | Value of a quotient structure. (Contributed by Mario Carneiro, 23-Feb-2015.) |
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ )) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ ) & ⊢ (𝜑 → ∼ ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ 𝑍) ⇒ ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) | ||
Theorem | quslem 16808* | The function in qusval 16807 is a surjection onto a quotient set. (Contributed by Mario Carneiro, 23-Feb-2015.) |
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ )) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ ) & ⊢ (𝜑 → ∼ ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ 𝑍) ⇒ ⊢ (𝜑 → 𝐹:𝑉–onto→(𝑉 / ∼ )) | ||
Theorem | qusin 16809 | Restrict the equivalence relation in a quotient structure to the base set. (Contributed by Mario Carneiro, 23-Feb-2015.) |
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ )) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → ∼ ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ 𝑍) & ⊢ (𝜑 → ( ∼ “ 𝑉) ⊆ 𝑉) ⇒ ⊢ (𝜑 → 𝑈 = (𝑅 /s ( ∼ ∩ (𝑉 × 𝑉)))) | ||
Theorem | qusbas 16810 | Base set of a quotient structure. (Contributed by Mario Carneiro, 23-Feb-2015.) |
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ )) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → ∼ ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ 𝑍) ⇒ ⊢ (𝜑 → (𝑉 / ∼ ) = (Base‘𝑈)) | ||
Theorem | quss 16811 | The scalar field of a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.) |
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ )) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → ∼ ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ 𝑍) & ⊢ 𝐾 = (Scalar‘𝑅) ⇒ ⊢ (𝜑 → 𝐾 = (Scalar‘𝑈)) | ||
Theorem | divsfval 16812* | Value of the function in qusval 16807. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.) |
⊢ (𝜑 → ∼ Er 𝑉) & ⊢ (𝜑 → 𝑉 ∈ 𝑊) & ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ ) ⇒ ⊢ (𝜑 → (𝐹‘𝐴) = [𝐴] ∼ ) | ||
Theorem | ercpbllem 16813* | Lemma for ercpbl 16814. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by AV, 12-Jul-2024.) |
⊢ (𝜑 → ∼ Er 𝑉) & ⊢ (𝜑 → 𝑉 ∈ 𝑊) & ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ ) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝐹‘𝐴) = (𝐹‘𝐵) ↔ 𝐴 ∼ 𝐵)) | ||
Theorem | ercpbl 16814* | Translate the function compatibility relation to a quotient set. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.) |
⊢ (𝜑 → ∼ Er 𝑉) & ⊢ (𝜑 → 𝑉 ∈ 𝑊) & ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ ) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (𝑎 + 𝑏) ∈ 𝑉) & ⊢ (𝜑 → ((𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷) → (𝐴 + 𝐵) ∼ (𝐶 + 𝐷))) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → (((𝐹‘𝐴) = (𝐹‘𝐶) ∧ (𝐹‘𝐵) = (𝐹‘𝐷)) → (𝐹‘(𝐴 + 𝐵)) = (𝐹‘(𝐶 + 𝐷)))) | ||
Theorem | erlecpbl 16815* | Translate the relation compatibility relation to a quotient set. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.) |
⊢ (𝜑 → ∼ Er 𝑉) & ⊢ (𝜑 → 𝑉 ∈ 𝑊) & ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ ) & ⊢ (𝜑 → ((𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷) → (𝐴𝑁𝐵 ↔ 𝐶𝑁𝐷))) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → (((𝐹‘𝐴) = (𝐹‘𝐶) ∧ (𝐹‘𝐵) = (𝐹‘𝐷)) → (𝐴𝑁𝐵 ↔ 𝐶𝑁𝐷))) | ||
Theorem | qusaddvallem 16816* | Value of an operation defined on a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.) |
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ )) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → ∼ Er 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑍) & ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 · 𝑏) ∼ (𝑝 · 𝑞))) & ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉) & ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ ) & ⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ([𝑋] ∼ ∙ [𝑌] ∼ ) = [(𝑋 · 𝑌)] ∼ ) | ||
Theorem | qusaddflem 16817* | The operation of a quotient structure is a function. (Contributed by Mario Carneiro, 24-Feb-2015.) |
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ )) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → ∼ Er 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑍) & ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 · 𝑏) ∼ (𝑝 · 𝑞))) & ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉) & ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ ) & ⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}) ⇒ ⊢ (𝜑 → ∙ :((𝑉 / ∼ ) × (𝑉 / ∼ ))⟶(𝑉 / ∼ )) | ||
Theorem | qusaddval 16818* | The base set of an image structure. (Contributed by Mario Carneiro, 24-Feb-2015.) |
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ )) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → ∼ Er 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑍) & ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 · 𝑏) ∼ (𝑝 · 𝑞))) & ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉) & ⊢ · = (+g‘𝑅) & ⊢ ∙ = (+g‘𝑈) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ([𝑋] ∼ ∙ [𝑌] ∼ ) = [(𝑋 · 𝑌)] ∼ ) | ||
Theorem | qusaddf 16819* | The base set of an image structure. (Contributed by Mario Carneiro, 24-Feb-2015.) |
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ )) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → ∼ Er 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑍) & ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 · 𝑏) ∼ (𝑝 · 𝑞))) & ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉) & ⊢ · = (+g‘𝑅) & ⊢ ∙ = (+g‘𝑈) ⇒ ⊢ (𝜑 → ∙ :((𝑉 / ∼ ) × (𝑉 / ∼ ))⟶(𝑉 / ∼ )) | ||
Theorem | qusmulval 16820* | The base set of an image structure. (Contributed by Mario Carneiro, 24-Feb-2015.) |
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ )) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → ∼ Er 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑍) & ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 · 𝑏) ∼ (𝑝 · 𝑞))) & ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉) & ⊢ · = (.r‘𝑅) & ⊢ ∙ = (.r‘𝑈) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ([𝑋] ∼ ∙ [𝑌] ∼ ) = [(𝑋 · 𝑌)] ∼ ) | ||
Theorem | qusmulf 16821* | The base set of an image structure. (Contributed by Mario Carneiro, 24-Feb-2015.) |
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ )) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → ∼ Er 𝑉) & ⊢ (𝜑 → 𝑅 ∈ 𝑍) & ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 · 𝑏) ∼ (𝑝 · 𝑞))) & ⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 · 𝑞) ∈ 𝑉) & ⊢ · = (.r‘𝑅) & ⊢ ∙ = (.r‘𝑈) ⇒ ⊢ (𝜑 → ∙ :((𝑉 / ∼ ) × (𝑉 / ∼ ))⟶(𝑉 / ∼ )) | ||
Theorem | fnpr2o 16822 | Function with a domain of 2o. (Contributed by Jim Kingdon, 25-Sep-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {〈∅, 𝐴〉, 〈1o, 𝐵〉} Fn 2o) | ||
Theorem | fnpr2ob 16823 | Biconditional version of fnpr2o 16822. (Contributed by Jim Kingdon, 27-Sep-2023.) |
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ {〈∅, 𝐴〉, 〈1o, 𝐵〉} Fn 2o) | ||
Theorem | fvpr0o 16824 | The value of a function with a domain of (at most) two elements. (Contributed by Jim Kingdon, 25-Sep-2023.) |
⊢ (𝐴 ∈ 𝑉 → ({〈∅, 𝐴〉, 〈1o, 𝐵〉}‘∅) = 𝐴) | ||
Theorem | fvpr1o 16825 | The value of a function with a domain of (at most) two elements. (Contributed by Jim Kingdon, 25-Sep-2023.) |
⊢ (𝐵 ∈ 𝑉 → ({〈∅, 𝐴〉, 〈1o, 𝐵〉}‘1o) = 𝐵) | ||
Theorem | fvprif 16826 | The value of the pair function at an element of 2o. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 2o) → ({〈∅, 𝐴〉, 〈1o, 𝐵〉}‘𝐶) = if(𝐶 = ∅, 𝐴, 𝐵)) | ||
Theorem | xpsfrnel 16827* | Elementhood in the target space of the function 𝐹 appearing in xpsval 16835. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ (𝐺 ∈ X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝐺 Fn 2o ∧ (𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵)) | ||
Theorem | xpsfeq 16828 | A function on 2o is determined by its values at zero and one. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ (𝐺 Fn 2o → {〈∅, (𝐺‘∅)〉, 〈1o, (𝐺‘1o)〉} = 𝐺) | ||
Theorem | xpsfrnel2 16829* | Elementhood in the target space of the function 𝐹 appearing in xpsval 16835. (Contributed by Mario Carneiro, 15-Aug-2015.) |
⊢ ({〈∅, 𝑋〉, 〈1o, 𝑌〉} ∈ X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵)) | ||
Theorem | xpscf 16830 | Equivalent condition for the pair function to be a proper function on 𝐴. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ ({〈∅, 𝑋〉, 〈1o, 𝑌〉}:2o⟶𝐴 ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) | ||
Theorem | xpsfval 16831* | The value of the function appearing in xpsval 16835. (Contributed by Mario Carneiro, 15-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) ⇒ ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐹𝑌) = {〈∅, 𝑋〉, 〈1o, 𝑌〉}) | ||
Theorem | xpsff1o 16832* | The function appearing in xpsval 16835 is a bijection from the cartesian product to the indexed cartesian product indexed on the pair 2o = {∅, 1o}. (Contributed by Mario Carneiro, 15-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) ⇒ ⊢ 𝐹:(𝐴 × 𝐵)–1-1-onto→X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) | ||
Theorem | xpsfrn 16833* | A short expression for the indexed cartesian product on two indices. (Contributed by Mario Carneiro, 15-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) ⇒ ⊢ ran 𝐹 = X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) | ||
Theorem | xpsff1o2 16834* | The function appearing in xpsval 16835 is a bijection from the cartesian product to the indexed cartesian product indexed on the pair 2o = {∅, 1o}. (Contributed by Mario Carneiro, 24-Jan-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) ⇒ ⊢ 𝐹:(𝐴 × 𝐵)–1-1-onto→ran 𝐹 | ||
Theorem | xpsval 16835* | Value of the binary structure product function. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Jim Kingdon, 25-Sep-2023.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑌 = (Base‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) & ⊢ 𝐺 = (Scalar‘𝑅) & ⊢ 𝑈 = (𝐺Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}) ⇒ ⊢ (𝜑 → 𝑇 = (◡𝐹 “s 𝑈)) | ||
Theorem | xpsrnbas 16836* | The indexed structure product that appears in xpsval 16835 has the same base as the target of the function 𝐹. (Contributed by Mario Carneiro, 15-Aug-2015.) (Revised by Jim Kingdon, 25-Sep-2023.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑌 = (Base‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) & ⊢ 𝐺 = (Scalar‘𝑅) & ⊢ 𝑈 = (𝐺Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}) ⇒ ⊢ (𝜑 → ran 𝐹 = (Base‘𝑈)) | ||
Theorem | xpsbas 16837 | The base set of the binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑌 = (Base‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝑋 × 𝑌) = (Base‘𝑇)) | ||
Theorem | xpsaddlem 16838* | Lemma for xpsadd 16839 and xpsmul 16840. (Contributed by Mario Carneiro, 15-Aug-2015.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑌 = (Base‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑌) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑌) & ⊢ (𝜑 → (𝐴 · 𝐶) ∈ 𝑋) & ⊢ (𝜑 → (𝐵 × 𝐷) ∈ 𝑌) & ⊢ · = (𝐸‘𝑅) & ⊢ × = (𝐸‘𝑆) & ⊢ ∙ = (𝐸‘𝑇) & ⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) & ⊢ 𝑈 = ((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}) & ⊢ ((𝜑 ∧ {〈∅, 𝐴〉, 〈1o, 𝐵〉} ∈ ran 𝐹 ∧ {〈∅, 𝐶〉, 〈1o, 𝐷〉} ∈ ran 𝐹) → ((◡𝐹‘{〈∅, 𝐴〉, 〈1o, 𝐵〉}) ∙ (◡𝐹‘{〈∅, 𝐶〉, 〈1o, 𝐷〉})) = (◡𝐹‘({〈∅, 𝐴〉, 〈1o, 𝐵〉} (𝐸‘𝑈){〈∅, 𝐶〉, 〈1o, 𝐷〉}))) & ⊢ (({〈∅, 𝑅〉, 〈1o, 𝑆〉} Fn 2o ∧ {〈∅, 𝐴〉, 〈1o, 𝐵〉} ∈ (Base‘𝑈) ∧ {〈∅, 𝐶〉, 〈1o, 𝐷〉} ∈ (Base‘𝑈)) → ({〈∅, 𝐴〉, 〈1o, 𝐵〉} (𝐸‘𝑈){〈∅, 𝐶〉, 〈1o, 𝐷〉}) = (𝑘 ∈ 2o ↦ (({〈∅, 𝐴〉, 〈1o, 𝐵〉}‘𝑘)(𝐸‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘𝑘))({〈∅, 𝐶〉, 〈1o, 𝐷〉}‘𝑘)))) ⇒ ⊢ (𝜑 → (〈𝐴, 𝐵〉 ∙ 〈𝐶, 𝐷〉) = 〈(𝐴 · 𝐶), (𝐵 × 𝐷)〉) | ||
Theorem | xpsadd 16839 | Value of the addition operation in a binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑌 = (Base‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑌) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑌) & ⊢ (𝜑 → (𝐴 · 𝐶) ∈ 𝑋) & ⊢ (𝜑 → (𝐵 × 𝐷) ∈ 𝑌) & ⊢ · = (+g‘𝑅) & ⊢ × = (+g‘𝑆) & ⊢ ∙ = (+g‘𝑇) ⇒ ⊢ (𝜑 → (〈𝐴, 𝐵〉 ∙ 〈𝐶, 𝐷〉) = 〈(𝐴 · 𝐶), (𝐵 × 𝐷)〉) | ||
Theorem | xpsmul 16840 | Value of the multiplication operation in a binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑌 = (Base‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑌) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑌) & ⊢ (𝜑 → (𝐴 · 𝐶) ∈ 𝑋) & ⊢ (𝜑 → (𝐵 × 𝐷) ∈ 𝑌) & ⊢ · = (.r‘𝑅) & ⊢ × = (.r‘𝑆) & ⊢ ∙ = (.r‘𝑇) ⇒ ⊢ (𝜑 → (〈𝐴, 𝐵〉 ∙ 〈𝐶, 𝐷〉) = 〈(𝐴 · 𝐶), (𝐵 × 𝐷)〉) | ||
Theorem | xpssca 16841 | Value of the scalar field of a binary structure product. For concreteness, we choose the scalar field to match the left argument, but in most cases where this slot is meaningful both factors will have the same scalar field, so that it doesn't matter which factor is chosen. (Contributed by Mario Carneiro, 15-Aug-2015.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝐺 = (Scalar‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝐺 = (Scalar‘𝑇)) | ||
Theorem | xpsvsca 16842 | Value of the scalar multiplication function in a binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝐺 = (Scalar‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑌 = (Base‘𝑆) & ⊢ 𝐾 = (Base‘𝐺) & ⊢ · = ( ·𝑠 ‘𝑅) & ⊢ × = ( ·𝑠 ‘𝑆) & ⊢ ∙ = ( ·𝑠 ‘𝑇) & ⊢ (𝜑 → 𝐴 ∈ 𝐾) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) & ⊢ (𝜑 → 𝐶 ∈ 𝑌) & ⊢ (𝜑 → (𝐴 · 𝐵) ∈ 𝑋) & ⊢ (𝜑 → (𝐴 × 𝐶) ∈ 𝑌) ⇒ ⊢ (𝜑 → (𝐴 ∙ 〈𝐵, 𝐶〉) = 〈(𝐴 · 𝐵), (𝐴 × 𝐶)〉) | ||
Theorem | xpsless 16843 | Closure of the ordering in a binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑌 = (Base‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ ≤ = (le‘𝑇) ⇒ ⊢ (𝜑 → ≤ ⊆ ((𝑋 × 𝑌) × (𝑋 × 𝑌))) | ||
Theorem | xpsle 16844 | Value of the ordering in a binary structure product. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑌 = (Base‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ ≤ = (le‘𝑇) & ⊢ 𝑀 = (le‘𝑅) & ⊢ 𝑁 = (le‘𝑆) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑌) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑌) ⇒ ⊢ (𝜑 → (〈𝐴, 𝐵〉 ≤ 〈𝐶, 𝐷〉 ↔ (𝐴𝑀𝐶 ∧ 𝐵𝑁𝐷))) | ||
Syntax | cmre 16845 | The class of Moore systems. |
class Moore | ||
Syntax | cmrc 16846 | The class function generating Moore closures. |
class mrCls | ||
Syntax | cmri 16847 | mrInd is a class function which takes a Moore system to its set of independent sets. |
class mrInd | ||
Syntax | cacs 16848 | The class of algebraic closure (Moore) systems. |
class ACS | ||
Definition | df-mre 16849* |
Define a Moore collection, which is a family of subsets of a base set
which preserve arbitrary intersection. Elements of a Moore collection
are termed closed; Moore collections generalize the notion of
closedness from topologies (cldmre 21683) and vector spaces (lssmre 19731)
to the most general setting in which such concepts make sense.
Definition of Moore collection of sets in [Schechter] p. 78. A Moore
collection may also be called a closure system (Section 0.6 in
[Gratzer] p. 23.) The name Moore
collection is after Eliakim Hastings
Moore, who discussed these systems in Part I of [Moore] p. 53 to 76.
See ismre 16853, mresspw 16855, mre1cl 16857 and mreintcl 16858 for the major properties of a Moore collection. Note that a Moore collection uniquely determines its base set (mreuni 16863); as such the disjoint union of all Moore collections is sometimes considered as ∪ ran Moore, justified by mreunirn 16864. (Contributed by Stefan O'Rear, 30-Jan-2015.) (Revised by David Moews, 1-May-2017.) |
⊢ Moore = (𝑥 ∈ V ↦ {𝑐 ∈ 𝒫 𝒫 𝑥 ∣ (𝑥 ∈ 𝑐 ∧ ∀𝑠 ∈ 𝒫 𝑐(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝑐))}) | ||
Definition | df-mrc 16850* |
Define the Moore closure of a generating set, which is the smallest
closed set containing all generating elements. Definition of Moore
closure in [Schechter] p. 79. This
generalizes topological closure
(mrccls 21684) and linear span (mrclsp 19754).
A Moore closure operation 𝑁 is (1) extensive, i.e., 𝑥 ⊆ (𝑁‘𝑥) for all subsets 𝑥 of the base set (mrcssid 16880), (2) isotone, i.e., 𝑥 ⊆ 𝑦 implies that (𝑁‘𝑥) ⊆ (𝑁‘𝑦) for all subsets 𝑥 and 𝑦 of the base set (mrcss 16879), and (3) idempotent, i.e., (𝑁‘(𝑁‘𝑥)) = (𝑁‘𝑥) for all subsets 𝑥 of the base set (mrcidm 16882.) Operators satisfying these three properties are in bijective correspondence with Moore collections, so these properties may be used to give an alternate characterization of a Moore collection by providing a closure operation 𝑁 on the set of subsets of a given base set which satisfies (1), (2), and (3); the closed sets can be recovered as those sets which equal their closures (Section 4.5 in [Schechter] p. 82.) (Contributed by Stefan O'Rear, 31-Jan-2015.) (Revised by David Moews, 1-May-2017.) |
⊢ mrCls = (𝑐 ∈ ∪ ran Moore ↦ (𝑥 ∈ 𝒫 ∪ 𝑐 ↦ ∩ {𝑠 ∈ 𝑐 ∣ 𝑥 ⊆ 𝑠})) | ||
Definition | df-mri 16851* | In a Moore system, a set is independent if no element of the set is in the closure of the set with the element removed (Section 0.6 in [Gratzer] p. 27; Definition 4.1.1 in [FaureFrolicher] p. 83.) mrInd is a class function which takes a Moore system to its set of independent sets. (Contributed by David Moews, 1-May-2017.) |
⊢ mrInd = (𝑐 ∈ ∪ ran Moore ↦ {𝑠 ∈ 𝒫 ∪ 𝑐 ∣ ∀𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))}) | ||
Definition | df-acs 16852* | An important subclass of Moore systems are those which can be interpreted as closure under some collection of operators of finite arity (the collection itself is not required to be finite). These are termed algebraic closure systems; similar to definition (A) of an algebraic closure system in [Schechter] p. 84, but to avoid the complexity of an arbitrary mixed collection of functions of various arities (especially if the axiom of infinity omex 9090 is to be avoided), we consider a single function defined on finite sets instead. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ ACS = (𝑥 ∈ V ↦ {𝑐 ∈ (Moore‘𝑥) ∣ ∃𝑓(𝑓:𝒫 𝑥⟶𝒫 𝑥 ∧ ∀𝑠 ∈ 𝒫 𝑥(𝑠 ∈ 𝑐 ↔ ∪ (𝑓 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠))}) | ||
Theorem | ismre 16853* | Property of being a Moore collection on some base set. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ (𝐶 ∈ (Moore‘𝑋) ↔ (𝐶 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ 𝐶 ∧ ∀𝑠 ∈ 𝒫 𝐶(𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝐶))) | ||
Theorem | fnmre 16854 | The Moore collection generator is a well-behaved function. Analogue for Moore collections of fntopon 21529 for topologies. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ Moore Fn V | ||
Theorem | mresspw 16855 | A Moore collection is a subset of the power of the base set; each closed subset of the system is actually a subset of the base. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐶 ⊆ 𝒫 𝑋) | ||
Theorem | mress 16856 | A Moore-closed subset is a subset. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑆 ∈ 𝐶) → 𝑆 ⊆ 𝑋) | ||
Theorem | mre1cl 16857 | In any Moore collection the base set is closed. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ (𝐶 ∈ (Moore‘𝑋) → 𝑋 ∈ 𝐶) | ||
Theorem | mreintcl 16858 | A nonempty collection of closed sets has a closed intersection. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑆 ⊆ 𝐶 ∧ 𝑆 ≠ ∅) → ∩ 𝑆 ∈ 𝐶) | ||
Theorem | mreiincl 16859* | A nonempty indexed intersection of closed sets is closed. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝐼 ≠ ∅ ∧ ∀𝑦 ∈ 𝐼 𝑆 ∈ 𝐶) → ∩ 𝑦 ∈ 𝐼 𝑆 ∈ 𝐶) | ||
Theorem | mrerintcl 16860 | The relative intersection of a set of closed sets is closed. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑆 ⊆ 𝐶) → (𝑋 ∩ ∩ 𝑆) ∈ 𝐶) | ||
Theorem | mreriincl 16861* | The relative intersection of a family of closed sets is closed. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑦 ∈ 𝐼 𝑆 ∈ 𝐶) → (𝑋 ∩ ∩ 𝑦 ∈ 𝐼 𝑆) ∈ 𝐶) | ||
Theorem | mreincl 16862 | Two closed sets have a closed intersection. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐴 ∩ 𝐵) ∈ 𝐶) | ||
Theorem | mreuni 16863 | Since the entire base set of a Moore collection is the greatest element of it, the base set can be recovered from a Moore collection by set union. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ (𝐶 ∈ (Moore‘𝑋) → ∪ 𝐶 = 𝑋) | ||
Theorem | mreunirn 16864 | Two ways to express the notion of being a Moore collection on an unspecified base. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ (𝐶 ∈ ∪ ran Moore ↔ 𝐶 ∈ (Moore‘∪ 𝐶)) | ||
Theorem | ismred 16865* | Properties that determine a Moore collection. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ (𝜑 → 𝐶 ⊆ 𝒫 𝑋) & ⊢ (𝜑 → 𝑋 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑠 ⊆ 𝐶 ∧ 𝑠 ≠ ∅) → ∩ 𝑠 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐶 ∈ (Moore‘𝑋)) | ||
Theorem | ismred2 16866* | Properties that determine a Moore collection, using restricted intersection. (Contributed by Stefan O'Rear, 3-Apr-2015.) |
⊢ (𝜑 → 𝐶 ⊆ 𝒫 𝑋) & ⊢ ((𝜑 ∧ 𝑠 ⊆ 𝐶) → (𝑋 ∩ ∩ 𝑠) ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐶 ∈ (Moore‘𝑋)) | ||
Theorem | mremre 16867 | The Moore collections of subsets of a space, viewed as a kind of subset of the power set, form a Moore collection in their own right on the power set. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ (𝑋 ∈ 𝑉 → (Moore‘𝑋) ∈ (Moore‘𝒫 𝑋)) | ||
Theorem | submre 16868 | The subcollection of a closed set system below a given closed set is itself a closed set system. (Contributed by Stefan O'Rear, 9-Mar-2015.) |
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝐴 ∈ 𝐶) → (𝐶 ∩ 𝒫 𝐴) ∈ (Moore‘𝐴)) | ||
Theorem | mrcflem 16869* | The domain and range of the function expression for Moore closures. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ (𝐶 ∈ (Moore‘𝑋) → (𝑥 ∈ 𝒫 𝑋 ↦ ∩ {𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠}):𝒫 𝑋⟶𝐶) | ||
Theorem | fnmrc 16870 | Moore-closure is a well-behaved function. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ mrCls Fn ∪ ran Moore | ||
Theorem | mrcfval 16871* | Value of the function expression for the Moore closure. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐹 = (𝑥 ∈ 𝒫 𝑋 ↦ ∩ {𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠})) | ||
Theorem | mrcf 16872 | The Moore closure is a function mapping arbitrary subsets to closed sets. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐹:𝒫 𝑋⟶𝐶) | ||
Theorem | mrcval 16873* | Evaluation of the Moore closure of a set. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Proof shortened by Fan Zheng, 6-Jun-2016.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋) → (𝐹‘𝑈) = ∩ {𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠}) | ||
Theorem | mrccl 16874 | The Moore closure of a set is a closed set. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋) → (𝐹‘𝑈) ∈ 𝐶) | ||
Theorem | mrcsncl 16875 | The Moore closure of a singleton is a closed set. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ∈ 𝑋) → (𝐹‘{𝑈}) ∈ 𝐶) | ||
Theorem | mrcid 16876 | The closure of a closed set is itself. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ∈ 𝐶) → (𝐹‘𝑈) = 𝑈) | ||
Theorem | mrcssv 16877 | The closure of a set is a subset of the base. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ (𝐶 ∈ (Moore‘𝑋) → (𝐹‘𝑈) ⊆ 𝑋) | ||
Theorem | mrcidb 16878 | A set is closed iff it is equal to its closure. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ (𝐶 ∈ (Moore‘𝑋) → (𝑈 ∈ 𝐶 ↔ (𝐹‘𝑈) = 𝑈)) | ||
Theorem | mrcss 16879 | Closure preserves subset ordering. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑉 ∧ 𝑉 ⊆ 𝑋) → (𝐹‘𝑈) ⊆ (𝐹‘𝑉)) | ||
Theorem | mrcssid 16880 | The closure of a set is a superset. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋) → 𝑈 ⊆ (𝐹‘𝑈)) | ||
Theorem | mrcidb2 16881 | A set is closed iff it contains its closure. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋) → (𝑈 ∈ 𝐶 ↔ (𝐹‘𝑈) ⊆ 𝑈)) | ||
Theorem | mrcidm 16882 | The closure operation is idempotent. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋) → (𝐹‘(𝐹‘𝑈)) = (𝐹‘𝑈)) | ||
Theorem | mrcsscl 16883 | The closure is the minimal closed set; any closed set which contains the generators is a superset of the closure. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑉 ∧ 𝑉 ∈ 𝐶) → (𝐹‘𝑈) ⊆ 𝑉) | ||
Theorem | mrcuni 16884 | Idempotence of closure under a general union. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝒫 𝑋) → (𝐹‘∪ 𝑈) = (𝐹‘∪ (𝐹 “ 𝑈))) | ||
Theorem | mrcun 16885 | Idempotence of closure under a pair union. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋 ∧ 𝑉 ⊆ 𝑋) → (𝐹‘(𝑈 ∪ 𝑉)) = (𝐹‘((𝐹‘𝑈) ∪ (𝐹‘𝑉)))) | ||
Theorem | mrcssvd 16886 | The Moore closure of a set is a subset of the base. Deduction form of mrcssv 16877. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) ⇒ ⊢ (𝜑 → (𝑁‘𝐵) ⊆ 𝑋) | ||
Theorem | mrcssd 16887 | Moore closure preserves subset ordering. Deduction form of mrcss 16879. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ (𝜑 → 𝑈 ⊆ 𝑉) & ⊢ (𝜑 → 𝑉 ⊆ 𝑋) ⇒ ⊢ (𝜑 → (𝑁‘𝑈) ⊆ (𝑁‘𝑉)) | ||
Theorem | mrcssidd 16888 | A set is contained in its Moore closure. Deduction form of mrcssid 16880. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ (𝜑 → 𝑈 ⊆ 𝑋) ⇒ ⊢ (𝜑 → 𝑈 ⊆ (𝑁‘𝑈)) | ||
Theorem | mrcidmd 16889 | Moore closure is idempotent. Deduction form of mrcidm 16882. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ (𝜑 → 𝑈 ⊆ 𝑋) ⇒ ⊢ (𝜑 → (𝑁‘(𝑁‘𝑈)) = (𝑁‘𝑈)) | ||
Theorem | mressmrcd 16890 | In a Moore system, if a set is between another set and its closure, the two sets have the same closure. Deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ (𝜑 → 𝑆 ⊆ (𝑁‘𝑇)) & ⊢ (𝜑 → 𝑇 ⊆ 𝑆) ⇒ ⊢ (𝜑 → (𝑁‘𝑆) = (𝑁‘𝑇)) | ||
Theorem | submrc 16891 | In a closure system which is cut off above some level, closures below that level act as normal. (Contributed by Stefan O'Rear, 9-Mar-2015.) |
⊢ 𝐹 = (mrCls‘𝐶) & ⊢ 𝐺 = (mrCls‘(𝐶 ∩ 𝒫 𝐷)) ⇒ ⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝐷 ∈ 𝐶 ∧ 𝑈 ⊆ 𝐷) → (𝐺‘𝑈) = (𝐹‘𝑈)) | ||
Theorem | mrieqvlemd 16892 | In a Moore system, if 𝑌 is a member of 𝑆, (𝑆 ∖ {𝑌}) and 𝑆 have the same closure if and only if 𝑌 is in the closure of (𝑆 ∖ {𝑌}). Used in the proof of mrieqvd 16901 and mrieqv2d 16902. Deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ 𝑁 = (mrCls‘𝐴) & ⊢ (𝜑 → 𝑆 ⊆ 𝑋) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑌 ∈ (𝑁‘(𝑆 ∖ {𝑌})) ↔ (𝑁‘(𝑆 ∖ {𝑌})) = (𝑁‘𝑆))) | ||
Theorem | mrisval 16893* | Value of the set of independent sets of a Moore system. (Contributed by David Moews, 1-May-2017.) |
⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) ⇒ ⊢ (𝐴 ∈ (Moore‘𝑋) → 𝐼 = {𝑠 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑠 ¬ 𝑥 ∈ (𝑁‘(𝑠 ∖ {𝑥}))}) | ||
Theorem | ismri 16894* | Criterion for a set to be an independent set of a Moore system. (Contributed by David Moews, 1-May-2017.) |
⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) ⇒ ⊢ (𝐴 ∈ (Moore‘𝑋) → (𝑆 ∈ 𝐼 ↔ (𝑆 ⊆ 𝑋 ∧ ∀𝑥 ∈ 𝑆 ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥}))))) | ||
Theorem | ismri2 16895* | Criterion for a subset of the base set in a Moore system to be independent. (Contributed by David Moews, 1-May-2017.) |
⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) ⇒ ⊢ ((𝐴 ∈ (Moore‘𝑋) ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ 𝐼 ↔ ∀𝑥 ∈ 𝑆 ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥})))) | ||
Theorem | ismri2d 16896* | Criterion for a subset of the base set in a Moore system to be independent. Deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ (𝜑 → 𝑆 ⊆ 𝑋) ⇒ ⊢ (𝜑 → (𝑆 ∈ 𝐼 ↔ ∀𝑥 ∈ 𝑆 ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥})))) | ||
Theorem | ismri2dd 16897* | Definition of independence of a subset of the base set in a Moore system. One-way deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ (𝜑 → 𝑆 ⊆ 𝑋) & ⊢ (𝜑 → ∀𝑥 ∈ 𝑆 ¬ 𝑥 ∈ (𝑁‘(𝑆 ∖ {𝑥}))) ⇒ ⊢ (𝜑 → 𝑆 ∈ 𝐼) | ||
Theorem | mriss 16898 | An independent set of a Moore system is a subset of the base set. (Contributed by David Moews, 1-May-2017.) |
⊢ 𝐼 = (mrInd‘𝐴) ⇒ ⊢ ((𝐴 ∈ (Moore‘𝑋) ∧ 𝑆 ∈ 𝐼) → 𝑆 ⊆ 𝑋) | ||
Theorem | mrissd 16899 | An independent set of a Moore system is a subset of the base set. Deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ (𝜑 → 𝑆 ∈ 𝐼) ⇒ ⊢ (𝜑 → 𝑆 ⊆ 𝑋) | ||
Theorem | ismri2dad 16900 | Consequence of a set in a Moore system being independent. Deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ 𝑁 = (mrCls‘𝐴) & ⊢ 𝐼 = (mrInd‘𝐴) & ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋)) & ⊢ (𝜑 → 𝑆 ∈ 𝐼) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) ⇒ ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑁‘(𝑆 ∖ {𝑌}))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |