Metamath Proof Explorer


Theorem 3atlem1

Description: Lemma for 3at . (Contributed by NM, 22-Jun-2012)

Ref Expression
Hypotheses 3at.l = ( le ‘ 𝐾 )
3at.j = ( join ‘ 𝐾 )
3at.a 𝐴 = ( Atoms ‘ 𝐾 )
Assertion 3atlem1 ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( ( 𝑃 𝑄 ) 𝑅 ) = ( ( 𝑆 𝑇 ) 𝑈 ) )

Proof

Step Hyp Ref Expression
1 3at.l = ( le ‘ 𝐾 )
2 3at.j = ( join ‘ 𝐾 )
3 3at.a 𝐴 = ( Atoms ‘ 𝐾 )
4 simp11 ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → 𝐾 ∈ HL )
5 simp131 ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → 𝑆𝐴 )
6 simp132 ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → 𝑇𝐴 )
7 simp133 ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → 𝑈𝐴 )
8 2 3 hlatjass ( ( 𝐾 ∈ HL ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ( 𝑆 𝑇 ) 𝑈 ) = ( 𝑆 ( 𝑇 𝑈 ) ) )
9 4 5 6 7 8 syl13anc ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( ( 𝑆 𝑇 ) 𝑈 ) = ( 𝑆 ( 𝑇 𝑈 ) ) )
10 simp121 ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → 𝑃𝐴 )
11 simp122 ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → 𝑄𝐴 )
12 simp123 ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → 𝑅𝐴 )
13 2 3 hlatjass ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → ( ( 𝑃 𝑄 ) 𝑅 ) = ( 𝑃 ( 𝑄 𝑅 ) ) )
14 4 10 11 12 13 syl13anc ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( ( 𝑃 𝑄 ) 𝑅 ) = ( 𝑃 ( 𝑄 𝑅 ) ) )
15 simp3 ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) )
16 14 15 eqbrtrrd ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( 𝑃 ( 𝑄 𝑅 ) ) ( ( 𝑆 𝑇 ) 𝑈 ) )
17 4 hllatd ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → 𝐾 ∈ Lat )
18 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
19 18 3 atbase ( 𝑃𝐴𝑃 ∈ ( Base ‘ 𝐾 ) )
20 10 19 syl ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
21 18 2 3 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑄𝐴𝑅𝐴 ) → ( 𝑄 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
22 4 11 12 21 syl3anc ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( 𝑄 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
23 18 2 3 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴 ) → ( 𝑆 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
24 4 5 6 23 syl3anc ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( 𝑆 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
25 18 3 atbase ( 𝑈𝐴𝑈 ∈ ( Base ‘ 𝐾 ) )
26 7 25 syl ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → 𝑈 ∈ ( Base ‘ 𝐾 ) )
27 18 2 latjcl ( ( 𝐾 ∈ Lat ∧ ( 𝑆 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑆 𝑇 ) 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
28 17 24 26 27 syl3anc ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( ( 𝑆 𝑇 ) 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
29 18 1 2 latjle12 ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑆 𝑇 ) 𝑈 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑃 ( ( 𝑆 𝑇 ) 𝑈 ) ∧ ( 𝑄 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) ↔ ( 𝑃 ( 𝑄 𝑅 ) ) ( ( 𝑆 𝑇 ) 𝑈 ) ) )
30 17 20 22 28 29 syl13anc ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( ( 𝑃 ( ( 𝑆 𝑇 ) 𝑈 ) ∧ ( 𝑄 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) ↔ ( 𝑃 ( 𝑄 𝑅 ) ) ( ( 𝑆 𝑇 ) 𝑈 ) ) )
31 16 30 mpbird ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( 𝑃 ( ( 𝑆 𝑇 ) 𝑈 ) ∧ ( 𝑄 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) )
32 31 simpld ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → 𝑃 ( ( 𝑆 𝑇 ) 𝑈 ) )
33 32 9 breqtrd ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → 𝑃 ( 𝑆 ( 𝑇 𝑈 ) ) )
34 18 2 3 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑇𝐴𝑈𝐴 ) → ( 𝑇 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
35 4 6 7 34 syl3anc ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( 𝑇 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
36 simp22 ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ¬ 𝑃 ( 𝑇 𝑈 ) )
37 18 1 2 3 hlexchb2 ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑆𝐴 ∧ ( 𝑇 𝑈 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ) → ( 𝑃 ( 𝑆 ( 𝑇 𝑈 ) ) ↔ ( 𝑃 ( 𝑇 𝑈 ) ) = ( 𝑆 ( 𝑇 𝑈 ) ) ) )
38 4 10 5 35 36 37 syl131anc ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( 𝑃 ( 𝑆 ( 𝑇 𝑈 ) ) ↔ ( 𝑃 ( 𝑇 𝑈 ) ) = ( 𝑆 ( 𝑇 𝑈 ) ) ) )
39 33 38 mpbid ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( 𝑃 ( 𝑇 𝑈 ) ) = ( 𝑆 ( 𝑇 𝑈 ) ) )
40 2 3 hlatj12 ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑇𝐴𝑈𝐴 ) ) → ( 𝑃 ( 𝑇 𝑈 ) ) = ( 𝑇 ( 𝑃 𝑈 ) ) )
41 4 10 6 7 40 syl13anc ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( 𝑃 ( 𝑇 𝑈 ) ) = ( 𝑇 ( 𝑃 𝑈 ) ) )
42 9 39 41 3eqtr2d ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( ( 𝑆 𝑇 ) 𝑈 ) = ( 𝑇 ( 𝑃 𝑈 ) ) )
43 2 3 hlatj12 ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → ( 𝑃 ( 𝑄 𝑅 ) ) = ( 𝑄 ( 𝑃 𝑅 ) ) )
44 4 10 11 12 43 syl13anc ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( 𝑃 ( 𝑄 𝑅 ) ) = ( 𝑄 ( 𝑃 𝑅 ) ) )
45 16 44 42 3brtr3d ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( 𝑄 ( 𝑃 𝑅 ) ) ( 𝑇 ( 𝑃 𝑈 ) ) )
46 18 3 atbase ( 𝑄𝐴𝑄 ∈ ( Base ‘ 𝐾 ) )
47 11 46 syl ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
48 18 2 3 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑅𝐴 ) → ( 𝑃 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
49 4 10 12 48 syl3anc ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( 𝑃 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
50 18 3 atbase ( 𝑇𝐴𝑇 ∈ ( Base ‘ 𝐾 ) )
51 6 50 syl ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → 𝑇 ∈ ( Base ‘ 𝐾 ) )
52 18 2 3 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑈𝐴 ) → ( 𝑃 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
53 4 10 7 52 syl3anc ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( 𝑃 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
54 18 2 latjcl ( ( 𝐾 ∈ Lat ∧ 𝑇 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 𝑈 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑇 ( 𝑃 𝑈 ) ) ∈ ( Base ‘ 𝐾 ) )
55 17 51 53 54 syl3anc ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( 𝑇 ( 𝑃 𝑈 ) ) ∈ ( Base ‘ 𝐾 ) )
56 18 1 2 latjle12 ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑇 ( 𝑃 𝑈 ) ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑄 ( 𝑇 ( 𝑃 𝑈 ) ) ∧ ( 𝑃 𝑅 ) ( 𝑇 ( 𝑃 𝑈 ) ) ) ↔ ( 𝑄 ( 𝑃 𝑅 ) ) ( 𝑇 ( 𝑃 𝑈 ) ) ) )
57 17 47 49 55 56 syl13anc ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( ( 𝑄 ( 𝑇 ( 𝑃 𝑈 ) ) ∧ ( 𝑃 𝑅 ) ( 𝑇 ( 𝑃 𝑈 ) ) ) ↔ ( 𝑄 ( 𝑃 𝑅 ) ) ( 𝑇 ( 𝑃 𝑈 ) ) ) )
58 45 57 mpbird ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( 𝑄 ( 𝑇 ( 𝑃 𝑈 ) ) ∧ ( 𝑃 𝑅 ) ( 𝑇 ( 𝑃 𝑈 ) ) ) )
59 58 simpld ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → 𝑄 ( 𝑇 ( 𝑃 𝑈 ) ) )
60 simp23 ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ¬ 𝑄 ( 𝑃 𝑈 ) )
61 18 1 2 3 hlexchb2 ( ( 𝐾 ∈ HL ∧ ( 𝑄𝐴𝑇𝐴 ∧ ( 𝑃 𝑈 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) → ( 𝑄 ( 𝑇 ( 𝑃 𝑈 ) ) ↔ ( 𝑄 ( 𝑃 𝑈 ) ) = ( 𝑇 ( 𝑃 𝑈 ) ) ) )
62 4 11 6 53 60 61 syl131anc ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( 𝑄 ( 𝑇 ( 𝑃 𝑈 ) ) ↔ ( 𝑄 ( 𝑃 𝑈 ) ) = ( 𝑇 ( 𝑃 𝑈 ) ) ) )
63 59 62 mpbid ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( 𝑄 ( 𝑃 𝑈 ) ) = ( 𝑇 ( 𝑃 𝑈 ) ) )
64 18 2 latj13 ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑄 ( 𝑃 𝑈 ) ) = ( 𝑈 ( 𝑃 𝑄 ) ) )
65 17 47 20 26 64 syl13anc ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( 𝑄 ( 𝑃 𝑈 ) ) = ( 𝑈 ( 𝑃 𝑄 ) ) )
66 42 63 65 3eqtr2d ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( ( 𝑆 𝑇 ) 𝑈 ) = ( 𝑈 ( 𝑃 𝑄 ) ) )
67 18 2 3 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) → ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
68 4 10 11 67 syl3anc ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
69 18 3 atbase ( 𝑅𝐴𝑅 ∈ ( Base ‘ 𝐾 ) )
70 12 69 syl ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
71 18 1 2 latjle12 ( ( 𝐾 ∈ Lat ∧ ( ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑆 𝑇 ) 𝑈 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( 𝑃 𝑄 ) ( ( 𝑆 𝑇 ) 𝑈 ) ∧ 𝑅 ( ( 𝑆 𝑇 ) 𝑈 ) ) ↔ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) )
72 17 68 70 28 71 syl13anc ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( ( ( 𝑃 𝑄 ) ( ( 𝑆 𝑇 ) 𝑈 ) ∧ 𝑅 ( ( 𝑆 𝑇 ) 𝑈 ) ) ↔ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) )
73 15 72 mpbird ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( ( 𝑃 𝑄 ) ( ( 𝑆 𝑇 ) 𝑈 ) ∧ 𝑅 ( ( 𝑆 𝑇 ) 𝑈 ) ) )
74 73 simprd ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → 𝑅 ( ( 𝑆 𝑇 ) 𝑈 ) )
75 74 66 breqtrd ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → 𝑅 ( 𝑈 ( 𝑃 𝑄 ) ) )
76 simp21 ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ¬ 𝑅 ( 𝑃 𝑄 ) )
77 18 1 2 3 hlexchb2 ( ( 𝐾 ∈ HL ∧ ( 𝑅𝐴𝑈𝐴 ∧ ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) → ( 𝑅 ( 𝑈 ( 𝑃 𝑄 ) ) ↔ ( 𝑅 ( 𝑃 𝑄 ) ) = ( 𝑈 ( 𝑃 𝑄 ) ) ) )
78 4 12 7 68 76 77 syl131anc ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( 𝑅 ( 𝑈 ( 𝑃 𝑄 ) ) ↔ ( 𝑅 ( 𝑃 𝑄 ) ) = ( 𝑈 ( 𝑃 𝑄 ) ) ) )
79 75 78 mpbid ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( 𝑅 ( 𝑃 𝑄 ) ) = ( 𝑈 ( 𝑃 𝑄 ) ) )
80 18 2 latjcom ( ( 𝐾 ∈ Lat ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑅 ( 𝑃 𝑄 ) ) = ( ( 𝑃 𝑄 ) 𝑅 ) )
81 17 70 68 80 syl3anc ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( 𝑅 ( 𝑃 𝑄 ) ) = ( ( 𝑃 𝑄 ) 𝑅 ) )
82 66 79 81 3eqtr2rd ( ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) ∧ ( ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑃 ( 𝑇 𝑈 ) ∧ ¬ 𝑄 ( 𝑃 𝑈 ) ) ∧ ( ( 𝑃 𝑄 ) 𝑅 ) ( ( 𝑆 𝑇 ) 𝑈 ) ) → ( ( 𝑃 𝑄 ) 𝑅 ) = ( ( 𝑆 𝑇 ) 𝑈 ) )