Metamath Proof Explorer


Theorem dalawlem13

Description: Lemma for dalaw . Special case to eliminate the requirement ( ( P .\/ Q ) .\/ R ) e. O in dalawlem1 . (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 dalawlem13 ( ( ( 𝐾 ∈ 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 simp11 ( ( ( 𝐾 ∈ HL ∧ ¬ ( ( 𝑃 𝑄 ) 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → 𝐾 ∈ HL )
7 simp12 ( ( ( 𝐾 ∈ HL ∧ ¬ ( ( 𝑃 𝑄 ) 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ¬ ( ( 𝑃 𝑄 ) 𝑅 ) ∈ 𝑂 )
8 simp22 ( ( ( 𝐾 ∈ HL ∧ ¬ ( ( 𝑃 𝑄 ) 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → 𝑄𝐴 )
9 simp23 ( ( ( 𝐾 ∈ HL ∧ ¬ ( ( 𝑃 𝑄 ) 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → 𝑅𝐴 )
10 simp21 ( ( ( 𝐾 ∈ HL ∧ ¬ ( ( 𝑃 𝑄 ) 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → 𝑃𝐴 )
11 1 2 4 5 islpln2a ( ( 𝐾 ∈ HL ∧ ( 𝑄𝐴𝑅𝐴𝑃𝐴 ) ) → ( ( ( 𝑄 𝑅 ) 𝑃 ) ∈ 𝑂 ↔ ( 𝑄𝑅 ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ) ) )
12 6 8 9 10 11 syl13anc ( ( ( 𝐾 ∈ HL ∧ ¬ ( ( 𝑃 𝑄 ) 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ( ( 𝑄 𝑅 ) 𝑃 ) ∈ 𝑂 ↔ ( 𝑄𝑅 ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ) ) )
13 df-ne ( 𝑄𝑅 ↔ ¬ 𝑄 = 𝑅 )
14 13 anbi1i ( ( 𝑄𝑅 ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ) ↔ ( ¬ 𝑄 = 𝑅 ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ) )
15 pm4.56 ( ( ¬ 𝑄 = 𝑅 ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ) ↔ ¬ ( 𝑄 = 𝑅𝑃 ( 𝑄 𝑅 ) ) )
16 14 15 bitri ( ( 𝑄𝑅 ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ) ↔ ¬ ( 𝑄 = 𝑅𝑃 ( 𝑄 𝑅 ) ) )
17 12 16 bitr2di ( ( ( 𝐾 ∈ HL ∧ ¬ ( ( 𝑃 𝑄 ) 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ¬ ( 𝑄 = 𝑅𝑃 ( 𝑄 𝑅 ) ) ↔ ( ( 𝑄 𝑅 ) 𝑃 ) ∈ 𝑂 ) )
18 2 4 hlatjrot ( ( 𝐾 ∈ HL ∧ ( 𝑄𝐴𝑅𝐴𝑃𝐴 ) ) → ( ( 𝑄 𝑅 ) 𝑃 ) = ( ( 𝑃 𝑄 ) 𝑅 ) )
19 6 8 9 10 18 syl13anc ( ( ( 𝐾 ∈ HL ∧ ¬ ( ( 𝑃 𝑄 ) 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ( 𝑄 𝑅 ) 𝑃 ) = ( ( 𝑃 𝑄 ) 𝑅 ) )
20 19 eleq1d ( ( ( 𝐾 ∈ HL ∧ ¬ ( ( 𝑃 𝑄 ) 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ( ( 𝑄 𝑅 ) 𝑃 ) ∈ 𝑂 ↔ ( ( 𝑃 𝑄 ) 𝑅 ) ∈ 𝑂 ) )
21 17 20 bitrd ( ( ( 𝐾 ∈ HL ∧ ¬ ( ( 𝑃 𝑄 ) 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ¬ ( 𝑄 = 𝑅𝑃 ( 𝑄 𝑅 ) ) ↔ ( ( 𝑃 𝑄 ) 𝑅 ) ∈ 𝑂 ) )
22 21 con1bid ( ( ( 𝐾 ∈ HL ∧ ¬ ( ( 𝑃 𝑄 ) 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ¬ ( ( 𝑃 𝑄 ) 𝑅 ) ∈ 𝑂 ↔ ( 𝑄 = 𝑅𝑃 ( 𝑄 𝑅 ) ) ) )
23 7 22 mpbid ( ( ( 𝐾 ∈ HL ∧ ¬ ( ( 𝑃 𝑄 ) 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( 𝑄 = 𝑅𝑃 ( 𝑄 𝑅 ) ) )
24 simp13 ( ( ( 𝐾 ∈ HL ∧ ¬ ( ( 𝑃 𝑄 ) 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) )
25 simp2 ( ( ( 𝐾 ∈ HL ∧ ¬ ( ( 𝑃 𝑄 ) 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) )
26 simp3 ( ( ( 𝐾 ∈ HL ∧ ¬ ( ( 𝑃 𝑄 ) 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) )
27 1 2 3 4 dalawlem12 ( ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ( 𝑃 𝑄 ) ( 𝑆 𝑇 ) ) ( ( ( 𝑄 𝑅 ) ( 𝑇 𝑈 ) ) ( ( 𝑅 𝑃 ) ( 𝑈 𝑆 ) ) ) )
28 27 3expib ( ( 𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) → ( ( ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ( 𝑃 𝑄 ) ( 𝑆 𝑇 ) ) ( ( ( 𝑄 𝑅 ) ( 𝑇 𝑈 ) ) ( ( 𝑅 𝑃 ) ( 𝑈 𝑆 ) ) ) ) )
29 28 3exp ( 𝐾 ∈ HL → ( 𝑄 = 𝑅 → ( ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) → ( ( ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ( 𝑃 𝑄 ) ( 𝑆 𝑇 ) ) ( ( ( 𝑄 𝑅 ) ( 𝑇 𝑈 ) ) ( ( 𝑅 𝑃 ) ( 𝑈 𝑆 ) ) ) ) ) ) )
30 1 2 3 4 dalawlem11 ( ( ( 𝐾 ∈ HL ∧ 𝑃 ( 𝑄 𝑅 ) ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ( 𝑃 𝑄 ) ( 𝑆 𝑇 ) ) ( ( ( 𝑄 𝑅 ) ( 𝑇 𝑈 ) ) ( ( 𝑅 𝑃 ) ( 𝑈 𝑆 ) ) ) )
31 30 3expib ( ( 𝐾 ∈ HL ∧ 𝑃 ( 𝑄 𝑅 ) ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) → ( ( ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ( 𝑃 𝑄 ) ( 𝑆 𝑇 ) ) ( ( ( 𝑄 𝑅 ) ( 𝑇 𝑈 ) ) ( ( 𝑅 𝑃 ) ( 𝑈 𝑆 ) ) ) ) )
32 31 3exp ( 𝐾 ∈ HL → ( 𝑃 ( 𝑄 𝑅 ) → ( ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) → ( ( ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ( 𝑃 𝑄 ) ( 𝑆 𝑇 ) ) ( ( ( 𝑄 𝑅 ) ( 𝑇 𝑈 ) ) ( ( 𝑅 𝑃 ) ( 𝑈 𝑆 ) ) ) ) ) ) )
33 29 32 jaod ( 𝐾 ∈ HL → ( ( 𝑄 = 𝑅𝑃 ( 𝑄 𝑅 ) ) → ( ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) → ( ( ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ( 𝑃 𝑄 ) ( 𝑆 𝑇 ) ) ( ( ( 𝑄 𝑅 ) ( 𝑇 𝑈 ) ) ( ( 𝑅 𝑃 ) ( 𝑈 𝑆 ) ) ) ) ) ) )
34 33 3imp ( ( 𝐾 ∈ HL ∧ ( 𝑄 = 𝑅𝑃 ( 𝑄 𝑅 ) ) ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) → ( ( ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ( 𝑃 𝑄 ) ( 𝑆 𝑇 ) ) ( ( ( 𝑄 𝑅 ) ( 𝑇 𝑈 ) ) ( ( 𝑅 𝑃 ) ( 𝑈 𝑆 ) ) ) ) )
35 34 3impib ( ( ( 𝐾 ∈ HL ∧ ( 𝑄 = 𝑅𝑃 ( 𝑄 𝑅 ) ) ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ( 𝑃 𝑄 ) ( 𝑆 𝑇 ) ) ( ( ( 𝑄 𝑅 ) ( 𝑇 𝑈 ) ) ( ( 𝑅 𝑃 ) ( 𝑈 𝑆 ) ) ) )
36 6 23 24 25 26 35 syl311anc ( ( ( 𝐾 ∈ HL ∧ ¬ ( ( 𝑃 𝑄 ) 𝑅 ) ∈ 𝑂 ∧ ( ( 𝑃 𝑆 ) ( 𝑄 𝑇 ) ) ( 𝑅 𝑈 ) ) ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑆𝐴𝑇𝐴𝑈𝐴 ) ) → ( ( 𝑃 𝑄 ) ( 𝑆 𝑇 ) ) ( ( ( 𝑄 𝑅 ) ( 𝑇 𝑈 ) ) ( ( 𝑅 𝑃 ) ( 𝑈 𝑆 ) ) ) )