Home | Metamath
Proof Explorer Theorem List (p. 399 of 450) | < 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: | Metamath Proof Explorer
(1-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44926) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | algsca 39801 | The set of scalars of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝐴 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), × 〉} ∪ {〈(Scalar‘ndx), 𝑆〉, 〈( ·𝑠 ‘ndx), · 〉}) ⇒ ⊢ (𝑆 ∈ 𝑉 → 𝑆 = (Scalar‘𝐴)) | ||
Theorem | algvsca 39802 | The scalar product operation of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝐴 = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), × 〉} ∪ {〈(Scalar‘ndx), 𝑆〉, 〈( ·𝑠 ‘ndx), · 〉}) ⇒ ⊢ ( · ∈ 𝑉 → · = ( ·𝑠 ‘𝐴)) | ||
Theorem | mendval 39803* | Value of the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
⊢ 𝐵 = (𝑀 LMHom 𝑀) & ⊢ + = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f (+g‘𝑀)𝑦)) & ⊢ × = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦)) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ · = (𝑥 ∈ (Base‘𝑆), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘f ( ·𝑠 ‘𝑀)𝑦)) ⇒ ⊢ (𝑀 ∈ 𝑋 → (MEndo‘𝑀) = ({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), × 〉} ∪ {〈(Scalar‘ndx), 𝑆〉, 〈( ·𝑠 ‘ndx), · 〉})) | ||
Theorem | mendbas 39804 | Base set of the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
⊢ 𝐴 = (MEndo‘𝑀) ⇒ ⊢ (𝑀 LMHom 𝑀) = (Base‘𝐴) | ||
Theorem | mendplusgfval 39805* | Addition in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) (Proof shortened by AV, 3-Mar-2024.) |
⊢ 𝐴 = (MEndo‘𝑀) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ + = (+g‘𝑀) ⇒ ⊢ (+g‘𝐴) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f + 𝑦)) | ||
Theorem | mendplusg 39806 | A specific addition in the module endomorphism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.) |
⊢ 𝐴 = (MEndo‘𝑀) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ + = (+g‘𝑀) & ⊢ ✚ = (+g‘𝐴) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ✚ 𝑌) = (𝑋 ∘f + 𝑌)) | ||
Theorem | mendmulrfval 39807* | Multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) (Proof shortened by AV, 3-Mar-2024.) |
⊢ 𝐴 = (MEndo‘𝑀) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ (.r‘𝐴) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦)) | ||
Theorem | mendmulr 39808 | A specific multiplication in the module endormoprhism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.) |
⊢ 𝐴 = (MEndo‘𝑀) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ · = (.r‘𝐴) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) = (𝑋 ∘ 𝑌)) | ||
Theorem | mendsca 39809 | The module endomorphism algebra has the same scalars as the underlying module. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
⊢ 𝐴 = (MEndo‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) ⇒ ⊢ 𝑆 = (Scalar‘𝐴) | ||
Theorem | mendvscafval 39810* | Scalar multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) (Proof shortened by AV, 3-Mar-2024.) |
⊢ 𝐴 = (MEndo‘𝑀) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐸 = (Base‘𝑀) ⇒ ⊢ ( ·𝑠 ‘𝐴) = (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘f · 𝑦)) | ||
Theorem | mendvsca 39811 | A specific scalar multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.) |
⊢ 𝐴 = (MEndo‘𝑀) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝐸 = (Base‘𝑀) & ⊢ ∙ = ( ·𝑠 ‘𝐴) ⇒ ⊢ ((𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∙ 𝑌) = ((𝐸 × {𝑋}) ∘f · 𝑌)) | ||
Theorem | mendring 39812 | The module endomorphism algebra is a ring. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐴 = (MEndo‘𝑀) ⇒ ⊢ (𝑀 ∈ LMod → 𝐴 ∈ Ring) | ||
Theorem | mendlmod 39813 | The module endomorphism algebra is a left module. (Contributed by Mario Carneiro, 22-Sep-2015.) |
⊢ 𝐴 = (MEndo‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝐴 ∈ LMod) | ||
Theorem | mendassa 39814 | The module endomorphism algebra is an algebra. (Contributed by Mario Carneiro, 22-Sep-2015.) |
⊢ 𝐴 = (MEndo‘𝑀) & ⊢ 𝑆 = (Scalar‘𝑀) ⇒ ⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝐴 ∈ AssAlg) | ||
Theorem | idomrootle 39815* | No element of an integral domain can have more than 𝑁 𝑁-th roots. (Contributed by Stefan O'Rear, 11-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ ↑ = (.g‘(mulGrp‘𝑅)) ⇒ ⊢ ((𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ) → (♯‘{𝑦 ∈ 𝐵 ∣ (𝑁 ↑ 𝑦) = 𝑋}) ≤ 𝑁) | ||
Theorem | idomodle 39816* | Limit on the number of 𝑁-th roots of unity in an integral domain. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
⊢ 𝐺 = ((mulGrp‘𝑅) ↾s (Unit‘𝑅)) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) ⇒ ⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → (♯‘{𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁}) ≤ 𝑁) | ||
Theorem | fiuneneq 39817 | Two finite sets of equal size have a union of the same size iff they were equal. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐴 ∈ Fin) → ((𝐴 ∪ 𝐵) ≈ 𝐴 ↔ 𝐴 = 𝐵)) | ||
Theorem | idomsubgmo 39818* | The units of an integral domain have at most one subgroup of any single finite cardinality. (Contributed by Stefan O'Rear, 12-Sep-2015.) (Revised by NM, 17-Jun-2017.) |
⊢ 𝐺 = ((mulGrp‘𝑅) ↾s (Unit‘𝑅)) ⇒ ⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) → ∃*𝑦 ∈ (SubGrp‘𝐺)(♯‘𝑦) = 𝑁) | ||
Theorem | proot1mul 39819 | Any primitive 𝑁-th root of unity is a multiple of any other. (Contributed by Stefan O'Rear, 2-Nov-2015.) |
⊢ 𝐺 = ((mulGrp‘𝑅) ↾s (Unit‘𝑅)) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) ⇒ ⊢ (((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ) ∧ (𝑋 ∈ (◡𝑂 “ {𝑁}) ∧ 𝑌 ∈ (◡𝑂 “ {𝑁}))) → 𝑋 ∈ (𝐾‘{𝑌})) | ||
Theorem | proot1hash 39820 | If an integral domain has a primitive 𝑁-th root of unity, it has exactly (ϕ‘𝑁) of them. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
⊢ 𝐺 = ((mulGrp‘𝑅) ↾s (Unit‘𝑅)) & ⊢ 𝑂 = (od‘𝐺) ⇒ ⊢ ((𝑅 ∈ IDomn ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ (◡𝑂 “ {𝑁})) → (♯‘(◡𝑂 “ {𝑁})) = (ϕ‘𝑁)) | ||
Theorem | proot1ex 39821 | The complex field has primitive 𝑁-th roots of unity for all 𝑁. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
⊢ 𝐺 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})) & ⊢ 𝑂 = (od‘𝐺) ⇒ ⊢ (𝑁 ∈ ℕ → (-1↑𝑐(2 / 𝑁)) ∈ (◡𝑂 “ {𝑁})) | ||
Syntax | ccytp 39822 | Syntax for the sequence of cyclotomic polynomials. |
class CytP | ||
Definition | df-cytp 39823* | The Nth cyclotomic polynomial is the polynomial which has as its zeros precisely the primitive Nth roots of unity. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ CytP = (𝑛 ∈ ℕ ↦ ((mulGrp‘(Poly1‘ℂfld)) Σg (𝑟 ∈ (◡(od‘((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))) “ {𝑛}) ↦ ((var1‘ℂfld)(-g‘(Poly1‘ℂfld))((algSc‘(Poly1‘ℂfld))‘𝑟))))) | ||
Theorem | isdomn3 39824 | Nonzero elements form a multiplicative submonoid of any domain. (Contributed by Stefan O'Rear, 11-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑈 = (mulGrp‘𝑅) ⇒ ⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ Ring ∧ (𝐵 ∖ { 0 }) ∈ (SubMnd‘𝑈))) | ||
Theorem | mon1pid 39825 | Monicity and degree of the unit polynomial. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 1 = (1r‘𝑃) & ⊢ 𝑀 = (Monic1p‘𝑅) & ⊢ 𝐷 = ( deg1 ‘𝑅) ⇒ ⊢ (𝑅 ∈ NzRing → ( 1 ∈ 𝑀 ∧ (𝐷‘ 1 ) = 0)) | ||
Theorem | mon1psubm 39826 | Monic polynomials are a multiplicative submonoid. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑀 = (Monic1p‘𝑅) & ⊢ 𝑈 = (mulGrp‘𝑃) ⇒ ⊢ (𝑅 ∈ NzRing → 𝑀 ∈ (SubMnd‘𝑈)) | ||
Theorem | deg1mhm 39827 | Homomorphic property of the polynomial degree. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝐵 = (Base‘𝑃) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝑌 = ((mulGrp‘𝑃) ↾s (𝐵 ∖ { 0 })) & ⊢ 𝑁 = (ℂfld ↾s ℕ0) ⇒ ⊢ (𝑅 ∈ Domn → (𝐷 ↾ (𝐵 ∖ { 0 })) ∈ (𝑌 MndHom 𝑁)) | ||
Theorem | cytpfn 39828 | Functionality of the cyclotomic polynomial sequence. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ CytP Fn ℕ | ||
Theorem | cytpval 39829* | Substitutions for the Nth cyclotomic polynomial. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝑇 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})) & ⊢ 𝑂 = (od‘𝑇) & ⊢ 𝑃 = (Poly1‘ℂfld) & ⊢ 𝑋 = (var1‘ℂfld) & ⊢ 𝑄 = (mulGrp‘𝑃) & ⊢ − = (-g‘𝑃) & ⊢ 𝐴 = (algSc‘𝑃) ⇒ ⊢ (𝑁 ∈ ℕ → (CytP‘𝑁) = (𝑄 Σg (𝑟 ∈ (◡𝑂 “ {𝑁}) ↦ (𝑋 − (𝐴‘𝑟))))) | ||
Theorem | fgraphopab 39830* | Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝐹‘𝑎) = 𝑏)}) | ||
Theorem | fgraphxp 39831* | Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 = {𝑥 ∈ (𝐴 × 𝐵) ∣ (𝐹‘(1st ‘𝑥)) = (2nd ‘𝑥)}) | ||
Theorem | hausgraph 39832 | The graph of a continuous function into a Hausdorff space is closed. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 ∈ (Clsd‘(𝐽 ×t 𝐾))) | ||
Syntax | ctopsep 39833 | The class of separable toplogies. |
class TopSep | ||
Syntax | ctoplnd 39834 | The class of Lindelöf toplogies. |
class TopLnd | ||
Definition | df-topsep 39835* | A topology is separable iff it has a countable dense subset. (Contributed by Stefan O'Rear, 8-Jan-2015.) |
⊢ TopSep = {𝑗 ∈ Top ∣ ∃𝑥 ∈ 𝒫 ∪ 𝑗(𝑥 ≼ ω ∧ ((cls‘𝑗)‘𝑥) = ∪ 𝑗)} | ||
Definition | df-toplnd 39836* | A topology is Lindelöf iff every open cover has a countable subcover. (Contributed by Stefan O'Rear, 8-Jan-2015.) |
⊢ TopLnd = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 = ∪ 𝑦 → ∃𝑧 ∈ 𝒫 𝑥(𝑧 ≼ ω ∧ ∪ 𝑥 = ∪ 𝑧))} | ||
Theorem | iocunico 39837 | Split an open interval into two pieces at point B, Co-author TA. (Contributed by Jon Pennant, 8-Jun-2019.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → ((𝐴(,]𝐵) ∪ (𝐵[,)𝐶)) = (𝐴(,)𝐶)) | ||
Theorem | iocinico 39838 | The intersection of two sets that meet at a point is that point. (Contributed by Jon Pennant, 12-Jun-2019.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 < 𝐶)) → ((𝐴(,]𝐵) ∩ (𝐵[,)𝐶)) = {𝐵}) | ||
Theorem | iocmbl 39839 | An open-below, closed-above real interval is measurable. (Contributed by Jon Pennant, 12-Jun-2019.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ) → (𝐴(,]𝐵) ∈ dom vol) | ||
Theorem | cnioobibld 39840* | A bounded, continuous function on an open bounded interval is integrable. The function must be bounded. For a counterexample, consider 𝐹 = (𝑥 ∈ (0(,)1) ↦ (1 / 𝑥)). See cniccibl 24441 for closed bounded intervals. (Contributed by Jon Pennant, 31-May-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ)) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) ⇒ ⊢ (𝜑 → 𝐹 ∈ 𝐿1) | ||
Theorem | itgpowd 39841* | The integral of a monomial on a closed bounded interval of the real line. Co-authors TA and MC. (Contributed by Jon Pennant, 31-May-2019.) (Revised by Thierry Arnoux, 14-Jun-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → ∫(𝐴[,]𝐵)(𝑥↑𝑁) d𝑥 = (((𝐵↑(𝑁 + 1)) − (𝐴↑(𝑁 + 1))) / (𝑁 + 1))) | ||
Theorem | arearect 39842 | The area of a rectangle whose sides are parallel to the coordinate axes in (ℝ × ℝ) is its width multiplied by its height. (Contributed by Jon Pennant, 19-Mar-2019.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ & ⊢ 𝐷 ∈ ℝ & ⊢ 𝐴 ≤ 𝐵 & ⊢ 𝐶 ≤ 𝐷 & ⊢ 𝑆 = ((𝐴[,]𝐵) × (𝐶[,]𝐷)) ⇒ ⊢ (area‘𝑆) = ((𝐵 − 𝐴) · (𝐷 − 𝐶)) | ||
Theorem | areaquad 39843* | The area of a quadrilateral with two sides which are parallel to the y-axis in (ℝ × ℝ) is its width multiplied by the average height of its higher edge minus the average height of its lower edge. Co-author TA. (Contributed by Jon Pennant, 31-May-2019.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈ ℝ & ⊢ 𝐷 ∈ ℝ & ⊢ 𝐸 ∈ ℝ & ⊢ 𝐹 ∈ ℝ & ⊢ 𝐴 < 𝐵 & ⊢ 𝐶 ≤ 𝐸 & ⊢ 𝐷 ≤ 𝐹 & ⊢ 𝑈 = (𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) & ⊢ 𝑉 = (𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) & ⊢ 𝑆 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))} ⇒ ⊢ (area‘𝑆) = ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵 − 𝐴)) | ||
Theorem | ifpan123g 39844 | Conjunction of conditional logical operators. (Contributed by RP, 18-Apr-2020.) |
⊢ ((if-(𝜑, 𝜒, 𝜏) ∧ if-(𝜓, 𝜃, 𝜂)) ↔ (((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∧ ((¬ 𝜓 ∨ 𝜃) ∧ (𝜓 ∨ 𝜂)))) | ||
Theorem | ifpan23 39845 | Conjunction of conditional logical operators. (Contributed by RP, 20-Apr-2020.) |
⊢ ((if-(𝜑, 𝜓, 𝜒) ∧ if-(𝜑, 𝜃, 𝜏)) ↔ if-(𝜑, (𝜓 ∧ 𝜃), (𝜒 ∧ 𝜏))) | ||
Theorem | ifpdfor2 39846 | Define or in terms of conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 ∨ 𝜓) ↔ if-(𝜑, 𝜑, 𝜓)) | ||
Theorem | ifporcor 39847 | Corollary of commutation of or. (Contributed by RP, 20-Apr-2020.) |
⊢ (if-(𝜑, 𝜑, 𝜓) ↔ if-(𝜓, 𝜓, 𝜑)) | ||
Theorem | ifpdfan2 39848 | Define and with conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
⊢ ((𝜑 ∧ 𝜓) ↔ if-(𝜑, 𝜓, 𝜑)) | ||
Theorem | ifpancor 39849 | Corollary of commutation of and. (Contributed by RP, 25-Apr-2020.) |
⊢ (if-(𝜑, 𝜓, 𝜑) ↔ if-(𝜓, 𝜑, 𝜓)) | ||
Theorem | ifpdfor 39850 | Define or in terms of conditional logic operator and true. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 ∨ 𝜓) ↔ if-(𝜑, ⊤, 𝜓)) | ||
Theorem | ifpdfan 39851 | Define and with conditional logic operator and false. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 ∧ 𝜓) ↔ if-(𝜑, 𝜓, ⊥)) | ||
Theorem | ifpbi2 39852 | Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.) |
⊢ ((𝜑 ↔ 𝜓) → (if-(𝜒, 𝜑, 𝜃) ↔ if-(𝜒, 𝜓, 𝜃))) | ||
Theorem | ifpbi3 39853 | Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.) |
⊢ ((𝜑 ↔ 𝜓) → (if-(𝜒, 𝜃, 𝜑) ↔ if-(𝜒, 𝜃, 𝜓))) | ||
Theorem | ifpim1 39854 | Restate implication as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 → 𝜓) ↔ if-(¬ 𝜑, ⊤, 𝜓)) | ||
Theorem | ifpnot 39855 | Restate negated wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ (¬ 𝜑 ↔ if-(𝜑, ⊥, ⊤)) | ||
Theorem | ifpid2 39856 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ (𝜑 ↔ if-(𝜑, ⊤, ⊥)) | ||
Theorem | ifpim2 39857 | Restate implication as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 → 𝜓) ↔ if-(𝜓, ⊤, ¬ 𝜑)) | ||
Theorem | ifpbi23 39858 | Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.) |
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → (if-(𝜏, 𝜑, 𝜒) ↔ if-(𝜏, 𝜓, 𝜃))) | ||
Theorem | ifpdfbi 39859 | Define biimplication as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 ↔ 𝜓) ↔ if-(𝜑, 𝜓, ¬ 𝜓)) | ||
Theorem | ifpbiidcor 39860 | Restatement of biid 263. (Contributed by RP, 25-Apr-2020.) |
⊢ if-(𝜑, 𝜑, ¬ 𝜑) | ||
Theorem | ifpbicor 39861 | Corollary of commutation of biimplication. (Contributed by RP, 25-Apr-2020.) |
⊢ (if-(𝜑, 𝜓, ¬ 𝜓) ↔ if-(𝜓, 𝜑, ¬ 𝜑)) | ||
Theorem | ifpxorcor 39862 | Corollary of commutation of biimplication. (Contributed by RP, 25-Apr-2020.) |
⊢ (if-(𝜑, ¬ 𝜓, 𝜓) ↔ if-(𝜓, ¬ 𝜑, 𝜑)) | ||
Theorem | ifpbi1 39863 | Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.) |
⊢ ((𝜑 ↔ 𝜓) → (if-(𝜑, 𝜒, 𝜃) ↔ if-(𝜓, 𝜒, 𝜃))) | ||
Theorem | ifpnot23 39864 | Negation of conditional logical operator. (Contributed by RP, 18-Apr-2020.) |
⊢ (¬ if-(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, ¬ 𝜓, ¬ 𝜒)) | ||
Theorem | ifpnotnotb 39865 | Factor conditional logic operator over negation in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
⊢ (if-(𝜑, ¬ 𝜓, ¬ 𝜒) ↔ ¬ if-(𝜑, 𝜓, 𝜒)) | ||
Theorem | ifpnorcor 39866 | Corollary of commutation of nor. (Contributed by RP, 25-Apr-2020.) |
⊢ (if-(𝜑, ¬ 𝜑, ¬ 𝜓) ↔ if-(𝜓, ¬ 𝜓, ¬ 𝜑)) | ||
Theorem | ifpnancor 39867 | Corollary of commutation of and. (Contributed by RP, 25-Apr-2020.) |
⊢ (if-(𝜑, ¬ 𝜓, ¬ 𝜑) ↔ if-(𝜓, ¬ 𝜑, ¬ 𝜓)) | ||
Theorem | ifpnot23b 39868 | Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.) |
⊢ (¬ if-(𝜑, ¬ 𝜓, 𝜒) ↔ if-(𝜑, 𝜓, ¬ 𝜒)) | ||
Theorem | ifpbiidcor2 39869 | Restatement of biid 263. (Contributed by RP, 25-Apr-2020.) |
⊢ ¬ if-(𝜑, ¬ 𝜑, 𝜑) | ||
Theorem | ifpnot23c 39870 | Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.) |
⊢ (¬ if-(𝜑, 𝜓, ¬ 𝜒) ↔ if-(𝜑, ¬ 𝜓, 𝜒)) | ||
Theorem | ifpnot23d 39871 | Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.) |
⊢ (¬ if-(𝜑, ¬ 𝜓, ¬ 𝜒) ↔ if-(𝜑, 𝜓, 𝜒)) | ||
Theorem | ifpdfnan 39872 | Define nand as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 ⊼ 𝜓) ↔ if-(𝜑, ¬ 𝜓, ⊤)) | ||
Theorem | ifpdfxor 39873 | Define xor as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 ⊻ 𝜓) ↔ if-(𝜑, ¬ 𝜓, 𝜓)) | ||
Theorem | ifpbi12 39874 | Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.) |
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → (if-(𝜑, 𝜒, 𝜏) ↔ if-(𝜓, 𝜃, 𝜏))) | ||
Theorem | ifpbi13 39875 | Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.) |
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → (if-(𝜑, 𝜏, 𝜒) ↔ if-(𝜓, 𝜏, 𝜃))) | ||
Theorem | ifpbi123 39876 | Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.) |
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) → (if-(𝜑, 𝜒, 𝜏) ↔ if-(𝜓, 𝜃, 𝜂))) | ||
Theorem | ifpidg 39877 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜃 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ ((((𝜑 ∧ 𝜓) → 𝜃) ∧ ((𝜑 ∧ 𝜃) → 𝜓)) ∧ ((𝜒 → (𝜑 ∨ 𝜃)) ∧ (𝜃 → (𝜑 ∨ 𝜒))))) | ||
Theorem | ifpid3g 39878 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜒 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ (((𝜑 ∧ 𝜓) → 𝜒) ∧ ((𝜑 ∧ 𝜒) → 𝜓))) | ||
Theorem | ifpid2g 39879 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜓 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ ((𝜓 → (𝜑 ∨ 𝜒)) ∧ (𝜒 → (𝜑 ∨ 𝜓)))) | ||
Theorem | ifpid1g 39880 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((𝜑 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ ((𝜒 → 𝜑) ∧ (𝜑 → 𝜓))) | ||
Theorem | ifpim23g 39881 | Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
⊢ (((𝜑 → 𝜓) ↔ if-(𝜒, 𝜓, ¬ 𝜑)) ↔ (((𝜑 ∧ 𝜓) → 𝜒) ∧ (𝜒 → (𝜑 ∨ 𝜓)))) | ||
Theorem | ifpim3 39882 | Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
⊢ ((𝜑 → 𝜓) ↔ if-(𝜑, 𝜓, ¬ 𝜑)) | ||
Theorem | ifpnim1 39883 | Restate negated implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
⊢ (¬ (𝜑 → 𝜓) ↔ if-(𝜑, ¬ 𝜓, 𝜑)) | ||
Theorem | ifpim4 39884 | Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
⊢ ((𝜑 → 𝜓) ↔ if-(𝜓, 𝜓, ¬ 𝜑)) | ||
Theorem | ifpnim2 39885 | Restate negated implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
⊢ (¬ (𝜑 → 𝜓) ↔ if-(𝜓, ¬ 𝜓, 𝜑)) | ||
Theorem | ifpim123g 39886 | Implication of conditional logical operators. The right hand side is basically conjunctive normal form which is useful in proofs. (Contributed by RP, 16-Apr-2020.) |
⊢ ((if-(𝜑, 𝜒, 𝜏) → if-(𝜓, 𝜃, 𝜂)) ↔ ((((𝜑 → ¬ 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜏 → 𝜃))) ∧ (((𝜑 → 𝜓) ∨ (𝜒 → 𝜂)) ∧ ((¬ 𝜓 → 𝜑) ∨ (𝜏 → 𝜂))))) | ||
Theorem | ifpim1g 39887 | Implication of conditional logical operators. (Contributed by RP, 18-Apr-2020.) |
⊢ ((if-(𝜑, 𝜒, 𝜃) → if-(𝜓, 𝜒, 𝜃)) ↔ (((𝜓 → 𝜑) ∨ (𝜃 → 𝜒)) ∧ ((𝜑 → 𝜓) ∨ (𝜒 → 𝜃)))) | ||
Theorem | ifp1bi 39888 | Substitute the first element of conditional logical operator. (Contributed by RP, 20-Apr-2020.) |
⊢ ((if-(𝜑, 𝜒, 𝜃) ↔ if-(𝜓, 𝜒, 𝜃)) ↔ ((((𝜑 → 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜑 → 𝜓) ∨ (𝜃 → 𝜒))) ∧ (((𝜓 → 𝜑) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜃 → 𝜒))))) | ||
Theorem | ifpbi1b 39889 | When the first variable is irrelevant, it can be replaced. (Contributed by RP, 25-Apr-2020.) |
⊢ (if-(𝜑, 𝜒, 𝜒) ↔ if-(𝜓, 𝜒, 𝜒)) | ||
Theorem | ifpimimb 39890 | Factor conditional logic operator over implication in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
⊢ (if-(𝜑, (𝜓 → 𝜒), (𝜃 → 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏))) | ||
Theorem | ifpororb 39891 | Factor conditional logic operator over disjunction in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
⊢ (if-(𝜑, (𝜓 ∨ 𝜒), (𝜃 ∨ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ∨ if-(𝜑, 𝜒, 𝜏))) | ||
Theorem | ifpananb 39892 | Factor conditional logic operator over conjunction in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
⊢ (if-(𝜑, (𝜓 ∧ 𝜒), (𝜃 ∧ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ∧ if-(𝜑, 𝜒, 𝜏))) | ||
Theorem | ifpnannanb 39893 | Factor conditional logic operator over nand in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
⊢ (if-(𝜑, (𝜓 ⊼ 𝜒), (𝜃 ⊼ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ⊼ if-(𝜑, 𝜒, 𝜏))) | ||
Theorem | ifpor123g 39894 | Disjunction of conditional logical operators. (Contributed by RP, 18-Apr-2020.) |
⊢ ((if-(𝜑, 𝜒, 𝜏) ∨ if-(𝜓, 𝜃, 𝜂)) ↔ ((((𝜑 → ¬ 𝜓) ∨ (𝜒 ∨ 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜏 ∨ 𝜃))) ∧ (((𝜑 → 𝜓) ∨ (𝜒 ∨ 𝜂)) ∧ ((¬ 𝜓 → 𝜑) ∨ (𝜏 ∨ 𝜂))))) | ||
Theorem | ifpimim 39895 | Consequnce of implication. (Contributed by RP, 17-Apr-2020.) |
⊢ (if-(𝜑, (𝜓 → 𝜒), (𝜃 → 𝜏)) → (if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏))) | ||
Theorem | ifpbibib 39896 | Factor conditional logic operator over biimplication in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
⊢ (if-(𝜑, (𝜓 ↔ 𝜒), (𝜃 ↔ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ↔ if-(𝜑, 𝜒, 𝜏))) | ||
Theorem | ifpxorxorb 39897 | Factor conditional logic operator over xor in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
⊢ (if-(𝜑, (𝜓 ⊻ 𝜒), (𝜃 ⊻ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ⊻ if-(𝜑, 𝜒, 𝜏))) | ||
Theorem | rp-fakeimass 39898 | A special case where implication appears to conform to a mixed associative law. (Contributed by RP, 29-Feb-2020.) |
⊢ ((𝜑 ∨ 𝜒) ↔ (((𝜑 → 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒)))) | ||
Theorem | rp-fakeanorass 39899 | A special case where a mixture of and and or appears to conform to a mixed associative law. (Contributed by RP, 26-Feb-2020.) |
⊢ ((𝜒 → 𝜑) ↔ (((𝜑 ∧ 𝜓) ∨ 𝜒) ↔ (𝜑 ∧ (𝜓 ∨ 𝜒)))) | ||
Theorem | rp-fakeoranass 39900 | A special case where a mixture of or and and appears to conform to a mixed associative law. (Contributed by RP, 29-Feb-2020.) |
⊢ ((𝜑 → 𝜒) ↔ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜑 ∨ (𝜓 ∧ 𝜒)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |