This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tendo0cl

Description: The additive identity is a trace-preserving endormorphism. (Contributed by NM, 12-Jun-2013)

Ref Expression
Hypotheses tendo0.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
tendo0.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
tendo0.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
tendo0.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
tendo0.o ⊢ 𝑂 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
Assertion tendo0cl ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑂 ∈ 𝐸 )

Proof

Step Hyp Ref Expression
1 tendo0.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 tendo0.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 tendo0.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4 tendo0.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
5 tendo0.o ⊢ 𝑂 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
6 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
7 eqid ⊢ ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
8 id ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9 1 2 3 idltrn ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝐵 ) ∈ 𝑇 )
10 9 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝑇 ) → ( I ↾ 𝐵 ) ∈ 𝑇 )
11 5 tendo0cbv ⊢ 𝑂 = ( 𝑔 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
12 10 11 fmptd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑂 : 𝑇 ⟶ 𝑇 )
13 1 2 3 4 5 tendo0co2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇 ) → ( 𝑂 ‘ ( 𝑔 ∘ ℎ ) ) = ( ( 𝑂 ‘ 𝑔 ) ∘ ( 𝑂 ‘ ℎ ) ) )
14 1 2 3 4 5 6 7 tendo0tp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝑇 ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑂 ‘ 𝑔 ) ) ( le ‘ 𝐾 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑔 ) )
15 6 2 3 7 4 8 12 13 14 istendod ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑂 ∈ 𝐸 )