Metamath Proof Explorer

Theorem tendoidcl

Description: The identity is a trace-preserving endomorphism. (Contributed by NM, 30-Jul-2013)

Ref Expression
Hypotheses tendof.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
tendof.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
tendof.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
Assertion tendoidcl ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝑇 ) ∈ 𝐸 )

Proof

Step Hyp Ref Expression
1 tendof.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 tendof.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 tendof.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
4 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
5 eqid ⊢ ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
6 id ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7 f1oi ⊢ ( I ↾ 𝑇 ) : 𝑇 –1-1-onto→ 𝑇
8 f1of ⊢ ( ( I ↾ 𝑇 ) : 𝑇 –1-1-onto→ 𝑇 → ( I ↾ 𝑇 ) : 𝑇 ⟶ 𝑇 )
9 7 8 mp1i ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝑇 ) : 𝑇 ⟶ 𝑇 )
10 1 2 ltrnco ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ 𝑇 ∧ 𝑔 ∈ 𝑇 ) → ( 𝑓 ∘ 𝑔 ) ∈ 𝑇 )
11 fvresi ⊢ ( ( 𝑓 ∘ 𝑔 ) ∈ 𝑇 → ( ( I ↾ 𝑇 ) ‘ ( 𝑓 ∘ 𝑔 ) ) = ( 𝑓 ∘ 𝑔 ) )
12 10 11 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ 𝑇 ∧ 𝑔 ∈ 𝑇 ) → ( ( I ↾ 𝑇 ) ‘ ( 𝑓 ∘ 𝑔 ) ) = ( 𝑓 ∘ 𝑔 ) )
13 fvresi ⊢ ( 𝑓 ∈ 𝑇 → ( ( I ↾ 𝑇 ) ‘ 𝑓 ) = 𝑓 )
14 13 3ad2ant2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ 𝑇 ∧ 𝑔 ∈ 𝑇 ) → ( ( I ↾ 𝑇 ) ‘ 𝑓 ) = 𝑓 )
15 fvresi ⊢ ( 𝑔 ∈ 𝑇 → ( ( I ↾ 𝑇 ) ‘ 𝑔 ) = 𝑔 )
16 15 3ad2ant3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ 𝑇 ∧ 𝑔 ∈ 𝑇 ) → ( ( I ↾ 𝑇 ) ‘ 𝑔 ) = 𝑔 )
17 14 16 coeq12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ 𝑇 ∧ 𝑔 ∈ 𝑇 ) → ( ( ( I ↾ 𝑇 ) ‘ 𝑓 ) ∘ ( ( I ↾ 𝑇 ) ‘ 𝑔 ) ) = ( 𝑓 ∘ 𝑔 ) )
18 12 17 eqtr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ 𝑇 ∧ 𝑔 ∈ 𝑇 ) → ( ( I ↾ 𝑇 ) ‘ ( 𝑓 ∘ 𝑔 ) ) = ( ( ( I ↾ 𝑇 ) ‘ 𝑓 ) ∘ ( ( I ↾ 𝑇 ) ‘ 𝑔 ) ) )
19 13 adantl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ 𝑇 ) → ( ( I ↾ 𝑇 ) ‘ 𝑓 ) = 𝑓 )
20 19 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ 𝑇 ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( I ↾ 𝑇 ) ‘ 𝑓 ) ) = ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) )
21 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
22 21 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ 𝑇 ) → 𝐾 ∈ Lat )
23 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
24 23 1 2 5 trlcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ 𝑇 ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ∈ ( Base ‘ 𝐾 ) )
25 23 4 latref ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ( le ‘ 𝐾 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) )
26 22 24 25 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ 𝑇 ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ( le ‘ 𝐾 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) )
27 20 26 eqbrtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ 𝑇 ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( I ↾ 𝑇 ) ‘ 𝑓 ) ) ( le ‘ 𝐾 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) )
28 4 1 2 5 3 6 9 18 27 istendod ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝑇 ) ∈ 𝐸 )