Metamath Proof Explorer

Theorem tendopltp

Description: Trace-preserving property of endomorphism sum operation P , based on Theorems 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 ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
tendopl.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
tendopl.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
tendopl.p ⊢ 𝑃 = ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) )
tendopltp.l ⊢ ≤ = ( le ‘ 𝐾 )
tendopltp.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
Assertion tendopltp ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ ( ( 𝑈 𝑃 𝑉 ) ‘ 𝐹 ) ) ≤ ( 𝑅 ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 tendopl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 tendopl.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 tendopl.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
4 tendopl.p ⊢ 𝑃 = ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) )
5 tendopltp.l ⊢ ≤ = ( le ‘ 𝐾 )
6 tendopltp.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
7 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
8 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ 𝐹 ∈ 𝑇 ) → 𝐾 ∈ HL )
9 8 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ 𝐹 ∈ 𝑇 ) → 𝐾 ∈ Lat )
10 simp1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
11 1 2 3 4 tendoplcl2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑈 𝑃 𝑉 ) ‘ 𝐹 ) ∈ 𝑇 )
12 7 1 2 6 trlcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑈 𝑃 𝑉 ) ‘ 𝐹 ) ∈ 𝑇 ) → ( 𝑅 ‘ ( ( 𝑈 𝑃 𝑉 ) ‘ 𝐹 ) ) ∈ ( Base ‘ 𝐾 ) )
13 10 11 12 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ ( ( 𝑈 𝑃 𝑉 ) ‘ 𝐹 ) ) ∈ ( Base ‘ 𝐾 ) )
14 1 2 3 tendocl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( 𝑈 ‘ 𝐹 ) ∈ 𝑇 )
15 14 3adant2r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑈 ‘ 𝐹 ) ∈ 𝑇 )
16 7 1 2 6 trlcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ‘ 𝐹 ) ∈ 𝑇 ) → ( 𝑅 ‘ ( 𝑈 ‘ 𝐹 ) ) ∈ ( Base ‘ 𝐾 ) )
17 10 15 16 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ ( 𝑈 ‘ 𝐹 ) ) ∈ ( Base ‘ 𝐾 ) )
18 1 2 3 tendocl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑉 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( 𝑉 ‘ 𝐹 ) ∈ 𝑇 )
19 18 3adant2l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑉 ‘ 𝐹 ) ∈ 𝑇 )
20 7 1 2 6 trlcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑉 ‘ 𝐹 ) ∈ 𝑇 ) → ( 𝑅 ‘ ( 𝑉 ‘ 𝐹 ) ) ∈ ( Base ‘ 𝐾 ) )
21 10 19 20 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ ( 𝑉 ‘ 𝐹 ) ) ∈ ( Base ‘ 𝐾 ) )
22 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
23 7 22 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ‘ ( 𝑈 ‘ 𝐹 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅 ‘ ( 𝑉 ‘ 𝐹 ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑅 ‘ ( 𝑈 ‘ 𝐹 ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑉 ‘ 𝐹 ) ) ) ∈ ( Base ‘ 𝐾 ) )
24 9 17 21 23 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑅 ‘ ( 𝑈 ‘ 𝐹 ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑉 ‘ 𝐹 ) ) ) ∈ ( Base ‘ 𝐾 ) )
25 simp3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ 𝐹 ∈ 𝑇 ) → 𝐹 ∈ 𝑇 )
26 7 1 2 6 trlcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) )
27 10 25 26 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) )
28 simp2l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ 𝐹 ∈ 𝑇 ) → 𝑈 ∈ 𝐸 )
29 simp2r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ 𝐹 ∈ 𝑇 ) → 𝑉 ∈ 𝐸 )
30 4 2 tendopl2 ⊢ ( ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑈 𝑃 𝑉 ) ‘ 𝐹 ) = ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑉 ‘ 𝐹 ) ) )
31 28 29 25 30 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑈 𝑃 𝑉 ) ‘ 𝐹 ) = ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑉 ‘ 𝐹 ) ) )
32 31 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ ( ( 𝑈 𝑃 𝑉 ) ‘ 𝐹 ) ) = ( 𝑅 ‘ ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑉 ‘ 𝐹 ) ) ) )
33 5 22 1 2 6 trlco ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ‘ 𝐹 ) ∈ 𝑇 ∧ ( 𝑉 ‘ 𝐹 ) ∈ 𝑇 ) → ( 𝑅 ‘ ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑉 ‘ 𝐹 ) ) ) ≤ ( ( 𝑅 ‘ ( 𝑈 ‘ 𝐹 ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑉 ‘ 𝐹 ) ) ) )
34 10 15 19 33 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑉 ‘ 𝐹 ) ) ) ≤ ( ( 𝑅 ‘ ( 𝑈 ‘ 𝐹 ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑉 ‘ 𝐹 ) ) ) )
35 32 34 eqbrtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ ( ( 𝑈 𝑃 𝑉 ) ‘ 𝐹 ) ) ≤ ( ( 𝑅 ‘ ( 𝑈 ‘ 𝐹 ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑉 ‘ 𝐹 ) ) ) )
36 5 1 2 6 3 tendotp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ ( 𝑈 ‘ 𝐹 ) ) ≤ ( 𝑅 ‘ 𝐹 ) )
37 36 3adant2r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ ( 𝑈 ‘ 𝐹 ) ) ≤ ( 𝑅 ‘ 𝐹 ) )
38 5 1 2 6 3 tendotp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑉 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ ( 𝑉 ‘ 𝐹 ) ) ≤ ( 𝑅 ‘ 𝐹 ) )
39 38 3adant2l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ ( 𝑉 ‘ 𝐹 ) ) ≤ ( 𝑅 ‘ 𝐹 ) )
40 7 5 22 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑅 ‘ ( 𝑈 ‘ 𝐹 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅 ‘ ( 𝑉 ‘ 𝐹 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( 𝑅 ‘ ( 𝑈 ‘ 𝐹 ) ) ≤ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ ( 𝑉 ‘ 𝐹 ) ) ≤ ( 𝑅 ‘ 𝐹 ) ) ↔ ( ( 𝑅 ‘ ( 𝑈 ‘ 𝐹 ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑉 ‘ 𝐹 ) ) ) ≤ ( 𝑅 ‘ 𝐹 ) ) )
41 9 17 21 27 40 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( ( 𝑅 ‘ ( 𝑈 ‘ 𝐹 ) ) ≤ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝑅 ‘ ( 𝑉 ‘ 𝐹 ) ) ≤ ( 𝑅 ‘ 𝐹 ) ) ↔ ( ( 𝑅 ‘ ( 𝑈 ‘ 𝐹 ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑉 ‘ 𝐹 ) ) ) ≤ ( 𝑅 ‘ 𝐹 ) ) )
42 37 39 41 mpbi2and ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑅 ‘ ( 𝑈 ‘ 𝐹 ) ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝑉 ‘ 𝐹 ) ) ) ≤ ( 𝑅 ‘ 𝐹 ) )
43 7 5 9 13 24 27 35 42 lattrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ ( ( 𝑈 𝑃 𝑉 ) ‘ 𝐹 ) ) ≤ ( 𝑅 ‘ 𝐹 ) )