Metamath Proof Explorer

Theorem tendopltp

Description: Trace-preserving property of endomorphism sum operation P , based on theorem trlco . Part of remark in Crawley p. 118, 2nd line, "it is clear from the second part of G (our trlco ) that Delta is a subring of E." (In our development, we will bypass their E and go directly to their Delta, whose base set is our ( TEndoK )W .) (Contributed by NM, 9-Jun-2013)

Ref Expression
Hypotheses tendopl.h ⊢ H = LHyp ⁡ K
tendopl.t ⊢ T = LTrn ⁡ K ⁡ W
tendopl.e ⊢ E = TEndo ⁡ K ⁡ W
tendopl.p ⊢ P = s ∈ E , t ∈ E ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f
tendopltp.l ⊢ ≤ ˙ = ≤ K
tendopltp.r ⊢ R = trL ⁡ K ⁡ W
Assertion tendopltp ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ F ∈ T → R ⁡ U P V ⁡ F ≤ ˙ R ⁡ F

Proof

Step Hyp Ref Expression
1 tendopl.h ⊢ H = LHyp ⁡ K
2 tendopl.t ⊢ T = LTrn ⁡ K ⁡ W
3 tendopl.e ⊢ E = TEndo ⁡ K ⁡ W
4 tendopl.p ⊢ P = s ∈ E , t ∈ E ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f
5 tendopltp.l ⊢ ≤ ˙ = ≤ K
6 tendopltp.r ⊢ R = trL ⁡ K ⁡ W
7 eqid ⊢ Base K = Base K
8 simp1l ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ F ∈ T → K ∈ HL
9 8 hllatd ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ F ∈ T → K ∈ Lat
10 simp1 ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ F ∈ T → K ∈ HL ∧ W ∈ H
11 1 2 3 4 tendoplcl2 ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ F ∈ T → U P V ⁡ F ∈ T
12 7 1 2 6 trlcl ⊢ K ∈ HL ∧ W ∈ H ∧ U P V ⁡ F ∈ T → R ⁡ U P V ⁡ F ∈ Base K
13 10 11 12 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ F ∈ T → R ⁡ U P V ⁡ F ∈ Base K
14 1 2 3 tendocl ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ F ∈ T → U ⁡ F ∈ T
15 14 3adant2r ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ F ∈ T → U ⁡ F ∈ T
16 7 1 2 6 trlcl ⊢ K ∈ HL ∧ W ∈ H ∧ U ⁡ F ∈ T → R ⁡ U ⁡ F ∈ Base K
17 10 15 16 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ F ∈ T → R ⁡ U ⁡ F ∈ Base K
18 1 2 3 tendocl ⊢ K ∈ HL ∧ W ∈ H ∧ V ∈ E ∧ F ∈ T → V ⁡ F ∈ T
19 18 3adant2l ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ F ∈ T → V ⁡ F ∈ T
20 7 1 2 6 trlcl ⊢ K ∈ HL ∧ W ∈ H ∧ V ⁡ F ∈ T → R ⁡ V ⁡ F ∈ Base K
21 10 19 20 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ F ∈ T → R ⁡ V ⁡ F ∈ Base K
22 eqid ⊢ join ⁡ K = join ⁡ K
23 7 22 latjcl ⊢ K ∈ Lat ∧ R ⁡ U ⁡ F ∈ Base K ∧ R ⁡ V ⁡ F ∈ Base K → R ⁡ U ⁡ F join ⁡ K R ⁡ V ⁡ F ∈ Base K
24 9 17 21 23 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ F ∈ T → R ⁡ U ⁡ F join ⁡ K R ⁡ V ⁡ F ∈ Base K
25 simp3 ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ F ∈ T → F ∈ T
26 7 1 2 6 trlcl ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T → R ⁡ F ∈ Base K
27 10 25 26 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ F ∈ T → R ⁡ F ∈ Base K
28 simp2l ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ F ∈ T → U ∈ E
29 simp2r ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ F ∈ T → V ∈ E
30 4 2 tendopl2 ⊢ U ∈ E ∧ V ∈ E ∧ F ∈ T → U P V ⁡ F = U ⁡ F ∘ V ⁡ F
31 28 29 25 30 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ F ∈ T → U P V ⁡ F = U ⁡ F ∘ V ⁡ F
32 31 fveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ F ∈ T → R ⁡ U P V ⁡ F = R ⁡ U ⁡ F ∘ V ⁡ F
33 5 22 1 2 6 trlco ⊢ K ∈ HL ∧ W ∈ H ∧ U ⁡ F ∈ T ∧ V ⁡ F ∈ T → R ⁡ U ⁡ F ∘ V ⁡ F ≤ ˙ R ⁡ U ⁡ F join ⁡ K R ⁡ V ⁡ F
34 10 15 19 33 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ F ∈ T → R ⁡ U ⁡ F ∘ V ⁡ F ≤ ˙ R ⁡ U ⁡ F join ⁡ K R ⁡ V ⁡ F
35 32 34 eqbrtrd ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ F ∈ T → R ⁡ U P V ⁡ F ≤ ˙ R ⁡ U ⁡ F join ⁡ K R ⁡ V ⁡ F
36 5 1 2 6 3 tendotp ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ F ∈ T → R ⁡ U ⁡ F ≤ ˙ R ⁡ F
37 36 3adant2r ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ F ∈ T → R ⁡ U ⁡ F ≤ ˙ R ⁡ F
38 5 1 2 6 3 tendotp ⊢ K ∈ HL ∧ W ∈ H ∧ V ∈ E ∧ F ∈ T → R ⁡ V ⁡ F ≤ ˙ R ⁡ F
39 38 3adant2l ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ F ∈ T → R ⁡ V ⁡ F ≤ ˙ R ⁡ F
40 7 5 22 latjle12 ⊢ K ∈ Lat ∧ R ⁡ U ⁡ F ∈ Base K ∧ R ⁡ V ⁡ F ∈ Base K ∧ R ⁡ F ∈ Base K → R ⁡ U ⁡ F ≤ ˙ R ⁡ F ∧ R ⁡ V ⁡ F ≤ ˙ R ⁡ F ↔ R ⁡ U ⁡ F join ⁡ K R ⁡ V ⁡ F ≤ ˙ R ⁡ F
41 9 17 21 27 40 syl13anc ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ F ∈ T → R ⁡ U ⁡ F ≤ ˙ R ⁡ F ∧ R ⁡ V ⁡ F ≤ ˙ R ⁡ F ↔ R ⁡ U ⁡ F join ⁡ K R ⁡ V ⁡ F ≤ ˙ R ⁡ F
42 37 39 41 mpbi2and ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ F ∈ T → R ⁡ U ⁡ F join ⁡ K R ⁡ V ⁡ F ≤ ˙ R ⁡ F
43 7 5 9 13 24 27 35 42 lattrd ⊢ K ∈ HL ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ F ∈ T → R ⁡ U P V ⁡ F ≤ ˙ R ⁡ F