Metamath Proof Explorer

Theorem tendoidcl

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

Ref Expression
Hypotheses tendof.h ⊢ H = LHyp ⁡ K
tendof.t ⊢ T = LTrn ⁡ K ⁡ W
tendof.e ⊢ E = TEndo ⁡ K ⁡ W
Assertion tendoidcl ⊢ K ∈ HL ∧ W ∈ H → I ↾ T ∈ E

Proof

Step Hyp Ref Expression
1 tendof.h ⊢ H = LHyp ⁡ K
2 tendof.t ⊢ T = LTrn ⁡ K ⁡ W
3 tendof.e ⊢ E = TEndo ⁡ K ⁡ W
4 eqid ⊢ ≤ K = ≤ K
5 eqid ⊢ trL ⁡ K ⁡ W = trL ⁡ K ⁡ W
6 id ⊢ K ∈ HL ∧ W ∈ H → K ∈ HL ∧ W ∈ H
7 f1oi ⊢ I ↾ T : T ⟶ 1-1 onto T
8 f1of ⊢ I ↾ T : T ⟶ 1-1 onto T → I ↾ T : T ⟶ T
9 7 8 mp1i ⊢ K ∈ HL ∧ W ∈ H → I ↾ T : T ⟶ T
10 1 2 ltrnco ⊢ K ∈ HL ∧ W ∈ H ∧ f ∈ T ∧ g ∈ T → f ∘ g ∈ T
11 fvresi ⊢ f ∘ g ∈ T → I ↾ T ⁡ f ∘ g = f ∘ g
12 10 11 syl ⊢ K ∈ HL ∧ W ∈ H ∧ f ∈ T ∧ g ∈ T → I ↾ T ⁡ f ∘ g = f ∘ g
13 fvresi ⊢ f ∈ T → I ↾ T ⁡ f = f
14 13 3ad2ant2 ⊢ K ∈ HL ∧ W ∈ H ∧ f ∈ T ∧ g ∈ T → I ↾ T ⁡ f = f
15 fvresi ⊢ g ∈ T → I ↾ T ⁡ g = g
16 15 3ad2ant3 ⊢ K ∈ HL ∧ W ∈ H ∧ f ∈ T ∧ g ∈ T → I ↾ T ⁡ g = g
17 14 16 coeq12d ⊢ K ∈ HL ∧ W ∈ H ∧ f ∈ T ∧ g ∈ T → I ↾ T ⁡ f ∘ I ↾ T ⁡ g = f ∘ g
18 12 17 eqtr4d ⊢ K ∈ HL ∧ W ∈ H ∧ f ∈ T ∧ g ∈ T → I ↾ T ⁡ f ∘ g = I ↾ T ⁡ f ∘ I ↾ T ⁡ g
19 13 adantl ⊢ K ∈ HL ∧ W ∈ H ∧ f ∈ T → I ↾ T ⁡ f = f
20 19 fveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ f ∈ T → trL ⁡ K ⁡ W ⁡ I ↾ T ⁡ f = trL ⁡ K ⁡ W ⁡ f
21 hllat ⊢ K ∈ HL → K ∈ Lat
22 21 ad2antrr ⊢ K ∈ HL ∧ W ∈ H ∧ f ∈ T → K ∈ Lat
23 eqid ⊢ Base K = Base K
24 23 1 2 5 trlcl ⊢ K ∈ HL ∧ W ∈ H ∧ f ∈ T → trL ⁡ K ⁡ W ⁡ f ∈ Base K
25 23 4 latref ⊢ K ∈ Lat ∧ trL ⁡ K ⁡ W ⁡ f ∈ Base K → trL ⁡ K ⁡ W ⁡ f ≤ K trL ⁡ K ⁡ W ⁡ f
26 22 24 25 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ f ∈ T → trL ⁡ K ⁡ W ⁡ f ≤ K trL ⁡ K ⁡ W ⁡ f
27 20 26 eqbrtrd ⊢ K ∈ HL ∧ W ∈ H ∧ f ∈ T → trL ⁡ K ⁡ W ⁡ I ↾ T ⁡ f ≤ K trL ⁡ K ⁡ W ⁡ f
28 4 1 2 5 3 6 9 18 27 istendod ⊢ K ∈ HL ∧ W ∈ H → I ↾ T ∈ E