Metamath Proof Explorer

Theorem 3dimlem4

Description: Lemma for 3dim1 . (Contributed by NM, 25-Jul-2012)

Ref Expression
Hypotheses 3dim0.j ⊢ ∨ = ( join ‘ 𝐾 )
3dim0.l ⊢ ≤ = ( le ‘ 𝐾 )
3dim0.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion 3dimlem4 ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) → ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 3dim0.j ⊢ ∨ = ( join ‘ 𝐾 )
2 3dim0.l ⊢ ≤ = ( le ‘ 𝐾 )
3 3dim0.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 simp2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) → 𝑃 ≠ 𝑄 )
5 simp2r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) → ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) )
6 simp11 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝐾 ∈ HL )
7 simp2l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑅 ∈ 𝐴 )
8 simp12 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑃 ∈ 𝐴 )
9 simp13 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑄 ∈ 𝐴 )
10 simp3l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑄 ≠ 𝑅 )
11 10 necomd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑅 ≠ 𝑄 )
12 2 1 3 hlatexch2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑅 ≠ 𝑄 ) → ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) → 𝑃 ≤ ( 𝑅 ∨ 𝑄 ) ) )
13 6 7 8 9 11 12 syl131anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) → 𝑃 ≤ ( 𝑅 ∨ 𝑄 ) ) )
14 1 3 hlatjcom ⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( 𝑄 ∨ 𝑅 ) = ( 𝑅 ∨ 𝑄 ) )
15 6 9 7 14 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( 𝑄 ∨ 𝑅 ) = ( 𝑅 ∨ 𝑄 ) )
16 15 breq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ↔ 𝑃 ≤ ( 𝑅 ∨ 𝑄 ) ) )
17 13 16 sylibrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) → 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) )
18 17 3ad2ant1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) → ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) → 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) )
19 5 18 mtod ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) → ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) )
20 simp11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) → ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) )
21 simp12 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) → ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) )
22 simp13r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) → ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) )
23 simp3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) → ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) )
24 1 2 3 3dimlem4a ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
25 20 21 22 5 23 24 syl113anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) → ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
26 4 19 25 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) → ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )