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 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑈 ≠ 𝑂 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ ( 𝑈 ‘ 𝐹 ) ) = ( 𝑅 ‘ 𝐹 ) )