![]() |
Metamath
Proof Explorer Theorem List (p. 381 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 | cdlemg29 38001* | Eliminate (𝐹‘𝑃) ≠ 𝑃 and (𝐺‘𝑃) ≠ 𝑃 from cdlemg28 38000. TODO: would it be better to do this later? (Contributed by NM, 29-May-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝑁 = ((𝑃 ∨ 𝑣) ∧ (𝑄 ∨ (𝑅‘𝐹))) & ⊢ 𝑂 = ((𝑃 ∨ 𝑣) ∧ (𝑄 ∨ (𝑅‘𝐺))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) ∧ ((𝑧 ≠ 𝑁 ∧ 𝑧 ≠ 𝑂) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑣 ≠ (𝑅‘𝐺)))) → ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ 𝑊) = ((𝑄 ∨ (𝐹‘(𝐺‘𝑄))) ∧ 𝑊)) | ||
Theorem | cdlemg33a 38002* | TODO: Fix comment. (Contributed by NM, 29-May-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝑁 = ((𝑃 ∨ 𝑣) ∧ (𝑄 ∨ (𝑅‘𝐹))) & ⊢ 𝑂 = ((𝑃 ∨ 𝑣) ∧ (𝑄 ∨ (𝑅‘𝐺))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ 𝑂 ∈ 𝐴) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑁 ≠ 𝑂) ∧ 𝑣 ≠ (𝑅‘𝐹) ∧ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑧 ≠ 𝑁 ∧ 𝑧 ≠ 𝑂 ∧ 𝑧 ≤ (𝑃 ∨ 𝑣)))) | ||
Theorem | cdlemg33b 38003* | TODO: Fix comment. (Contributed by NM, 30-May-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝑁 = ((𝑃 ∨ 𝑣) ∧ (𝑄 ∨ (𝑅‘𝐹))) & ⊢ 𝑂 = ((𝑃 ∨ 𝑣) ∧ (𝑄 ∨ (𝑅‘𝐺))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ 𝑂 ∈ 𝐴) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑣 ≠ (𝑅‘𝐹) ∧ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑧 ≠ 𝑁 ∧ 𝑧 ≠ 𝑂 ∧ 𝑧 ≤ (𝑃 ∨ 𝑣)))) | ||
Theorem | cdlemg33c 38004* | TODO: Fix comment. (Contributed by NM, 30-May-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝑁 = ((𝑃 ∨ 𝑣) ∧ (𝑄 ∨ (𝑅‘𝐹))) & ⊢ 𝑂 = ((𝑃 ∨ 𝑣) ∧ (𝑄 ∨ (𝑅‘𝐺))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ 𝑂 = (0.‘𝐾)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑣 ≠ (𝑅‘𝐹) ∧ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑧 ≠ 𝑁 ∧ 𝑧 ≠ 𝑂 ∧ 𝑧 ≤ (𝑃 ∨ 𝑣)))) | ||
Theorem | cdlemg33d 38005* | TODO: Fix comment. (Contributed by NM, 30-May-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝑁 = ((𝑃 ∨ 𝑣) ∧ (𝑄 ∨ (𝑅‘𝐹))) & ⊢ 𝑂 = ((𝑃 ∨ 𝑣) ∧ (𝑄 ∨ (𝑅‘𝐺))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝑁 = (0.‘𝐾) ∧ 𝑂 ∈ 𝐴) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑣 ≠ (𝑅‘𝐺) ∧ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑧 ≠ 𝑁 ∧ 𝑧 ≠ 𝑂 ∧ 𝑧 ≤ (𝑃 ∨ 𝑣)))) | ||
Theorem | cdlemg33e 38006* | TODO: Fix comment. (Contributed by NM, 30-May-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝑁 = ((𝑃 ∨ 𝑣) ∧ (𝑄 ∨ (𝑅‘𝐹))) & ⊢ 𝑂 = ((𝑃 ∨ 𝑣) ∧ (𝑄 ∨ (𝑅‘𝐺))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝑁 = (0.‘𝐾) ∧ 𝑂 = (0.‘𝐾)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑣 ≠ (𝑅‘𝐹) ∧ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑧 ≠ 𝑁 ∧ 𝑧 ≠ 𝑂 ∧ 𝑧 ≤ (𝑃 ∨ 𝑣)))) | ||
Theorem | cdlemg33 38007* | Combine cdlemg33b 38003, cdlemg33c 38004, cdlemg33d 38005, cdlemg33e 38006. TODO: Fix comment. (Contributed by NM, 30-May-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝑁 = ((𝑃 ∨ 𝑣) ∧ (𝑄 ∨ (𝑅‘𝐹))) & ⊢ 𝑂 = ((𝑃 ∨ 𝑣) ∧ (𝑄 ∨ (𝑅‘𝐺))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑃 ≠ 𝑄) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑣 ≠ (𝑅‘𝐺) ∧ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑧 ≠ 𝑁 ∧ 𝑧 ≠ 𝑂 ∧ 𝑧 ≤ (𝑃 ∨ 𝑣)))) | ||
Theorem | cdlemg34 38008* | Use cdlemg33 to eliminate 𝑧 from cdlemg29 38001. TODO: Fix comment. (Contributed by NM, 31-May-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝑁 = ((𝑃 ∨ 𝑣) ∧ (𝑄 ∨ (𝑅‘𝐹))) & ⊢ 𝑂 = ((𝑃 ∨ 𝑣) ∧ (𝑄 ∨ (𝑅‘𝐺))) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑃 ≠ 𝑄) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑣 ≠ (𝑅‘𝐺) ∧ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ 𝑊) = ((𝑄 ∨ (𝐹‘(𝐺‘𝑄))) ∧ 𝑊)) | ||
Theorem | cdlemg35 38009* | TODO: Fix comment. TODO: should we have a more general version of hlsupr 36682 to avoid the ≠ conditions? (Contributed by NM, 31-May-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝐹‘𝑃) ≠ 𝑃 ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ∃𝑣 ∈ 𝐴 (𝑣 ≤ 𝑊 ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑣 ≠ (𝑅‘𝐺)))) | ||
Theorem | cdlemg36 38010* | Use cdlemg35 to eliminate 𝑣 from cdlemg34 38008. TODO: Fix comment. (Contributed by NM, 31-May-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘𝑃) ≠ 𝑃 ∧ (𝐺‘𝑃) ≠ 𝑃) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ 𝑊) = ((𝑄 ∨ (𝐹‘(𝐺‘𝑄))) ∧ 𝑊)) | ||
Theorem | cdlemg38 38011 | Use cdlemg37 37985 to eliminate ∃𝑟 ∈ 𝐴 from cdlemg36 38010. TODO: Fix comment. (Contributed by NM, 31-May-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘𝑃) ≠ 𝑃 ∧ (𝐺‘𝑃) ≠ 𝑃) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ 𝑊) = ((𝑄 ∨ (𝐹‘(𝐺‘𝑄))) ∧ 𝑊)) | ||
Theorem | cdlemg39 38012 | Eliminate ≠ conditions from cdlemg38 38011. TODO: Would this better be done at cdlemg35 38009? TODO: Fix comment. (Contributed by NM, 31-May-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄)) → ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ 𝑊) = ((𝑄 ∨ (𝐹‘(𝐺‘𝑄))) ∧ 𝑊)) | ||
Theorem | cdlemg40 38013 | Eliminate 𝑃 ≠ 𝑄 conditions from cdlemg39 38012. TODO: Fix comment. (Contributed by NM, 31-May-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) → ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ 𝑊) = ((𝑄 ∨ (𝐹‘(𝐺‘𝑄))) ∧ 𝑊)) | ||
Theorem | cdlemg41 38014 | Convert cdlemg40 38013 to function composition. TODO: Fix comment. (Contributed by NM, 31-May-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) → ((𝑃 ∨ ((𝐹 ∘ 𝐺)‘𝑃)) ∧ 𝑊) = ((𝑄 ∨ ((𝐹 ∘ 𝐺)‘𝑄)) ∧ 𝑊)) | ||
Theorem | ltrnco 38015 | The composition of two translations is a translation. Part of proof of Lemma G of [Crawley] p. 116, line 15 on p. 117. (Contributed by NM, 31-May-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝐹 ∘ 𝐺) ∈ 𝑇) | ||
Theorem | trlcocnv 38016 | Swap the arguments of the trace of a composition with converse. (Contributed by NM, 1-Jul-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝑅‘(𝐹 ∘ ◡𝐺)) = (𝑅‘(𝐺 ∘ ◡𝐹))) | ||
Theorem | trlcoabs 38017 | Absorption into a composition by joining with trace. (Contributed by NM, 22-Jul-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝐹 ∘ 𝐺)‘𝑃) ∨ (𝑅‘𝐹)) = ((𝐺‘𝑃) ∨ (𝑅‘𝐹))) | ||
Theorem | trlcoabs2N 38018 | Absorption of the trace of a composition. (Contributed by NM, 29-Jul-2013.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐹))) = ((𝐹‘𝑃) ∨ (𝐺‘𝑃))) | ||
Theorem | trlcoat 38019 | The trace of a composition of two translations is an atom if their traces are different. (Contributed by NM, 15-Jun-2013.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺)) → (𝑅‘(𝐹 ∘ 𝐺)) ∈ 𝐴) | ||
Theorem | trlcocnvat 38020 | Commonly used special case of trlcoat 38019. (Contributed by NM, 1-Jul-2013.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺)) → (𝑅‘(𝐹 ∘ ◡𝐺)) ∈ 𝐴) | ||
Theorem | trlconid 38021 | The composition of two different translations is not the identity translation. (Contributed by NM, 22-Jul-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺)) → (𝐹 ∘ 𝐺) ≠ ( I ↾ 𝐵)) | ||
Theorem | trlcolem 38022 | Lemma for trlco 38023. (Contributed by NM, 1-Jun-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘(𝐹 ∘ 𝐺)) ≤ ((𝑅‘𝐹) ∨ (𝑅‘𝐺))) | ||
Theorem | trlco 38023 | The trace of a composition of translations is less than or equal to the join of their traces. Part of proof of Lemma G of [Crawley] p. 116, second paragraph on p. 117. (Contributed by NM, 2-Jun-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝑅‘(𝐹 ∘ 𝐺)) ≤ ((𝑅‘𝐹) ∨ (𝑅‘𝐺))) | ||
Theorem | trlcone 38024 | If two translations have different traces, the trace of their composition is also different. (Contributed by NM, 14-Jun-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝐺) ∧ 𝐺 ≠ ( I ↾ 𝐵))) → (𝑅‘𝐹) ≠ (𝑅‘(𝐹 ∘ 𝐺))) | ||
Theorem | cdlemg42 38025 | Part of proof of Lemma G of [Crawley] p. 116, first line of third paragraph on p. 117. (Contributed by NM, 3-Jun-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ¬ (𝐺‘𝑃) ≤ (𝑃 ∨ (𝐹‘𝑃))) | ||
Theorem | cdlemg43 38026 | Part of proof of Lemma G of [Crawley] p. 116, third line of third paragraph on p. 117. (Contributed by NM, 3-Jun-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝐹‘(𝐺‘𝑃)) = (((𝐺‘𝑃) ∨ (𝑅‘𝐹)) ∧ ((𝐹‘𝑃) ∨ (𝑅‘𝐺)))) | ||
Theorem | cdlemg44a 38027 | Part of proof of Lemma G of [Crawley] p. 116, fourth line of third paragraph on p. 117: "so fg(p) = gf(p)." (Contributed by NM, 3-Jun-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ ((𝐹‘𝑃) ≠ 𝑃 ∧ (𝐺‘𝑃) ≠ 𝑃 ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝐹‘(𝐺‘𝑃)) = (𝐺‘(𝐹‘𝑃))) | ||
Theorem | cdlemg44b 38028 | Eliminate (𝐹‘𝑃) ≠ 𝑃, (𝐺‘𝑃) ≠ 𝑃 from cdlemg44a 38027. (Contributed by NM, 3-Jun-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺)) → (𝐹‘(𝐺‘𝑃)) = (𝐺‘(𝐹‘𝑃))) | ||
Theorem | cdlemg44 38029 | Part of proof of Lemma G of [Crawley] p. 116, fifth line of third paragraph on p. 117: "and hence fg = gf." (Contributed by NM, 3-Jun-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺)) → (𝐹 ∘ 𝐺) = (𝐺 ∘ 𝐹)) | ||
Theorem | cdlemg47a 38030 | TODO: fix comment. TODO: Use this above in place of (𝐹‘𝑃) = 𝑃 antecedents? (Contributed by NM, 5-Jun-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝐹 = ( I ↾ 𝐵)) → (𝐹 ∘ 𝐺) = (𝐺 ∘ 𝐹)) | ||
Theorem | cdlemg46 38031* | Part of proof of Lemma G of [Crawley] p. 116, seventh line of third paragraph on p. 117: "hf and f have different traces." (Contributed by NM, 5-Jun-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ ℎ ∈ 𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ℎ ≠ ( I ↾ 𝐵) ∧ (𝑅‘ℎ) ≠ (𝑅‘𝐹))) → (𝑅‘(ℎ ∘ 𝐹)) ≠ (𝑅‘𝐹)) | ||
Theorem | cdlemg47 38032* | Part of proof of Lemma G of [Crawley] p. 116, ninth line of third paragraph on p. 117: "we conclude that gf = fg." (Contributed by NM, 5-Jun-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (ℎ ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝐺)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ℎ ≠ ( I ↾ 𝐵) ∧ (𝑅‘ℎ) ≠ (𝑅‘𝐹))) → (𝐹 ∘ 𝐺) = (𝐺 ∘ 𝐹)) | ||
Theorem | cdlemg48 38033 | Eliminate ℎ from cdlemg47 38032. (Contributed by NM, 5-Jun-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) = (𝑅‘𝐺))) → (𝐹 ∘ 𝐺) = (𝐺 ∘ 𝐹)) | ||
Theorem | ltrncom 38034 | Composition is commutative for translations. Part of proof of Lemma G of [Crawley] p. 116. (Contributed by NM, 5-Jun-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝐹 ∘ 𝐺) = (𝐺 ∘ 𝐹)) | ||
Theorem | ltrnco4 38035 | Rearrange a composition of 4 translations, analogous to an4 655. (Contributed by NM, 10-Jun-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐸 ∈ 𝑇 ∧ 𝐹 ∈ 𝑇) → ((𝐷 ∘ 𝐸) ∘ (𝐹 ∘ 𝐺)) = ((𝐷 ∘ 𝐹) ∘ (𝐸 ∘ 𝐺))) | ||
Theorem | trljco 38036 | Trace joined with trace of composition. (Contributed by NM, 15-Jun-2013.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → ((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺))) = ((𝑅‘𝐹) ∨ (𝑅‘𝐺))) | ||
Theorem | trljco2 38037 | Trace joined with trace of composition. (Contributed by NM, 16-Jun-2013.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → ((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺))) = ((𝑅‘𝐺) ∨ (𝑅‘(𝐹 ∘ 𝐺)))) | ||
Syntax | ctgrp 38038 | Extend class notation with translation group. |
class TGrp | ||
Definition | df-tgrp 38039* | Define the class of all translation groups. 𝑘 is normally a member of HL. Each base set is the set of all lattice translations with respect to a hyperplane 𝑤, and the operation is function composition. Similar to definition of G in [Crawley] p. 116, third paragraph (which defines this for geomodular lattices). (Contributed by NM, 5-Jun-2013.) |
⊢ TGrp = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {〈(Base‘ndx), ((LTrn‘𝑘)‘𝑤)〉, 〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉})) | ||
Theorem | tgrpfset 38040* | The translation group maps for a lattice 𝐾. (Contributed by NM, 5-Jun-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑉 → (TGrp‘𝐾) = (𝑤 ∈ 𝐻 ↦ {〈(Base‘ndx), ((LTrn‘𝐾)‘𝑤)〉, 〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉})) | ||
Theorem | tgrpset 38041* | The translation group for a fiducial co-atom 𝑊. (Contributed by NM, 5-Jun-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐺 = ((TGrp‘𝐾)‘𝑊) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝐺 = {〈(Base‘ndx), 𝑇〉, 〈(+g‘ndx), (𝑓 ∈ 𝑇, 𝑔 ∈ 𝑇 ↦ (𝑓 ∘ 𝑔))〉}) | ||
Theorem | tgrpbase 38042 | The base set of the translation group is the set of all translations (for a fiducial co-atom 𝑊). (Contributed by NM, 5-Jun-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐺 = ((TGrp‘𝐾)‘𝑊) & ⊢ 𝐶 = (Base‘𝐺) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝐶 = 𝑇) | ||
Theorem | tgrpopr 38043* | The group operation of the translation group is function composition. (Contributed by NM, 5-Jun-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐺 = ((TGrp‘𝐾)‘𝑊) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → + = (𝑓 ∈ 𝑇, 𝑔 ∈ 𝑇 ↦ (𝑓 ∘ 𝑔))) | ||
Theorem | tgrpov 38044 | The group operation value of the translation group is the composition of translations. (Contributed by NM, 5-Jun-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐺 = ((TGrp‘𝐾)‘𝑊) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ∧ (𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝑇)) → (𝑋 + 𝑌) = (𝑋 ∘ 𝑌)) | ||
Theorem | tgrpgrplem 38045 | Lemma for tgrpgrp 38046. (Contributed by NM, 6-Jun-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐺 = ((TGrp‘𝐾)‘𝑊) & ⊢ + = (+g‘𝐺) & ⊢ 𝐵 = (Base‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐺 ∈ Grp) | ||
Theorem | tgrpgrp 38046 | The translation group is a group. (Contributed by NM, 6-Jun-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐺 = ((TGrp‘𝐾)‘𝑊) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐺 ∈ Grp) | ||
Theorem | tgrpabl 38047 | The translation group is an Abelian group. Lemma G of [Crawley] p. 116. (Contributed by NM, 6-Jun-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐺 = ((TGrp‘𝐾)‘𝑊) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐺 ∈ Abel) | ||
Syntax | ctendo 38048 | Extend class notation with translation group endomorphisms. |
class TEndo | ||
Syntax | cedring 38049 | Extend class notation with division ring on trace-preserving endomorphisms. |
class EDRing | ||
Syntax | cedring-rN 38050 | Extend class notation with division ring on trace-preserving endomorphisms, with multiplication reversed. TODO: remove EDRingR theorems if not used. |
class EDRingR | ||
Definition | df-tendo 38051* | Define trace-preserving endomorphisms on the set of translations. (Contributed by NM, 8-Jun-2013.) |
⊢ TEndo = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {𝑓 ∣ (𝑓:((LTrn‘𝑘)‘𝑤)⟶((LTrn‘𝑘)‘𝑤) ∧ ∀𝑥 ∈ ((LTrn‘𝑘)‘𝑤)∀𝑦 ∈ ((LTrn‘𝑘)‘𝑤)(𝑓‘(𝑥 ∘ 𝑦)) = ((𝑓‘𝑥) ∘ (𝑓‘𝑦)) ∧ ∀𝑥 ∈ ((LTrn‘𝑘)‘𝑤)(((trL‘𝑘)‘𝑤)‘(𝑓‘𝑥))(le‘𝑘)(((trL‘𝑘)‘𝑤)‘𝑥))})) | ||
Definition | df-edring-rN 38052* | Define division ring on trace-preserving endomorphisms. Definition of E of [Crawley] p. 117, 4th line from bottom. (Contributed by NM, 8-Jun-2013.) |
⊢ EDRingR = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {〈(Base‘ndx), ((TEndo‘𝑘)‘𝑤)〉, 〈(+g‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))〉, 〈(.r‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑡 ∘ 𝑠))〉})) | ||
Definition | df-edring 38053* | Define division ring on trace-preserving endomorphisms. The multiplication operation is reversed composition, per the definition of E of [Crawley] p. 117, 4th line from bottom. (Contributed by NM, 8-Jun-2013.) |
⊢ EDRing = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ {〈(Base‘ndx), ((TEndo‘𝑘)‘𝑤)〉, 〈(+g‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))〉, 〈(.r‘ndx), (𝑠 ∈ ((TEndo‘𝑘)‘𝑤), 𝑡 ∈ ((TEndo‘𝑘)‘𝑤) ↦ (𝑠 ∘ 𝑡))〉})) | ||
Theorem | tendofset 38054* | The set of all trace-preserving endomorphisms on the set of translations for a lattice 𝐾. (Contributed by NM, 8-Jun-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑉 → (TEndo‘𝐾) = (𝑤 ∈ 𝐻 ↦ {𝑠 ∣ (𝑠:((LTrn‘𝐾)‘𝑤)⟶((LTrn‘𝐾)‘𝑤) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)(((trL‘𝐾)‘𝑤)‘(𝑠‘𝑓)) ≤ (((trL‘𝐾)‘𝑤)‘𝑓))})) | ||
Theorem | tendoset 38055* | The set of trace-preserving endomorphisms on the set of translations for a fiducial co-atom 𝑊. (Contributed by NM, 8-Jun-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝐸 = {𝑠 ∣ (𝑠:𝑇⟶𝑇 ∧ ∀𝑓 ∈ 𝑇 ∀𝑔 ∈ 𝑇 (𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ 𝑇 (𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓))}) | ||
Theorem | istendo 38056* | The predicate "is a trace-preserving endomorphism". Similar to definition of trace-preserving endomorphism in [Crawley] p. 117, penultimate line. (Contributed by NM, 8-Jun-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → (𝑆 ∈ 𝐸 ↔ (𝑆:𝑇⟶𝑇 ∧ ∀𝑓 ∈ 𝑇 ∀𝑔 ∈ 𝑇 (𝑆‘(𝑓 ∘ 𝑔)) = ((𝑆‘𝑓) ∘ (𝑆‘𝑔)) ∧ ∀𝑓 ∈ 𝑇 (𝑅‘(𝑆‘𝑓)) ≤ (𝑅‘𝑓)))) | ||
Theorem | tendotp 38057 | Trace-preserving property of a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇) → (𝑅‘(𝑆‘𝐹)) ≤ (𝑅‘𝐹)) | ||
Theorem | istendod 38058* | Deduce the predicate "is a trace-preserving endomorphism". (Contributed by NM, 9-Jun-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑆:𝑇⟶𝑇) & ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑇 ∧ 𝑔 ∈ 𝑇) → (𝑆‘(𝑓 ∘ 𝑔)) = ((𝑆‘𝑓) ∘ (𝑆‘𝑔))) & ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑇) → (𝑅‘(𝑆‘𝑓)) ≤ (𝑅‘𝑓)) ⇒ ⊢ (𝜑 → 𝑆 ∈ 𝐸) | ||
Theorem | tendof 38059 | Functionality of a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) → 𝑆:𝑇⟶𝑇) | ||
Theorem | tendoeq1 38060* | Condition determining equality of two trace-preserving endomorphisms. (Contributed by NM, 11-Jun-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) ∧ ∀𝑓 ∈ 𝑇 (𝑈‘𝑓) = (𝑉‘𝑓)) → 𝑈 = 𝑉) | ||
Theorem | tendovalco 38061 | Value of composition of translations in a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ∧ 𝑆 ∈ 𝐸) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) → (𝑆‘(𝐹 ∘ 𝐺)) = ((𝑆‘𝐹) ∘ (𝑆‘𝐺))) | ||
Theorem | tendocoval 38062 | Value of composition of endomorphisms in a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) ∧ 𝐹 ∈ 𝑇) → ((𝑈 ∘ 𝑉)‘𝐹) = (𝑈‘(𝑉‘𝐹))) | ||
Theorem | tendocl 38063 | Closure of a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇) → (𝑆‘𝐹) ∈ 𝑇) | ||
Theorem | tendoco2 38064 | Distribution of compositions in preparation for endomorphism sum definition. (Contributed by NM, 10-Jun-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) → ((𝑈‘(𝐹 ∘ 𝐺)) ∘ (𝑉‘(𝐹 ∘ 𝐺))) = (((𝑈‘𝐹) ∘ (𝑉‘𝐹)) ∘ ((𝑈‘𝐺) ∘ (𝑉‘𝐺)))) | ||
Theorem | tendoidcl 38065 | The identity is a trace-preserving endomorphism. (Contributed by NM, 30-Jul-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( I ↾ 𝑇) ∈ 𝐸) | ||
Theorem | tendo1mul 38066 | Multiplicative identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 20-Nov-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸) → (( I ↾ 𝑇) ∘ 𝑈) = 𝑈) | ||
Theorem | tendo1mulr 38067 | Multiplicative identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 20-Nov-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸) → (𝑈 ∘ ( I ↾ 𝑇)) = 𝑈) | ||
Theorem | tendococl 38068 | The composition of two trace-preserving endomorphisms (multiplication in the endormorphism ring) is a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝑇 ∈ 𝐸) → (𝑆 ∘ 𝑇) ∈ 𝐸) | ||
Theorem | tendoid 38069 | The identity value of a trace-preserving endomorphism. (Contributed by NM, 21-Jun-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) → (𝑆‘( I ↾ 𝐵)) = ( I ↾ 𝐵)) | ||
Theorem | tendoeq2 38070* | Condition determining equality of two trace-preserving endomorphisms, showing it is unnecessary to consider the identity translation. In tendocan 38120, we show that we only need to consider a single non-identity translation. (Contributed by NM, 21-Jun-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) ∧ ∀𝑓 ∈ 𝑇 (𝑓 ≠ ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓))) → 𝑈 = 𝑉) | ||
Theorem | tendoplcbv 38071* | Define sum operation for trace-preserving endomorphisms. Change bound variables to isolate them later. (Contributed by NM, 11-Jun-2013.) |
⊢ 𝑃 = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓)))) ⇒ ⊢ 𝑃 = (𝑢 ∈ 𝐸, 𝑣 ∈ 𝐸 ↦ (𝑔 ∈ 𝑇 ↦ ((𝑢‘𝑔) ∘ (𝑣‘𝑔)))) | ||
Theorem | tendopl 38072* | Value of endomorphism sum operation. (Contributed by NM, 10-Jun-2013.) |
⊢ 𝑃 = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓)))) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) ⇒ ⊢ ((𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) → (𝑈𝑃𝑉) = (𝑔 ∈ 𝑇 ↦ ((𝑈‘𝑔) ∘ (𝑉‘𝑔)))) | ||
Theorem | tendopl2 38073* | Value of result of endomorphism sum operation. (Contributed by NM, 10-Jun-2013.) |
⊢ 𝑃 = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓)))) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) ⇒ ⊢ ((𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇) → ((𝑈𝑃𝑉)‘𝐹) = ((𝑈‘𝐹) ∘ (𝑉‘𝐹))) | ||
Theorem | tendoplcl2 38074* | Value of result of endomorphism sum operation. (Contributed by NM, 10-Jun-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑃 = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓)))) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) ∧ 𝐹 ∈ 𝑇) → ((𝑈𝑃𝑉)‘𝐹) ∈ 𝑇) | ||
Theorem | tendoplco2 38075* | Value of result of endomorphism sum operation on a translation composition. (Contributed by NM, 10-Jun-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑃 = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓)))) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) → ((𝑈𝑃𝑉)‘(𝐹 ∘ 𝐺)) = (((𝑈𝑃𝑉)‘𝐹) ∘ ((𝑈𝑃𝑉)‘𝐺))) | ||
Theorem | tendopltp 38076* | Trace-preserving property of endomorphism sum operation 𝑃, based on theorem trlco 38023. Part of remark in [Crawley] p. 118, 2nd line, "it is clear from the second part of G (our trlco 38023) that Delta is a subring of E." (In our development, we will bypass their E and go directly to their Delta, whose base set is our (TEndo‘𝐾)‘𝑊.) (Contributed by NM, 9-Jun-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑃 = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓)))) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) ∧ 𝐹 ∈ 𝑇) → (𝑅‘((𝑈𝑃𝑉)‘𝐹)) ≤ (𝑅‘𝐹)) | ||
Theorem | tendoplcl 38077* | Endomorphism sum is a trace-preserving endomorphism. (Contributed by NM, 10-Jun-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑃 = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓)))) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) → (𝑈𝑃𝑉) ∈ 𝐸) | ||
Theorem | tendoplcom 38078* | The endomorphism sum operation is commutative. (Contributed by NM, 11-Jun-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑃 = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓)))) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) → (𝑈𝑃𝑉) = (𝑉𝑃𝑈)) | ||
Theorem | tendoplass 38079* | The endomorphism sum operation is associative. (Contributed by NM, 11-Jun-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑃 = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓)))) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → ((𝑆𝑃𝑈)𝑃𝑉) = (𝑆𝑃(𝑈𝑃𝑉))) | ||
Theorem | tendodi1 38080* | Endomorphism composition distributes over sum. (Contributed by NM, 13-Jun-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑃 = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓)))) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → (𝑆 ∘ (𝑈𝑃𝑉)) = ((𝑆 ∘ 𝑈)𝑃(𝑆 ∘ 𝑉))) | ||
Theorem | tendodi2 38081* | Endomorphism composition distributes over sum. (Contributed by NM, 13-Jun-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑃 = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓)))) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → ((𝑆𝑃𝑈) ∘ 𝑉) = ((𝑆 ∘ 𝑉)𝑃(𝑈 ∘ 𝑉))) | ||
Theorem | tendo0cbv 38082* | Define additive identity for trace-preserving endomorphisms. Change bound variable to isolate it later. (Contributed by NM, 11-Jun-2013.) |
⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵)) ⇒ ⊢ 𝑂 = (𝑔 ∈ 𝑇 ↦ ( I ↾ 𝐵)) | ||
Theorem | tendo02 38083* | Value of additive identity endomorphism. (Contributed by NM, 11-Jun-2013.) |
⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵)) & ⊢ 𝐵 = (Base‘𝐾) ⇒ ⊢ (𝐹 ∈ 𝑇 → (𝑂‘𝐹) = ( I ↾ 𝐵)) | ||
Theorem | tendo0co2 38084* | The additive identity trace-preserving endormorphism preserves composition of translations. TODO: why isn't this a special case of tendospdi1 38316? (Contributed by NM, 11-Jun-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵)) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝑂‘(𝐹 ∘ 𝐺)) = ((𝑂‘𝐹) ∘ (𝑂‘𝐺))) | ||
Theorem | tendo0tp 38085* | Trace-preserving property of endomorphism additive identity. (Contributed by NM, 11-Jun-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵)) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝑅‘(𝑂‘𝐹)) ≤ (𝑅‘𝐹)) | ||
Theorem | tendo0cl 38086* | The additive identity is a trace-preserving endormorphism. (Contributed by NM, 12-Jun-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵)) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑂 ∈ 𝐸) | ||
Theorem | tendo0pl 38087* | Property of the additive identity endormorphism. (Contributed by NM, 12-Jun-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵)) & ⊢ 𝑃 = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓)))) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) → (𝑂𝑃𝑆) = 𝑆) | ||
Theorem | tendo0plr 38088* | Property of the additive identity endormorphism. (Contributed by NM, 21-Feb-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵)) & ⊢ 𝑃 = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓)))) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) → (𝑆𝑃𝑂) = 𝑆) | ||
Theorem | tendoicbv 38089* | Define inverse function for trace-preserving endomorphisms. Change bound variable to isolate it later. (Contributed by NM, 12-Jun-2013.) |
⊢ 𝐼 = (𝑠 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ◡(𝑠‘𝑓))) ⇒ ⊢ 𝐼 = (𝑢 ∈ 𝐸 ↦ (𝑔 ∈ 𝑇 ↦ ◡(𝑢‘𝑔))) | ||
Theorem | tendoi 38090* | Value of inverse endomorphism. (Contributed by NM, 12-Jun-2013.) |
⊢ 𝐼 = (𝑠 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ◡(𝑠‘𝑓))) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) ⇒ ⊢ (𝑆 ∈ 𝐸 → (𝐼‘𝑆) = (𝑔 ∈ 𝑇 ↦ ◡(𝑆‘𝑔))) | ||
Theorem | tendoi2 38091* | Value of additive inverse endomorphism. (Contributed by NM, 12-Jun-2013.) |
⊢ 𝐼 = (𝑠 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ◡(𝑠‘𝑓))) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) ⇒ ⊢ ((𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇) → ((𝐼‘𝑆)‘𝐹) = ◡(𝑆‘𝐹)) | ||
Theorem | tendoicl 38092* | Closure of the additive inverse endomorphism. (Contributed by NM, 12-Jun-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝐼 = (𝑠 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ◡(𝑠‘𝑓))) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) → (𝐼‘𝑆) ∈ 𝐸) | ||
Theorem | tendoipl 38093* | Property of the additive inverse endomorphism. (Contributed by NM, 12-Jun-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝐼 = (𝑠 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ◡(𝑠‘𝑓))) & ⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑃 = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓)))) & ⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵)) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) → ((𝐼‘𝑆)𝑃𝑆) = 𝑂) | ||
Theorem | tendoipl2 38094* | Property of the additive inverse endomorphism. (Contributed by NM, 29-Sep-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝐼 = (𝑠 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ◡(𝑠‘𝑓))) & ⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑃 = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓)))) & ⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵)) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) → (𝑆𝑃(𝐼‘𝑆)) = 𝑂) | ||
Theorem | erngfset 38095* | The division rings on trace-preserving endomorphisms for a lattice 𝐾. (Contributed by NM, 8-Jun-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑉 → (EDRing‘𝐾) = (𝑤 ∈ 𝐻 ↦ {〈(Base‘ndx), ((TEndo‘𝐾)‘𝑤)〉, 〈(+g‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑡 ∈ ((TEndo‘𝐾)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))〉, 〈(.r‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑡 ∈ ((TEndo‘𝐾)‘𝑤) ↦ (𝑠 ∘ 𝑡))〉})) | ||
Theorem | erngset 38096* | The division ring on trace-preserving endomorphisms for a fiducial co-atom 𝑊. (Contributed by NM, 5-Jun-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝐷 = ((EDRing‘𝐾)‘𝑊) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝐷 = {〈(Base‘ndx), 𝐸〉, 〈(+g‘ndx), (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))〉, 〈(.r‘ndx), (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑠 ∘ 𝑡))〉}) | ||
Theorem | erngbase 38097 | The base set of the division ring on trace-preserving endomorphisms is the set of all trace-preserving endomorphisms (for a fiducial co-atom 𝑊). TODO: the .t hypothesis isn't used. (Also look at others.) (Contributed by NM, 9-Jun-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝐷 = ((EDRing‘𝐾)‘𝑊) & ⊢ 𝐶 = (Base‘𝐷) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝐶 = 𝐸) | ||
Theorem | erngfplus 38098* | Ring addition operation. (Contributed by NM, 9-Jun-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝐷 = ((EDRing‘𝐾)‘𝑊) & ⊢ + = (+g‘𝐷) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → + = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))) | ||
Theorem | erngplus 38099* | Ring addition operation. (Contributed by NM, 10-Jun-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝐷 = ((EDRing‘𝐾)‘𝑊) & ⊢ + = (+g‘𝐷) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → (𝑈 + 𝑉) = (𝑓 ∈ 𝑇 ↦ ((𝑈‘𝑓) ∘ (𝑉‘𝑓)))) | ||
Theorem | erngplus2 38100 | Ring addition operation. (Contributed by NM, 10-Jun-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝐷 = ((EDRing‘𝐾)‘𝑊) & ⊢ + = (+g‘𝐷) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇)) → ((𝑈 + 𝑉)‘𝐹) = ((𝑈‘𝐹) ∘ (𝑉‘𝐹))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |