Metamath Proof Explorer

Theorem 3dimlem2

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

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

Proof

Step Hyp Ref Expression
1 3dim0.j ⊢ ∨ = ( join ‘ 𝐾 )
2 3dim0.l ⊢ ≤ = ( le ‘ 𝐾 )
3 3dim0.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 simp3l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑃 ≠ 𝑄 )
5 simp22 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) )
6 1 3 hlatjcom ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑄 ∨ 𝑃 ) )
7 6 3ad2ant1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑄 ∨ 𝑃 ) )
8 simp3r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) )
9 simp11 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝐾 ∈ HL )
10 simp12 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑃 ∈ 𝐴 )
11 simp21 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑅 ∈ 𝐴 )
12 simp13 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑄 ∈ 𝐴 )
13 2 1 3 hlatexchb1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → ( 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ↔ ( 𝑄 ∨ 𝑃 ) = ( 𝑄 ∨ 𝑅 ) ) )
14 9 10 11 12 4 13 syl131anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ↔ ( 𝑄 ∨ 𝑃 ) = ( 𝑄 ∨ 𝑅 ) ) )
15 8 14 mpbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( 𝑄 ∨ 𝑃 ) = ( 𝑄 ∨ 𝑅 ) )
16 7 15 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑄 ∨ 𝑅 ) )
17 16 breq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ↔ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) )
18 5 17 mtbird ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) )
19 simp23 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) )
20 16 oveq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) = ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) )
21 20 breq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ↔ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) )
22 19 21 mtbird ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ¬ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) )
23 4 18 22 3jca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑇 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑆 ) ) )