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

Metamath Proof Explorer

Theorem dalawlem14

Description: Lemma for dalaw . Combine dalawlem10 and dalawlem13 . (Contributed by NM, 6-Oct-2012)

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

Proof

Step Hyp Ref Expression
1 dalawlem.l ⊢ ≤ = ( le ‘ 𝐾 )
2 dalawlem.j ⊢ ∨ = ( join ‘ 𝐾 )
3 dalawlem.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 dalawlem.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 dalawlem2.o ⊢ 𝑂 = ( LPlanes ‘ 𝐾 )
6 ianor ⊢ ( ¬ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑂 ∧ ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑃 ) ) ) ↔ ( ¬ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑂 ∨ ¬ ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑃 ) ) ) )
7 1 2 3 4 5 dalawlem13 ⊢ ( ( ( 𝐾 ∈ HL ∧ ¬ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( ( 𝑄 ∨ 𝑅 ) ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) )
8 7 3expib ⊢ ( ( 𝐾 ∈ HL ∧ ¬ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) → ( ( ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( ( 𝑄 ∨ 𝑅 ) ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) ) )
9 8 3exp ⊢ ( 𝐾 ∈ HL → ( ¬ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑂 → ( ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) → ( ( ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( ( 𝑄 ∨ 𝑅 ) ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) ) ) ) )
10 1 2 3 4 dalawlem10 ⊢ ( ( ( 𝐾 ∈ HL ∧ ¬ ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( ( 𝑄 ∨ 𝑅 ) ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) )
11 10 3expib ⊢ ( ( 𝐾 ∈ HL ∧ ¬ ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑃 ) ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) → ( ( ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( ( 𝑄 ∨ 𝑅 ) ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) ) )
12 11 3exp ⊢ ( 𝐾 ∈ HL → ( ¬ ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑃 ) ) → ( ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) → ( ( ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( ( 𝑄 ∨ 𝑅 ) ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) ) ) ) )
13 9 12 jaod ⊢ ( 𝐾 ∈ HL → ( ( ¬ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑂 ∨ ¬ ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑃 ) ) ) → ( ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) → ( ( ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( ( 𝑄 ∨ 𝑅 ) ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) ) ) ) )
14 6 13 biimtrid ⊢ ( 𝐾 ∈ HL → ( ¬ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑂 ∧ ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑃 ) ) ) → ( ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) → ( ( ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( ( 𝑄 ∨ 𝑅 ) ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) ) ) ) )
15 14 3imp ⊢ ( ( 𝐾 ∈ HL ∧ ¬ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑂 ∧ ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑃 ) ) ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) → ( ( ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( ( 𝑄 ∨ 𝑅 ) ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) ) )
16 15 3impib ⊢ ( ( ( 𝐾 ∈ HL ∧ ¬ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑂 ∧ ( ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑃 ) ) ) ∧ ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑄 ∨ 𝑇 ) ) ≤ ( 𝑅 ∨ 𝑈 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ≤ ( ( ( 𝑄 ∨ 𝑅 ) ∧ ( 𝑇 ∨ 𝑈 ) ) ∨ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑈 ∨ 𝑆 ) ) ) )