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

Metamath Proof Explorer

Theorem dalawlem2

Description: Lemma for dalaw . Utility lemma that breaks ( ( P .\/ Q ) ./\ ( S .\/ T ) ) into a join of two pieces. (Contributed by NM, 6-Oct-2012)

Ref Expression
Hypotheses dalawlem.l ⊢ ≤ = ( le ‘ 𝐾 )
dalawlem.j ⊢ ∨ = ( join ‘ 𝐾 )
dalawlem.m ⊢ ∧ = ( meet ‘ 𝐾 )
dalawlem.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion dalawlem2 ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ 𝑆 ) ∨ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ 𝑇 ) ) )

Proof

Step Hyp Ref Expression
1 dalawlem.l ⊢ ≤ = ( le ‘ 𝐾 )
2 dalawlem.j ⊢ ∨ = ( join ‘ 𝐾 )
3 dalawlem.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 dalawlem.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 simp1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → 𝐾 ∈ HL )
6 5 hllatd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → 𝐾 ∈ Lat )
7 simp2l ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → 𝑃 ∈ 𝐴 )
8 simp2r ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → 𝑄 ∈ 𝐴 )
9 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
10 9 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
11 5 7 8 10 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
12 simp3r ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → 𝑇 ∈ 𝐴 )
13 9 4 atbase ⊢ ( 𝑇 ∈ 𝐴 → 𝑇 ∈ ( Base ‘ 𝐾 ) )
14 12 13 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → 𝑇 ∈ ( Base ‘ 𝐾 ) )
15 9 1 2 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑇 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ∨ 𝑄 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) )
16 6 11 14 15 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( 𝑃 ∨ 𝑄 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) )
17 simp3l ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → 𝑆 ∈ 𝐴 )
18 9 4 atbase ⊢ ( 𝑆 ∈ 𝐴 → 𝑆 ∈ ( Base ‘ 𝐾 ) )
19 17 18 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → 𝑆 ∈ ( Base ‘ 𝐾 ) )
20 9 1 2 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ∨ 𝑄 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) )
21 6 11 19 20 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( 𝑃 ∨ 𝑄 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) )
22 9 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑇 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
23 6 11 14 22 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
24 9 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
25 6 11 19 24 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
26 9 1 3 latlem12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ ( 𝑃 ∨ 𝑄 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ) ↔ ( 𝑃 ∨ 𝑄 ) ≤ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ) ) )
27 6 11 23 25 26 syl13anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ ( 𝑃 ∨ 𝑄 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ) ↔ ( 𝑃 ∨ 𝑄 ) ≤ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ) ) )
28 16 21 27 mpbi2and ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( 𝑃 ∨ 𝑄 ) ≤ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ) )
29 9 3 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) )
30 6 23 25 29 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) )
31 9 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) → ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
32 5 17 12 31 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
33 9 1 3 latmlem1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ≤ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ) ∧ ( 𝑆 ∨ 𝑇 ) ) ) )
34 6 11 30 32 33 syl13anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ≤ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ) ∧ ( 𝑆 ∨ 𝑇 ) ) ) )
35 28 34 mpd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ) ∧ ( 𝑆 ∨ 𝑇 ) ) )
36 9 1 2 latlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) → 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) )
37 6 11 19 36 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) )
38 9 1 2 3 4 atmod3i1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑇 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ) → ( 𝑆 ∨ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ 𝑇 ) ) = ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ ( 𝑆 ∨ 𝑇 ) ) )
39 5 17 25 14 37 38 syl131anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( 𝑆 ∨ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ 𝑇 ) ) = ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ ( 𝑆 ∨ 𝑇 ) ) )
40 39 oveq2d ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ ( 𝑆 ∨ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ 𝑇 ) ) ) = ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ) )
41 9 3 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑇 ∈ ( Base ‘ 𝐾 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
42 6 25 14 41 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ 𝑇 ) ∈ ( Base ‘ 𝐾 ) )
43 9 1 2 3 latmlej22 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑇 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ 𝑇 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) )
44 6 14 25 11 43 syl13anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ 𝑇 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) )
45 9 1 2 3 4 atmod2i2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ 𝑇 ) ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ 𝑆 ) ∨ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ 𝑇 ) ) = ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ ( 𝑆 ∨ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ 𝑇 ) ) ) )
46 5 17 23 42 44 45 syl131anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ 𝑆 ) ∨ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ 𝑇 ) ) = ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ ( 𝑆 ∨ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ 𝑇 ) ) ) )
47 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
48 5 47 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → 𝐾 ∈ OL )
49 9 3 latmassOLD ⊢ ( ( 𝐾 ∈ OL ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑆 ∨ 𝑇 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ) ∧ ( 𝑆 ∨ 𝑇 ) ) = ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ) )
50 48 23 25 32 49 syl13anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ) ∧ ( 𝑆 ∨ 𝑇 ) ) = ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ) )
51 40 46 50 3eqtr4rd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ) ∧ ( 𝑆 ∨ 𝑇 ) ) = ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ 𝑆 ) ∨ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ 𝑇 ) ) )
52 35 51 breqtrd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑇 ) ∧ 𝑆 ) ∨ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ∧ 𝑇 ) ) )