Metamath Proof Explorer

Theorem 3dimlem3

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

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

Proof

Step Hyp Ref Expression
1 3dim0.j ⊢ ∨ = ( join ‘ 𝐾 )
2 3dim0.l ⊢ ≤ = ( le ‘ 𝐾 )
3 3dim0.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 simpr1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → 𝑃 ≠ 𝑄 )
5 simpr2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) )
6 simpl11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → 𝐾 ∈ HL )
7 simpl2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → 𝑅 ∈ 𝐴 )
8 simpl12 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → 𝑃 ∈ 𝐴 )
9 simpl13 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → 𝑄 ∈ 𝐴 )
10 simpl3l ⊢ ( ( ( ( 𝐾 ∈ 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 5 17 mtod ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) )
19 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) )
20 simpl2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) )
21 simpl3r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) )
22 simpr3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) )
23 1 2 3 3dimlem3a ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → ¬ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
24 19 20 21 5 22 23 syl113anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → ¬ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
25 4 18 24 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )