Metamath Proof Explorer

Theorem cdleme9

Description: Part of proof of Lemma E in Crawley p. 113, 2nd paragraph on p. 114. C and F represent s_1 and f(s) respectively. In their notation, we prove f(s) \/ s_1 = q \/ s_1. (Contributed by NM, 10-Jun-2012)

Ref Expression
Hypotheses cdleme9.l ⊢ ≤ = ( le ‘ 𝐾 )
cdleme9.j ⊢ ∨ = ( join ‘ 𝐾 )
cdleme9.m ⊢ ∧ = ( meet ‘ 𝐾 )
cdleme9.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdleme9.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
cdleme9.u ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
cdleme9.f ⊢ 𝐹 = ( ( 𝑆 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ) )
cdleme9.c ⊢ 𝐶 = ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 )
Assertion cdleme9 ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝐹 ∨ 𝐶 ) = ( 𝑄 ∨ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 cdleme9.l ⊢ ≤ = ( le ‘ 𝐾 )
2 cdleme9.j ⊢ ∨ = ( join ‘ 𝐾 )
3 cdleme9.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 cdleme9.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 cdleme9.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 cdleme9.u ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
7 cdleme9.f ⊢ 𝐹 = ( ( 𝑆 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ) )
8 cdleme9.c ⊢ 𝐶 = ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 )
9 1 2 3 4 5 6 7 8 cdleme3d ⊢ 𝐹 = ( ( 𝑆 ∨ 𝑈 ) ∧ ( 𝑄 ∨ 𝐶 ) )
10 9 oveq1i ⊢ ( 𝐹 ∨ 𝐶 ) = ( ( ( 𝑆 ∨ 𝑈 ) ∧ ( 𝑄 ∨ 𝐶 ) ) ∨ 𝐶 )
11 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝐾 ∈ HL )
12 simp1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13 simp21 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
14 simp23l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑆 ∈ 𝐴 )
15 11 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝐾 ∈ Lat )
16 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
17 16 4 atbase ⊢ ( 𝑆 ∈ 𝐴 → 𝑆 ∈ ( Base ‘ 𝐾 ) )
18 14 17 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑆 ∈ ( Base ‘ 𝐾 ) )
19 simp21l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑃 ∈ 𝐴 )
20 16 4 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
21 19 20 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
22 simp22 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑄 ∈ 𝐴 )
23 16 4 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
24 22 23 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
25 simp3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) )
26 16 1 2 latnlej1l ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑆 ≠ 𝑃 )
27 26 necomd ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑃 ≠ 𝑆 )
28 15 18 21 24 25 27 syl131anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑃 ≠ 𝑆 )
29 1 2 3 4 5 8 cdleme9a ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑆 ) ) → 𝐶 ∈ 𝐴 )
30 12 13 14 28 29 syl112anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝐶 ∈ 𝐴 )
31 1 2 3 4 5 6 16 cdleme0aa ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → 𝑈 ∈ ( Base ‘ 𝐾 ) )
32 12 19 22 31 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑈 ∈ ( Base ‘ 𝐾 ) )
33 16 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑆 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
34 15 18 32 33 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑆 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
35 16 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) → ( 𝑄 ∨ 𝐶 ) ∈ ( Base ‘ 𝐾 ) )
36 11 22 30 35 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑄 ∨ 𝐶 ) ∈ ( Base ‘ 𝐾 ) )
37 1 2 4 hlatlej2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) → 𝐶 ≤ ( 𝑄 ∨ 𝐶 ) )
38 11 22 30 37 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝐶 ≤ ( 𝑄 ∨ 𝐶 ) )
39 16 1 2 3 4 atmod4i1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝐶 ∈ 𝐴 ∧ ( 𝑆 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ 𝐶 ) ∈ ( Base ‘ 𝐾 ) ) ∧ 𝐶 ≤ ( 𝑄 ∨ 𝐶 ) ) → ( ( ( 𝑆 ∨ 𝑈 ) ∧ ( 𝑄 ∨ 𝐶 ) ) ∨ 𝐶 ) = ( ( ( 𝑆 ∨ 𝑈 ) ∨ 𝐶 ) ∧ ( 𝑄 ∨ 𝐶 ) ) )
40 11 30 34 36 38 39 syl131anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( ( 𝑆 ∨ 𝑈 ) ∧ ( 𝑄 ∨ 𝐶 ) ) ∨ 𝐶 ) = ( ( ( 𝑆 ∨ 𝑈 ) ∨ 𝐶 ) ∧ ( 𝑄 ∨ 𝐶 ) ) )
41 8 oveq2i ⊢ ( 𝑆 ∨ 𝐶 ) = ( 𝑆 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) )
42 16 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
43 11 19 14 42 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
44 simp1r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑊 ∈ 𝐻 )
45 16 5 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
46 44 45 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
47 1 2 4 hlatlej2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → 𝑆 ≤ ( 𝑃 ∨ 𝑆 ) )
48 11 19 14 47 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑆 ≤ ( 𝑃 ∨ 𝑆 ) )
49 16 1 2 3 4 atmod3i1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑆 ) ) → ( 𝑆 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ) = ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑆 ∨ 𝑊 ) ) )
50 11 14 43 46 48 49 syl131anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑆 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ) = ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑆 ∨ 𝑊 ) ) )
51 simp23r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ¬ 𝑆 ≤ 𝑊 )
52 eqid ⊢ ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
53 1 2 52 4 5 lhpjat2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ( 𝑆 ∨ 𝑊 ) = ( 1. ‘ 𝐾 ) )
54 12 14 51 53 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑆 ∨ 𝑊 ) = ( 1. ‘ 𝐾 ) )
55 54 oveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑆 ∨ 𝑊 ) ) = ( ( 𝑃 ∨ 𝑆 ) ∧ ( 1. ‘ 𝐾 ) ) )
56 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
57 11 56 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝐾 ∈ OL )
58 16 3 52 olm11 ⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑆 ) ∧ ( 1. ‘ 𝐾 ) ) = ( 𝑃 ∨ 𝑆 ) )
59 57 43 58 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( 𝑃 ∨ 𝑆 ) ∧ ( 1. ‘ 𝐾 ) ) = ( 𝑃 ∨ 𝑆 ) )
60 50 55 59 3eqtrrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑃 ∨ 𝑆 ) = ( 𝑆 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ) )
61 41 60 eqtr4id ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑆 ∨ 𝐶 ) = ( 𝑃 ∨ 𝑆 ) )
62 61 oveq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( 𝑆 ∨ 𝐶 ) ∨ 𝑈 ) = ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑈 ) )
63 16 4 atbase ⊢ ( 𝐶 ∈ 𝐴 → 𝐶 ∈ ( Base ‘ 𝐾 ) )
64 30 63 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝐶 ∈ ( Base ‘ 𝐾 ) )
65 16 2 latj32 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ 𝐶 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑆 ∨ 𝑈 ) ∨ 𝐶 ) = ( ( 𝑆 ∨ 𝐶 ) ∨ 𝑈 ) )
66 15 18 32 64 65 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( 𝑆 ∨ 𝑈 ) ∨ 𝐶 ) = ( ( 𝑆 ∨ 𝐶 ) ∨ 𝑈 ) )
67 2 4 hlatj32 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑄 ) = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) )
68 11 19 14 22 67 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑄 ) = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) )
69 16 2 latjcom ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑄 ) )
70 15 24 43 69 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑄 ) )
71 6 oveq2i ⊢ ( 𝑃 ∨ 𝑈 ) = ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) )
72 16 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
73 11 19 22 72 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
74 1 2 4 hlatlej1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → 𝑃 ≤ ( 𝑃 ∨ 𝑄 ) )
75 11 19 22 74 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑃 ≤ ( 𝑃 ∨ 𝑄 ) )
76 16 1 2 3 4 atmod3i1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑃 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑃 ∨ 𝑊 ) ) )
77 11 19 73 46 75 76 syl131anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑃 ∨ 𝑊 ) ) )
78 1 2 52 4 5 lhpjat2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑃 ∨ 𝑊 ) = ( 1. ‘ 𝐾 ) )
79 12 13 78 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑃 ∨ 𝑊 ) = ( 1. ‘ 𝐾 ) )
80 79 oveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑃 ∨ 𝑊 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 1. ‘ 𝐾 ) ) )
81 16 3 52 olm11 ⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 1. ‘ 𝐾 ) ) = ( 𝑃 ∨ 𝑄 ) )
82 57 73 81 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 1. ‘ 𝐾 ) ) = ( 𝑃 ∨ 𝑄 ) )
83 77 80 82 3eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) = ( 𝑃 ∨ 𝑄 ) )
84 71 83 syl5eq ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑃 ∨ 𝑈 ) = ( 𝑃 ∨ 𝑄 ) )
85 84 oveq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( 𝑃 ∨ 𝑈 ) ∨ 𝑆 ) = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) )
86 68 70 85 3eqtr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑈 ) ∨ 𝑆 ) )
87 16 2 latj32 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑃 ∨ 𝑈 ) ∨ 𝑆 ) = ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑈 ) )
88 15 21 32 18 87 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( 𝑃 ∨ 𝑈 ) ∨ 𝑆 ) = ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑈 ) )
89 86 88 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑆 ) ∨ 𝑈 ) )
90 62 66 89 3eqtr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( 𝑆 ∨ 𝑈 ) ∨ 𝐶 ) = ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) )
91 90 oveq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( ( 𝑆 ∨ 𝑈 ) ∨ 𝐶 ) ∧ ( 𝑄 ∨ 𝐶 ) ) = ( ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) ∧ ( 𝑄 ∨ 𝐶 ) ) )
92 16 1 3 latmle1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ≤ ( 𝑃 ∨ 𝑆 ) )
93 15 43 46 92 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ≤ ( 𝑃 ∨ 𝑆 ) )
94 8 93 eqbrtrid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝐶 ≤ ( 𝑃 ∨ 𝑆 ) )
95 16 1 2 latjlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐶 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝐶 ≤ ( 𝑃 ∨ 𝑆 ) → ( 𝑄 ∨ 𝐶 ) ≤ ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) ) )
96 15 64 43 24 95 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝐶 ≤ ( 𝑃 ∨ 𝑆 ) → ( 𝑄 ∨ 𝐶 ) ≤ ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) ) )
97 94 96 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑄 ∨ 𝐶 ) ≤ ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) )
98 16 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) )
99 15 24 43 98 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) )
100 16 1 3 latleeqm2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∨ 𝐶 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑄 ∨ 𝐶 ) ≤ ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) ↔ ( ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) ∧ ( 𝑄 ∨ 𝐶 ) ) = ( 𝑄 ∨ 𝐶 ) ) )
101 15 36 99 100 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( 𝑄 ∨ 𝐶 ) ≤ ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) ↔ ( ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) ∧ ( 𝑄 ∨ 𝐶 ) ) = ( 𝑄 ∨ 𝐶 ) ) )
102 97 101 mpbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( 𝑄 ∨ ( 𝑃 ∨ 𝑆 ) ) ∧ ( 𝑄 ∨ 𝐶 ) ) = ( 𝑄 ∨ 𝐶 ) )
103 40 91 102 3eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( ( 𝑆 ∨ 𝑈 ) ∧ ( 𝑄 ∨ 𝐶 ) ) ∨ 𝐶 ) = ( 𝑄 ∨ 𝐶 ) )
104 10 103 syl5eq ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝐹 ∨ 𝐶 ) = ( 𝑄 ∨ 𝐶 ) )