This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem trljco

Description: Trace joined with trace of composition. (Contributed by NM, 15-Jun-2013)

Ref Expression
Hypotheses trljco.j ⊢ ∨ = ( join ‘ 𝐾 )
trljco.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
trljco.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
trljco.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
Assertion trljco ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) = ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 trljco.j ⊢ ∨ = ( join ‘ 𝐾 )
2 trljco.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 trljco.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4 trljco.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
5 coeq1 ⊢ ( 𝐹 = ( I ↾ ( Base ‘ 𝐾 ) ) → ( 𝐹 ∘ 𝐺 ) = ( ( I ↾ ( Base ‘ 𝐾 ) ) ∘ 𝐺 ) )
6 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
7 6 2 3 ltrn1o ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ) → 𝐺 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) )
8 7 3adant2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → 𝐺 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) )
9 f1of ⊢ ( 𝐺 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) → 𝐺 : ( Base ‘ 𝐾 ) ⟶ ( Base ‘ 𝐾 ) )
10 fcoi2 ⊢ ( 𝐺 : ( Base ‘ 𝐾 ) ⟶ ( Base ‘ 𝐾 ) → ( ( I ↾ ( Base ‘ 𝐾 ) ) ∘ 𝐺 ) = 𝐺 )
11 8 9 10 3syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ( I ↾ ( Base ‘ 𝐾 ) ) ∘ 𝐺 ) = 𝐺 )
12 5 11 sylan9eqr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝐹 = ( I ↾ ( Base ‘ 𝐾 ) ) ) → ( 𝐹 ∘ 𝐺 ) = 𝐺 )
13 12 fveq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝐹 = ( I ↾ ( Base ‘ 𝐾 ) ) ) → ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( 𝑅 ‘ 𝐺 ) )
14 13 oveq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝐹 = ( I ↾ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) = ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) )
15 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → 𝐾 ∈ HL )
16 15 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → 𝐾 ∈ Lat )
17 6 2 3 4 trlcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) )
18 17 3adant3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) )
19 6 1 latjidm ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐹 ) ) = ( 𝑅 ‘ 𝐹 ) )
20 16 18 19 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐹 ) ) = ( 𝑅 ‘ 𝐹 ) )
21 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
22 15 21 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → 𝐾 ∈ OL )
23 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
24 6 1 23 olj01 ⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 0. ‘ 𝐾 ) ) = ( 𝑅 ‘ 𝐹 ) )
25 22 18 24 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 0. ‘ 𝐾 ) ) = ( 𝑅 ‘ 𝐹 ) )
26 20 25 eqtr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐹 ) ) = ( ( 𝑅 ‘ 𝐹 ) ∨ ( 0. ‘ 𝐾 ) ) )
27 26 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝐺 = ( I ↾ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐹 ) ) = ( ( 𝑅 ‘ 𝐹 ) ∨ ( 0. ‘ 𝐾 ) ) )
28 coeq2 ⊢ ( 𝐺 = ( I ↾ ( Base ‘ 𝐾 ) ) → ( 𝐹 ∘ 𝐺 ) = ( 𝐹 ∘ ( I ↾ ( Base ‘ 𝐾 ) ) ) )
29 6 2 3 ltrn1o ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → 𝐹 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) )
30 29 3adant3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → 𝐹 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) )
31 f1of ⊢ ( 𝐹 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) → 𝐹 : ( Base ‘ 𝐾 ) ⟶ ( Base ‘ 𝐾 ) )
32 fcoi1 ⊢ ( 𝐹 : ( Base ‘ 𝐾 ) ⟶ ( Base ‘ 𝐾 ) → ( 𝐹 ∘ ( I ↾ ( Base ‘ 𝐾 ) ) ) = 𝐹 )
33 30 31 32 3syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝐹 ∘ ( I ↾ ( Base ‘ 𝐾 ) ) ) = 𝐹 )
34 28 33 sylan9eqr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝐺 = ( I ↾ ( Base ‘ 𝐾 ) ) ) → ( 𝐹 ∘ 𝐺 ) = 𝐹 )
35 34 fveq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝐺 = ( I ↾ ( Base ‘ 𝐾 ) ) ) → ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( 𝑅 ‘ 𝐹 ) )
36 35 oveq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝐺 = ( I ↾ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) = ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐹 ) ) )
37 6 23 2 3 4 trlid0b ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ) → ( 𝐺 = ( I ↾ ( Base ‘ 𝐾 ) ) ↔ ( 𝑅 ‘ 𝐺 ) = ( 0. ‘ 𝐾 ) ) )
38 37 3adant2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝐺 = ( I ↾ ( Base ‘ 𝐾 ) ) ↔ ( 𝑅 ‘ 𝐺 ) = ( 0. ‘ 𝐾 ) ) )
39 38 biimpa ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝐺 = ( I ↾ ( Base ‘ 𝐾 ) ) ) → ( 𝑅 ‘ 𝐺 ) = ( 0. ‘ 𝐾 ) )
40 39 oveq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝐺 = ( I ↾ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) = ( ( 𝑅 ‘ 𝐹 ) ∨ ( 0. ‘ 𝐾 ) ) )
41 27 36 40 3eqtr4d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝐺 = ( I ↾ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) = ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) )
42 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
43 16 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) → 𝐾 ∈ Lat )
44 simp1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
45 2 3 ltrnco ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝐹 ∘ 𝐺 ) ∈ 𝑇 )
46 6 2 3 4 trlcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∘ 𝐺 ) ∈ 𝑇 ) → ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ∈ ( Base ‘ 𝐾 ) )
47 44 45 46 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ∈ ( Base ‘ 𝐾 ) )
48 6 1 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) ∈ ( Base ‘ 𝐾 ) )
49 16 18 47 48 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) ∈ ( Base ‘ 𝐾 ) )
50 49 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) ∈ ( Base ‘ 𝐾 ) )
51 6 2 3 4 trlcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐺 ) ∈ ( Base ‘ 𝐾 ) )
52 51 3adant2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐺 ) ∈ ( Base ‘ 𝐾 ) )
53 6 1 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐺 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ∈ ( Base ‘ 𝐾 ) )
54 16 18 52 53 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ∈ ( Base ‘ 𝐾 ) )
55 54 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ∈ ( Base ‘ 𝐾 ) )
56 6 42 1 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐺 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝐹 ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) )
57 16 18 52 56 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐹 ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) )
58 42 1 2 3 4 trlco ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) )
59 6 42 1 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( 𝑅 ‘ 𝐹 ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) ↔ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) )
60 16 18 47 54 59 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ( ( 𝑅 ‘ 𝐹 ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) ↔ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) )
61 57 58 60 mpbi2and ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) )
62 61 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) )
63 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) → ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) )
64 63 oveq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐹 ) ) = ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) )
65 6 42 1 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝐹 ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) )
66 16 18 47 65 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐹 ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) )
67 20 66 eqbrtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐹 ) ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) )
68 67 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐹 ) ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) )
69 64 68 eqbrtrrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) )
70 6 42 43 50 55 62 69 latasymd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) = ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) )
71 61 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ 𝐺 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) )
72 simpl1l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ 𝐺 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝐾 ∈ HL )
73 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ 𝐺 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
74 simpl2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ 𝐺 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝐹 ∈ 𝑇 )
75 simpr1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ 𝐺 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝐹 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) )
76 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
77 6 76 2 3 4 trlnidat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ) → ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) )
78 73 74 75 77 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ 𝐺 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) )
79 simpl3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ 𝐺 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝐺 ∈ 𝑇 )
80 74 79 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ 𝐺 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) )
81 simpr3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ 𝐺 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) )
82 76 2 3 4 trlcoat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) → ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ∈ ( Atoms ‘ 𝐾 ) )
83 73 80 81 82 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ 𝐺 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ∈ ( Atoms ‘ 𝐾 ) )
84 simpr2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ 𝐺 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝐺 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) )
85 6 2 3 4 trlcone ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ) ) → ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) )
86 73 80 81 84 85 syl112anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ 𝐺 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) )
87 6 76 2 3 4 trlnidat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ) → ( 𝑅 ‘ 𝐺 ) ∈ ( Atoms ‘ 𝐾 ) )
88 73 79 84 87 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ 𝐺 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐺 ) ∈ ( Atoms ‘ 𝐾 ) )
89 42 1 76 ps-1 ⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐺 ) ∈ ( Atoms ‘ 𝐾 ) ) ) → ( ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ↔ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) = ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) )
90 72 78 83 86 78 88 89 syl132anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ 𝐺 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ↔ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) = ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) )
91 71 90 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ 𝐺 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) = ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) )
92 14 41 70 91 pm2.61da3ne ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) = ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) )