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 syl5bi ( 𝐾 ∈ HL → ( ¬ ( ( ( 𝑃 𝑄 ) 𝑅 ) ∈ 𝑂 ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑃 𝑄 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑄 𝑅 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑃 ) ) ) → ( ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) → ( ( ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ( 𝑃 𝑄 ) ( 𝑆 𝑇 ) ) ( ( ( 𝑄 𝑅 ) ( 𝑇 𝑈 ) ) ( ( 𝑅 𝑃 ) ( 𝑈 𝑆 ) ) ) ) ) ) )
15 14 3imp ( ( 𝐾 ∈ HL ∧ ¬ ( ( ( 𝑃 𝑄 ) 𝑅 ) ∈ 𝑂 ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑃 𝑄 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑄 𝑅 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑃 ) ) ) ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) → ( ( ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ( 𝑃 𝑄 ) ( 𝑆 𝑇 ) ) ( ( ( 𝑄 𝑅 ) ( 𝑇 𝑈 ) ) ( ( 𝑅 𝑃 ) ( 𝑈 𝑆 ) ) ) ) )
16 15 3impib ( ( ( 𝐾 ∈ HL ∧ ¬ ( ( ( 𝑃 𝑄 ) 𝑅 ) ∈ 𝑂 ∧ ( ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑃 𝑄 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑄 𝑅 ) ∧ ¬ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑃 ) ) ) ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ( 𝑃 𝑄 ) ( 𝑆 𝑇 ) ) ( ( ( 𝑄 𝑅 ) ( 𝑇 𝑈 ) ) ( ( 𝑅 𝑃 ) ( 𝑈 𝑆 ) ) ) )