Metamath Proof Explorer

Theorem tendoid

Description: The identity value of a trace-preserving endomorphism. (Contributed by NM, 21-Jun-2013)

Ref Expression
Hypotheses tendoid.b ⊢B=BaseK
tendoid.h ⊢H=LHyp⁡K
tendoid.e ⊢E=TEndo⁡K⁡W
Assertion tendoid ⊢K∈HL∧W∈H∧S∈E→S⁡I↾B=I↾B

Proof

Step Hyp Ref Expression
1 tendoid.b ⊢B=BaseK
2 tendoid.h ⊢H=LHyp⁡K
3 tendoid.e ⊢E=TEndo⁡K⁡W
4 eqid ⊢LTrn⁡K⁡W=LTrn⁡K⁡W
5 1 2 4 idltrn ⊢K∈HL∧W∈H→I↾B∈LTrn⁡K⁡W
6 5 adantr ⊢K∈HL∧W∈H∧S∈E→I↾B∈LTrn⁡K⁡W
7 eqid ⊢≤K=≤K
8 eqid ⊢trL⁡K⁡W=trL⁡K⁡W
9 7 2 4 8 3 tendotp ⊢K∈HL∧W∈H∧S∈E∧I↾B∈LTrn⁡K⁡W→trL⁡K⁡W⁡S⁡I↾B≤KtrL⁡K⁡W⁡I↾B
10 6 9 mpd3an3 ⊢K∈HL∧W∈H∧S∈E→trL⁡K⁡W⁡S⁡I↾B≤KtrL⁡K⁡W⁡I↾B
11 eqid ⊢0.⁡K=0.⁡K
12 1 11 2 8 trlid0 ⊢K∈HL∧W∈H→trL⁡K⁡W⁡I↾B=0.⁡K
13 12 adantr ⊢K∈HL∧W∈H∧S∈E→trL⁡K⁡W⁡I↾B=0.⁡K
14 10 13 breqtrd ⊢K∈HL∧W∈H∧S∈E→trL⁡K⁡W⁡S⁡I↾B≤K0.⁡K
15 hlop ⊢K∈HL→K∈OP
16 15 ad2antrr ⊢K∈HL∧W∈H∧S∈E→K∈OP
17 2 4 3 tendocl ⊢K∈HL∧W∈H∧S∈E∧I↾B∈LTrn⁡K⁡W→S⁡I↾B∈LTrn⁡K⁡W
18 6 17 mpd3an3 ⊢K∈HL∧W∈H∧S∈E→S⁡I↾B∈LTrn⁡K⁡W
19 1 2 4 8 trlcl ⊢K∈HL∧W∈H∧S⁡I↾B∈LTrn⁡K⁡W→trL⁡K⁡W⁡S⁡I↾B∈B
20 18 19 syldan ⊢K∈HL∧W∈H∧S∈E→trL⁡K⁡W⁡S⁡I↾B∈B
21 1 7 11 ople0 ⊢K∈OP∧trL⁡K⁡W⁡S⁡I↾B∈B→trL⁡K⁡W⁡S⁡I↾B≤K0.⁡K↔trL⁡K⁡W⁡S⁡I↾B=0.⁡K
22 16 20 21 syl2anc ⊢K∈HL∧W∈H∧S∈E→trL⁡K⁡W⁡S⁡I↾B≤K0.⁡K↔trL⁡K⁡W⁡S⁡I↾B=0.⁡K
23 14 22 mpbid ⊢K∈HL∧W∈H∧S∈E→trL⁡K⁡W⁡S⁡I↾B=0.⁡K
24 1 11 2 4 8 trlid0b ⊢K∈HL∧W∈H∧S⁡I↾B∈LTrn⁡K⁡W→S⁡I↾B=I↾B↔trL⁡K⁡W⁡S⁡I↾B=0.⁡K
25 18 24 syldan ⊢K∈HL∧W∈H∧S∈E→S⁡I↾B=I↾B↔trL⁡K⁡W⁡S⁡I↾B=0.⁡K
26 23 25 mpbird ⊢K∈HL∧W∈H∧S∈E→S⁡I↾B=I↾B