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 ˙ = K
dalawlem.j ˙ = join K
dalawlem.m ˙ = meet K
dalawlem.a A = Atoms K
dalawlem2.o O = LPlanes K
Assertion dalawlem13 K HL ¬ P ˙ Q ˙ R O P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S

Proof

Step Hyp Ref Expression
1 dalawlem.l ˙ = K
2 dalawlem.j ˙ = join K
3 dalawlem.m ˙ = meet K
4 dalawlem.a A = Atoms K
5 dalawlem2.o O = LPlanes K
6 simp11 K HL ¬ P ˙ Q ˙ R O P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A K HL
7 simp12 K HL ¬ P ˙ Q ˙ R O P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A ¬ P ˙ Q ˙ R O
8 simp22 K HL ¬ P ˙ Q ˙ R O P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q A
9 simp23 K HL ¬ P ˙ Q ˙ R O P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A R A
10 simp21 K HL ¬ P ˙ Q ˙ R O P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P A
11 1 2 4 5 islpln2a K HL Q A R A P A Q ˙ R ˙ P O Q R ¬ P ˙ Q ˙ R
12 6 8 9 10 11 syl13anc K HL ¬ P ˙ Q ˙ R O P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ R ˙ P O Q R ¬ P ˙ Q ˙ R
13 df-ne Q R ¬ Q = R
14 13 anbi1i Q R ¬ P ˙ Q ˙ R ¬ Q = R ¬ P ˙ Q ˙ R
15 pm4.56 ¬ Q = R ¬ P ˙ Q ˙ R ¬ Q = R P ˙ Q ˙ R
16 14 15 bitri Q R ¬ P ˙ Q ˙ R ¬ Q = R P ˙ Q ˙ R
17 12 16 bitr2di K HL ¬ P ˙ Q ˙ R O P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A ¬ Q = R P ˙ Q ˙ R Q ˙ R ˙ P O
18 2 4 hlatjrot K HL Q A R A P A Q ˙ R ˙ P = P ˙ Q ˙ R
19 6 8 9 10 18 syl13anc K HL ¬ P ˙ Q ˙ R O P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ R ˙ P = P ˙ Q ˙ R
20 19 eleq1d K HL ¬ P ˙ Q ˙ R O P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ R ˙ P O P ˙ Q ˙ R O
21 17 20 bitrd K HL ¬ P ˙ Q ˙ R O P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A ¬ Q = R P ˙ Q ˙ R P ˙ Q ˙ R O
22 21 con1bid K HL ¬ P ˙ Q ˙ R O P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A ¬ P ˙ Q ˙ R O Q = R P ˙ Q ˙ R
23 7 22 mpbid K HL ¬ P ˙ Q ˙ R O P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q = R P ˙ Q ˙ R
24 simp13 K HL ¬ P ˙ Q ˙ R O P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ S ˙ Q ˙ T ˙ R ˙ U
25 simp2 K HL ¬ P ˙ Q ˙ R O P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P A Q A R A
26 simp3 K HL ¬ P ˙ Q ˙ R O P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A S A T A U A
27 1 2 3 4 dalawlem12 K HL Q = R P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
28 27 3expib K HL Q = R P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
29 28 3exp K HL Q = R P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
30 1 2 3 4 dalawlem11 K HL P ˙ Q ˙ R P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
31 30 3expib K HL P ˙ Q ˙ R P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
32 31 3exp K HL P ˙ Q ˙ R P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
33 29 32 jaod K HL Q = R P ˙ Q ˙ R P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
34 33 3imp K HL Q = R P ˙ Q ˙ R P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
35 34 3impib K HL Q = R P ˙ Q ˙ R P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
36 6 23 24 25 26 35 syl311anc K HL ¬ P ˙ Q ˙ R O P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S