Metamath Proof Explorer


Theorem tendotr

Description: The trace of the value of a nonzero trace-preserving endomorphism equals the trace of the argument. (Contributed by NM, 11-Aug-2013)

Ref Expression
Hypotheses tendotr.b 𝐵 = ( Base ‘ 𝐾 )
tendotr.h 𝐻 = ( LHyp ‘ 𝐾 )
tendotr.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
tendotr.r 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
tendotr.e 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
tendotr.o 𝑂 = ( 𝑓𝑇 ↦ ( I ↾ 𝐵 ) )
Assertion tendotr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑈𝑂 ) ∧ 𝐹𝑇 ) → ( 𝑅 ‘ ( 𝑈𝐹 ) ) = ( 𝑅𝐹 ) )

Proof

Step Hyp Ref Expression
1 tendotr.b 𝐵 = ( Base ‘ 𝐾 )
2 tendotr.h 𝐻 = ( LHyp ‘ 𝐾 )
3 tendotr.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4 tendotr.r 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
5 tendotr.e 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
6 tendotr.o 𝑂 = ( 𝑓𝑇 ↦ ( I ↾ 𝐵 ) )
7 simpl1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑈𝑂 ) ∧ 𝐹𝑇 ) ∧ 𝐹 = ( I ↾ 𝐵 ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
8 simpl2l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑈𝑂 ) ∧ 𝐹𝑇 ) ∧ 𝐹 = ( I ↾ 𝐵 ) ) → 𝑈𝐸 )
9 1 2 5 tendoid ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸 ) → ( 𝑈 ‘ ( I ↾ 𝐵 ) ) = ( I ↾ 𝐵 ) )
10 7 8 9 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑈𝑂 ) ∧ 𝐹𝑇 ) ∧ 𝐹 = ( I ↾ 𝐵 ) ) → ( 𝑈 ‘ ( I ↾ 𝐵 ) ) = ( I ↾ 𝐵 ) )
11 simpr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑈𝑂 ) ∧ 𝐹𝑇 ) ∧ 𝐹 = ( I ↾ 𝐵 ) ) → 𝐹 = ( I ↾ 𝐵 ) )
12 11 fveq2d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑈𝑂 ) ∧ 𝐹𝑇 ) ∧ 𝐹 = ( I ↾ 𝐵 ) ) → ( 𝑈𝐹 ) = ( 𝑈 ‘ ( I ↾ 𝐵 ) ) )
13 10 12 11 3eqtr4d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑈𝑂 ) ∧ 𝐹𝑇 ) ∧ 𝐹 = ( I ↾ 𝐵 ) ) → ( 𝑈𝐹 ) = 𝐹 )
14 13 fveq2d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑈𝑂 ) ∧ 𝐹𝑇 ) ∧ 𝐹 = ( I ↾ 𝐵 ) ) → ( 𝑅 ‘ ( 𝑈𝐹 ) ) = ( 𝑅𝐹 ) )
15 simpl1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑈𝑂 ) ∧ 𝐹𝑇 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
16 simpl2l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑈𝑂 ) ∧ 𝐹𝑇 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ) → 𝑈𝐸 )
17 simpl3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑈𝑂 ) ∧ 𝐹𝑇 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ) → 𝐹𝑇 )
18 eqid ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
19 18 2 3 4 5 tendotp ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸𝐹𝑇 ) → ( 𝑅 ‘ ( 𝑈𝐹 ) ) ( le ‘ 𝐾 ) ( 𝑅𝐹 ) )
20 15 16 17 19 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑈𝑂 ) ∧ 𝐹𝑇 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ) → ( 𝑅 ‘ ( 𝑈𝐹 ) ) ( le ‘ 𝐾 ) ( 𝑅𝐹 ) )
21 simpl1l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑈𝑂 ) ∧ 𝐹𝑇 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ) → 𝐾 ∈ HL )
22 hlatl ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
23 21 22 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑈𝑂 ) ∧ 𝐹𝑇 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ) → 𝐾 ∈ AtLat )
24 2 3 5 tendocl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸𝐹𝑇 ) → ( 𝑈𝐹 ) ∈ 𝑇 )
25 15 16 17 24 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑈𝑂 ) ∧ 𝐹𝑇 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ) → ( 𝑈𝐹 ) ∈ 𝑇 )
26 simpl2r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑈𝑂 ) ∧ 𝐹𝑇 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ) → 𝑈𝑂 )
27 simpr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑈𝑂 ) ∧ 𝐹𝑇 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ) → 𝐹 ≠ ( I ↾ 𝐵 ) )
28 1 2 3 5 6 tendoid0 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸 ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ) → ( ( 𝑈𝐹 ) = ( I ↾ 𝐵 ) ↔ 𝑈 = 𝑂 ) )
29 15 16 17 27 28 syl112anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑈𝑂 ) ∧ 𝐹𝑇 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ) → ( ( 𝑈𝐹 ) = ( I ↾ 𝐵 ) ↔ 𝑈 = 𝑂 ) )
30 29 necon3bid ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑈𝑂 ) ∧ 𝐹𝑇 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ) → ( ( 𝑈𝐹 ) ≠ ( I ↾ 𝐵 ) ↔ 𝑈𝑂 ) )
31 26 30 mpbird ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑈𝑂 ) ∧ 𝐹𝑇 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ) → ( 𝑈𝐹 ) ≠ ( I ↾ 𝐵 ) )
32 eqid ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
33 1 32 2 3 4 trlnidat ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐹 ) ∈ 𝑇 ∧ ( 𝑈𝐹 ) ≠ ( I ↾ 𝐵 ) ) → ( 𝑅 ‘ ( 𝑈𝐹 ) ) ∈ ( Atoms ‘ 𝐾 ) )
34 15 25 31 33 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑈𝑂 ) ∧ 𝐹𝑇 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ) → ( 𝑅 ‘ ( 𝑈𝐹 ) ) ∈ ( Atoms ‘ 𝐾 ) )
35 1 32 2 3 4 trlnidat ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) → ( 𝑅𝐹 ) ∈ ( Atoms ‘ 𝐾 ) )
36 15 17 27 35 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑈𝑂 ) ∧ 𝐹𝑇 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ) → ( 𝑅𝐹 ) ∈ ( Atoms ‘ 𝐾 ) )
37 18 32 atcmp ( ( 𝐾 ∈ AtLat ∧ ( 𝑅 ‘ ( 𝑈𝐹 ) ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑅 ‘ ( 𝑈𝐹 ) ) ( le ‘ 𝐾 ) ( 𝑅𝐹 ) ↔ ( 𝑅 ‘ ( 𝑈𝐹 ) ) = ( 𝑅𝐹 ) ) )
38 23 34 36 37 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑈𝑂 ) ∧ 𝐹𝑇 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ) → ( ( 𝑅 ‘ ( 𝑈𝐹 ) ) ( le ‘ 𝐾 ) ( 𝑅𝐹 ) ↔ ( 𝑅 ‘ ( 𝑈𝐹 ) ) = ( 𝑅𝐹 ) ) )
39 20 38 mpbid ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑈𝑂 ) ∧ 𝐹𝑇 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ) → ( 𝑅 ‘ ( 𝑈𝐹 ) ) = ( 𝑅𝐹 ) )
40 14 39 pm2.61dane ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑈𝑂 ) ∧ 𝐹𝑇 ) → ( 𝑅 ‘ ( 𝑈𝐹 ) ) = ( 𝑅𝐹 ) )