P. 414 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 41301-41400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cdlemg42 41301	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 41302	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 41303	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 41304	Eliminate (𝐹‘𝑃) ≠ 𝑃, (𝐺‘𝑃) ≠ 𝑃 from cdlemg44a 41303. (Contributed by NM, 3-Jun-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺)) → (𝐹‘(𝐺‘𝑃)) = (𝐺‘(𝐹‘𝑃)))
Theorem	cdlemg44 41305	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 41306	TODO: fix comment. TODO: Use this above in place of (𝐹‘𝑃) = 𝑃 antecedents? (Contributed by NM, 5-Jun-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝐹 = ( I ↾ 𝐵)) → (𝐹 ∘ 𝐺) = (𝐺 ∘ 𝐹))
Theorem	cdlemg46 41307*	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 41308*	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 41309	Eliminate ℎ from cdlemg47 41308. (Contributed by NM, 5-Jun-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) = (𝑅‘𝐺))) → (𝐹 ∘ 𝐺) = (𝐺 ∘ 𝐹))
Theorem	ltrncom 41310	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 41311	Rearrange a composition of 4 translations, analogous to an4 664. (Contributed by NM, 10-Jun-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐸 ∈ 𝑇 ∧ 𝐹 ∈ 𝑇) → ((𝐷 ∘ 𝐸) ∘ (𝐹 ∘ 𝐺)) = ((𝐷 ∘ 𝐹) ∘ (𝐸 ∘ 𝐺)))
Theorem	trljco 41312	Trace joined with trace of composition. (Contributed by NM, 15-Jun-2013.)
⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → ((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺))) = ((𝑅‘𝐹) ∨ (𝑅‘𝐺)))
Theorem	trljco2 41313	Trace joined with trace of composition. (Contributed by NM, 16-Jun-2013.)
⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → ((𝑅‘𝐹) ∨ (𝑅‘(𝐹 ∘ 𝐺))) = ((𝑅‘𝐺) ∨ (𝑅‘(𝐹 ∘ 𝐺))))
Syntax	ctgrp 41314	Extend class notation with translation group.
class TGrp
Definition	df-tgrp 41315*	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 41316*	The translation group maps for a lattice 𝐾. (Contributed by NM, 5-Jun-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → (TGrp‘𝐾) = (𝑤 ∈ 𝐻 ↦ {⟨(Base‘ndx), ((LTrn‘𝐾)‘𝑤)⟩, ⟨(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))⟩}))
Theorem	tgrpset 41317*	The translation group for a fiducial co-atom 𝑊. (Contributed by NM, 5-Jun-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((TGrp‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝐺 = {⟨(Base‘ndx), 𝑇⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑇, 𝑔 ∈ 𝑇 ↦ (𝑓 ∘ 𝑔))⟩})
Theorem	tgrpbase 41318	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 41319*	The group operation of the translation group is function composition. (Contributed by NM, 5-Jun-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((TGrp‘𝐾)‘𝑊)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → + = (𝑓 ∈ 𝑇, 𝑔 ∈ 𝑇 ↦ (𝑓 ∘ 𝑔)))
Theorem	tgrpov 41320	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 41321	Lemma for tgrpgrp 41322. (Contributed by NM, 6-Jun-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐺 = ((TGrp‘𝐾)‘𝑊)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝐵 = (Base‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐺 ∈ Grp)
Theorem	tgrpgrp 41322	The translation group is a group. (Contributed by NM, 6-Jun-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐺 = ((TGrp‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐺 ∈ Grp)
Theorem	tgrpabl 41323	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 41324	Extend class notation with translation group endomorphisms.
class TEndo
Syntax	cedring 41325	Extend class notation with division ring on trace-preserving endomorphisms.
class EDRing
Syntax	cedring-rN 41326	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 41327*	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 41328*	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 41329*	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 41330*	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 41331*	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 41332*	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 41333	Trace-preserving property of a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇) → (𝑅‘(𝑆‘𝐹)) ≤ (𝑅‘𝐹))
Theorem	istendod 41334*	Deduce the predicate "is a trace-preserving endomorphism". (Contributed by NM, 9-Jun-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ (𝜑 → (𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻))    &   ⊢ (𝜑 → 𝑆:𝑇⟶𝑇)    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑇 ∧ 𝑔 ∈ 𝑇) → (𝑆‘(𝑓 ∘ 𝑔)) = ((𝑆‘𝑓) ∘ (𝑆‘𝑔)))    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑇) → (𝑅‘(𝑆‘𝑓)) ≤ (𝑅‘𝑓))    ⇒   ⊢ (𝜑 → 𝑆 ∈ 𝐸)
Theorem	tendof 41335	Functionality of a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) → 𝑆:𝑇⟶𝑇)
Theorem	tendoeq1 41336*	Condition determining equality of two trace-preserving endomorphisms. (Contributed by NM, 11-Jun-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) ∧ ∀𝑓 ∈ 𝑇 (𝑈‘𝑓) = (𝑉‘𝑓)) → 𝑈 = 𝑉)
Theorem	tendovalco 41337	Value of composition of translations in a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ∧ 𝑆 ∈ 𝐸) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) → (𝑆‘(𝐹 ∘ 𝐺)) = ((𝑆‘𝐹) ∘ (𝑆‘𝐺)))
Theorem	tendocoval 41338	Value of composition of endomorphisms in a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) ∧ 𝐹 ∈ 𝑇) → ((𝑈 ∘ 𝑉)‘𝐹) = (𝑈‘(𝑉‘𝐹)))
Theorem	tendocl 41339	Closure of a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇) → (𝑆‘𝐹) ∈ 𝑇)
Theorem	tendoco2 41340	Distribution of compositions in preparation for endomorphism sum definition. (Contributed by NM, 10-Jun-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) → ((𝑈‘(𝐹 ∘ 𝐺)) ∘ (𝑉‘(𝐹 ∘ 𝐺))) = (((𝑈‘𝐹) ∘ (𝑉‘𝐹)) ∘ ((𝑈‘𝐺) ∘ (𝑉‘𝐺))))
Theorem	tendoidcl 41341	The identity is a trace-preserving endomorphism. (Contributed by NM, 30-Jul-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( I ↾ 𝑇) ∈ 𝐸)
Theorem	tendo1mul 41342	Multiplicative identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 20-Nov-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸) → (( I ↾ 𝑇) ∘ 𝑈) = 𝑈)
Theorem	tendo1mulr 41343	Multiplicative identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 20-Nov-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸) → (𝑈 ∘ ( I ↾ 𝑇)) = 𝑈)
Theorem	tendococl 41344	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 41345	The identity value of a trace-preserving endomorphism. (Contributed by NM, 21-Jun-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) → (𝑆‘( I ↾ 𝐵)) = ( I ↾ 𝐵))
Theorem	tendoeq2 41346*	Condition determining equality of two trace-preserving endomorphisms, showing it is unnecessary to consider the identity translation. In tendocan 41396, 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 41347*	Define sum operation for trace-preserving endomorphisms. Change bound variables to isolate them later. (Contributed by NM, 11-Jun-2013.)
⊢ 𝑃 = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))    ⇒   ⊢ 𝑃 = (𝑢 ∈ 𝐸, 𝑣 ∈ 𝐸 ↦ (𝑔 ∈ 𝑇 ↦ ((𝑢‘𝑔) ∘ (𝑣‘𝑔))))
Theorem	tendopl 41348*	Value of endomorphism sum operation. (Contributed by NM, 10-Jun-2013.)
⊢ 𝑃 = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ ((𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) → (𝑈𝑃𝑉) = (𝑔 ∈ 𝑇 ↦ ((𝑈‘𝑔) ∘ (𝑉‘𝑔))))
Theorem	tendopl2 41349*	Value of result of endomorphism sum operation. (Contributed by NM, 10-Jun-2013.)
⊢ 𝑃 = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ ((𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇) → ((𝑈𝑃𝑉)‘𝐹) = ((𝑈‘𝐹) ∘ (𝑉‘𝐹)))
Theorem	tendoplcl2 41350*	Value of result of endomorphism sum operation. (Contributed by NM, 10-Jun-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑃 = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) ∧ 𝐹 ∈ 𝑇) → ((𝑈𝑃𝑉)‘𝐹) ∈ 𝑇)
Theorem	tendoplco2 41351*	Value of result of endomorphism sum operation on a translation composition. (Contributed by NM, 10-Jun-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑃 = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) → ((𝑈𝑃𝑉)‘(𝐹 ∘ 𝐺)) = (((𝑈𝑃𝑉)‘𝐹) ∘ ((𝑈𝑃𝑉)‘𝐺)))
Theorem	tendopltp 41352*	Trace-preserving property of endomorphism sum operation 𝑃, based on Theorems trlco 41299. Part of remark in [Crawley] p. 118, 2nd line, "it is clear from the second part of G (our trlco 41299) 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 41353*	Endomorphism sum is a trace-preserving endomorphism. (Contributed by NM, 10-Jun-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑃 = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) → (𝑈𝑃𝑉) ∈ 𝐸)
Theorem	tendoplcom 41354*	The endomorphism sum operation is commutative. (Contributed by NM, 11-Jun-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑃 = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) → (𝑈𝑃𝑉) = (𝑉𝑃𝑈))
Theorem	tendoplass 41355*	The endomorphism sum operation is associative. (Contributed by NM, 11-Jun-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑃 = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → ((𝑆𝑃𝑈)𝑃𝑉) = (𝑆𝑃(𝑈𝑃𝑉)))
Theorem	tendodi1 41356*	Endomorphism composition distributes over sum. (Contributed by NM, 13-Jun-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑃 = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → (𝑆 ∘ (𝑈𝑃𝑉)) = ((𝑆 ∘ 𝑈)𝑃(𝑆 ∘ 𝑉)))
Theorem	tendodi2 41357*	Endomorphism composition distributes over sum. (Contributed by NM, 13-Jun-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑃 = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → ((𝑆𝑃𝑈) ∘ 𝑉) = ((𝑆 ∘ 𝑉)𝑃(𝑈 ∘ 𝑉)))
Theorem	tendo0cbv 41358*	Define additive identity for trace-preserving endomorphisms. Change bound variable to isolate it later. (Contributed by NM, 11-Jun-2013.)
⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))    ⇒   ⊢ 𝑂 = (𝑔 ∈ 𝑇 ↦ ( I ↾ 𝐵))
Theorem	tendo02 41359*	Value of additive identity endomorphism. (Contributed by NM, 11-Jun-2013.)
⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝐵 = (Base‘𝐾)    ⇒   ⊢ (𝐹 ∈ 𝑇 → (𝑂‘𝐹) = ( I ↾ 𝐵))
Theorem	tendo0co2 41360*	The additive identity trace-preserving endormorphism preserves composition of translations. TODO: why isn't this a special case of tendospdi1 41592? (Contributed by NM, 11-Jun-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝑂‘(𝐹 ∘ 𝐺)) = ((𝑂‘𝐹) ∘ (𝑂‘𝐺)))
Theorem	tendo0tp 41361*	Trace-preserving property of endomorphism additive identity. (Contributed by NM, 11-Jun-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝑅‘(𝑂‘𝐹)) ≤ (𝑅‘𝐹))
Theorem	tendo0cl 41362*	The additive identity is a trace-preserving endormorphism. (Contributed by NM, 12-Jun-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑂 ∈ 𝐸)
Theorem	tendo0pl 41363*	Property of the additive identity endormorphism. (Contributed by NM, 12-Jun-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝑃 = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) → (𝑂𝑃𝑆) = 𝑆)
Theorem	tendo0plr 41364*	Property of the additive identity endormorphism. (Contributed by NM, 21-Feb-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))    &   ⊢ 𝑃 = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) → (𝑆𝑃𝑂) = 𝑆)
Theorem	tendoicbv 41365*	Define inverse function for trace-preserving endomorphisms. Change bound variable to isolate it later. (Contributed by NM, 12-Jun-2013.)
⊢ 𝐼 = (𝑠 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ◡(𝑠‘𝑓)))    ⇒   ⊢ 𝐼 = (𝑢 ∈ 𝐸 ↦ (𝑔 ∈ 𝑇 ↦ ◡(𝑢‘𝑔)))
Theorem	tendoi 41366*	Value of inverse endomorphism. (Contributed by NM, 12-Jun-2013.)
⊢ 𝐼 = (𝑠 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ◡(𝑠‘𝑓)))    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ (𝑆 ∈ 𝐸 → (𝐼‘𝑆) = (𝑔 ∈ 𝑇 ↦ ◡(𝑆‘𝑔)))
Theorem	tendoi2 41367*	Value of additive inverse endomorphism. (Contributed by NM, 12-Jun-2013.)
⊢ 𝐼 = (𝑠 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ◡(𝑠‘𝑓)))    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    ⇒   ⊢ ((𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇) → ((𝐼‘𝑆)‘𝐹) = ◡(𝑆‘𝐹))
Theorem	tendoicl 41368*	Closure of the additive inverse endomorphism. (Contributed by NM, 12-Jun-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐼 = (𝑠 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ◡(𝑠‘𝑓)))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) → (𝐼‘𝑆) ∈ 𝐸)
Theorem	tendoipl 41369*	Property of the additive inverse endomorphism. (Contributed by NM, 12-Jun-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐼 = (𝑠 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ◡(𝑠‘𝑓)))    &   ⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑃 = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))    &   ⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) → ((𝐼‘𝑆)𝑃𝑆) = 𝑂)
Theorem	tendoipl2 41370*	Property of the additive inverse endomorphism. (Contributed by NM, 29-Sep-2014.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐼 = (𝑠 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ◡(𝑠‘𝑓)))    &   ⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑃 = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))    &   ⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) → (𝑆𝑃(𝐼‘𝑆)) = 𝑂)
Theorem	erngfset 41371*	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 41372*	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 41373	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 41374*	Ring addition operation. (Contributed by NM, 9-Jun-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐷 = ((EDRing‘𝐾)‘𝑊)    &   ⊢ + = (+g‘𝐷)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → + = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓)))))
Theorem	erngplus 41375*	Ring addition operation. (Contributed by NM, 10-Jun-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐷 = ((EDRing‘𝐾)‘𝑊)    &   ⊢ + = (+g‘𝐷)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → (𝑈 + 𝑉) = (𝑓 ∈ 𝑇 ↦ ((𝑈‘𝑓) ∘ (𝑉‘𝑓))))
Theorem	erngplus2 41376	Ring addition operation. (Contributed by NM, 10-Jun-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐷 = ((EDRing‘𝐾)‘𝑊)    &   ⊢ + = (+g‘𝐷)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇)) → ((𝑈 + 𝑉)‘𝐹) = ((𝑈‘𝐹) ∘ (𝑉‘𝐹)))
Theorem	erngfmul 41377*	Ring multiplication operation. (Contributed by NM, 9-Jun-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐷 = ((EDRing‘𝐾)‘𝑊)    &   ⊢ · = (.r‘𝐷)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → · = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑠 ∘ 𝑡)))
Theorem	erngmul 41378	Ring addition operation. (Contributed by NM, 10-Jun-2013.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐷 = ((EDRing‘𝐾)‘𝑊)    &   ⊢ · = (.r‘𝐷)    ⇒   ⊢ (((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → (𝑈 · 𝑉) = (𝑈 ∘ 𝑉))
Theorem	erngfset-rN 41379*	The division rings on trace-preserving endomorphisms for a lattice 𝐾. (Contributed by NM, 8-Jun-2013.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → (EDRingR‘𝐾) = (𝑤 ∈ 𝐻 ↦ {⟨(Base‘ndx), ((TEndo‘𝐾)‘𝑤)⟩, ⟨(+g‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑡 ∈ ((TEndo‘𝐾)‘𝑤) ↦ (𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))⟩, ⟨(.r‘ndx), (𝑠 ∈ ((TEndo‘𝐾)‘𝑤), 𝑡 ∈ ((TEndo‘𝐾)‘𝑤) ↦ (𝑡 ∘ 𝑠))⟩}))
Theorem	erngset-rN 41380*	The division ring on trace-preserving endomorphisms for a fiducial co-atom 𝑊. (Contributed by NM, 5-Jun-2013.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐷 = ((EDRingR‘𝐾)‘𝑊)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝐷 = {⟨(Base‘ndx), 𝐸⟩, ⟨(+g‘ndx), (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓))))⟩, ⟨(.r‘ndx), (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑡 ∘ 𝑠))⟩})
Theorem	erngbase-rN 41381	The base set of the division ring on trace-preserving endomorphisms is the set of all trace-preserving endomorphisms (for a fiducial co-atom 𝑊). (Contributed by NM, 9-Jun-2013.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐷 = ((EDRingR‘𝐾)‘𝑊)    &   ⊢ 𝐶 = (Base‘𝐷)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝐶 = 𝐸)
Theorem	erngfplus-rN 41382*	Ring addition operation. (Contributed by NM, 9-Jun-2013.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐷 = ((EDRingR‘𝐾)‘𝑊)    &   ⊢ + = (+g‘𝐷)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → + = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓)))))
Theorem	erngplus-rN 41383*	Ring addition operation. (Contributed by NM, 10-Jun-2013.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐷 = ((EDRingR‘𝐾)‘𝑊)    &   ⊢ + = (+g‘𝐷)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → (𝑈 + 𝑉) = (𝑓 ∈ 𝑇 ↦ ((𝑈‘𝑓) ∘ (𝑉‘𝑓))))
Theorem	erngplus2-rN 41384	Ring addition operation. (Contributed by NM, 10-Jun-2013.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐷 = ((EDRingR‘𝐾)‘𝑊)    &   ⊢ + = (+g‘𝐷)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇)) → ((𝑈 + 𝑉)‘𝐹) = ((𝑈‘𝐹) ∘ (𝑉‘𝐹)))
Theorem	erngfmul-rN 41385*	Ring multiplication operation. (Contributed by NM, 9-Jun-2013.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐷 = ((EDRingR‘𝐾)‘𝑊)    &   ⊢ · = (.r‘𝐷)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → · = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑡 ∘ 𝑠)))
Theorem	erngmul-rN 41386	Ring addition operation. (Contributed by NM, 10-Jun-2013.) (New usage is discouraged.)
⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝐷 = ((EDRingR‘𝐾)‘𝑊)    &   ⊢ · = (.r‘𝐷)    ⇒   ⊢ (((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → (𝑈 · 𝑉) = (𝑉 ∘ 𝑈))
Theorem	cdlemh1 41387	Part of proof of Lemma H of [Crawley] p. 118. (Contributed by NM, 17-Jun-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝑆 = ((𝑃 ∨ (𝑅‘𝐺)) ∧ (𝑄 ∨ (𝑅‘(𝐺 ∘ ◡𝐹))))    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹)) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑆 ∨ (𝑅‘(𝐺 ∘ ◡𝐹))) = (𝑄 ∨ (𝑅‘(𝐺 ∘ ◡𝐹))))
Theorem	cdlemh2 41388	Part of proof of Lemma H of [Crawley] p. 118. (Contributed by NM, 16-Jun-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝑆 = ((𝑃 ∨ (𝑅‘𝐺)) ∧ (𝑄 ∨ (𝑅‘(𝐺 ∘ ◡𝐹))))    &   ⊢ 0 = (0.‘𝐾)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑆 ∧ 𝑊) = 0 )
Theorem	cdlemh 41389	Lemma H of [Crawley] p. 118. (Contributed by NM, 17-Jun-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝑆 = ((𝑃 ∨ (𝑅‘𝐺)) ∧ (𝑄 ∨ (𝑅‘(𝐺 ∘ ◡𝐹))))    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊))
Theorem	cdlemi1 41390	Part of proof of Lemma I of [Crawley] p. 118. (Contributed by NM, 18-Jun-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑈‘𝐺)‘𝑃) ≤ (𝑃 ∨ (𝑅‘𝐺)))
Theorem	cdlemi2 41391	Part of proof of Lemma I of [Crawley] p. 118. (Contributed by NM, 18-Jun-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑈‘𝐺)‘𝑃) ≤ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐹))))
Theorem	cdlemi 41392	Lemma I of [Crawley] p. 118. (Contributed by NM, 19-Jun-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑆 = ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐹))))    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑈‘𝐺)‘𝑃) = 𝑆)
Theorem	cdlemj1 41393	Part of proof of Lemma J of [Crawley] p. 118. (Contributed by NM, 19-Jun-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ (𝑈‘𝐹) = (𝑉‘𝐹)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵) ∧ ℎ ∈ 𝑇)) ∧ (ℎ ≠ ( I ↾ 𝐵) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝑔) ∧ (𝑅‘𝑔) ≠ (𝑅‘ℎ) ∧ (𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊))) → ((𝑈‘ℎ)‘𝑝) = ((𝑉‘ℎ)‘𝑝))
Theorem	cdlemj2 41394	Part of proof of Lemma J of [Crawley] p. 118. Eliminate 𝑝. (Contributed by NM, 20-Jun-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ (𝑈‘𝐹) = (𝑉‘𝐹)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵) ∧ ℎ ∈ 𝑇)) ∧ (ℎ ≠ ( I ↾ 𝐵) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐹) ≠ (𝑅‘𝑔) ∧ (𝑅‘𝑔) ≠ (𝑅‘ℎ))) → (𝑈‘ℎ) = (𝑉‘ℎ))
Theorem	cdlemj3 41395	Part of proof of Lemma J of [Crawley] p. 118. Eliminate 𝑔. (Contributed by NM, 20-Jun-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ (𝑈‘𝐹) = (𝑉‘𝐹)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵) ∧ ℎ ∈ 𝑇)) ∧ ℎ ≠ ( I ↾ 𝐵)) → (𝑈‘ℎ) = (𝑉‘ℎ))
Theorem	tendocan 41396	Cancellation law: if the values of two trace-preserving endormorphisms are equal, so are the endormorphisms. Lemma J of [Crawley] p. 118. (Contributed by NM, 21-Jun-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ (𝑈‘𝐹) = (𝑉‘𝐹)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵))) → 𝑈 = 𝑉)
Theorem	tendoid0 41397*	A trace-preserving endomorphism is the additive identity iff at least one of its values (at a non-identity translation) is the identity translation. (Contributed by NM, 1-Aug-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ (𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵))) → ((𝑈‘𝐹) = ( I ↾ 𝐵) ↔ 𝑈 = 𝑂))
Theorem	tendo0mul 41398*	Additive identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 1-Aug-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸) → (𝑂 ∘ 𝑈) = 𝑂)
Theorem	tendo0mulr 41399*	Additive identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 13-Feb-2014.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸) → (𝑈 ∘ 𝑂) = 𝑂)
Theorem	tendo1ne0 41400*	The identity (unity) is not equal to the zero trace-preserving endomorphism. (Contributed by NM, 8-Aug-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    &   ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)    &   ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)    &   ⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( I ↾ 𝑇) ≠ 𝑂)