Metamath Proof Explorer


Theorem dalem48

Description: Lemma for dath . Analogue of dalem45 for P Q . (Contributed by NM, 16-Aug-2012)

Ref Expression
Hypotheses dalem.ph φ K HL C Base K P A Q A R A S A T A U A Y O Z O ¬ C ˙ P ˙ Q ¬ C ˙ Q ˙ R ¬ C ˙ R ˙ P ¬ C ˙ S ˙ T ¬ C ˙ T ˙ U ¬ C ˙ U ˙ S C ˙ P ˙ S C ˙ Q ˙ T C ˙ R ˙ U
dalem.l ˙ = K
dalem.j ˙ = join K
dalem.a A = Atoms K
dalem.ps ψ c A d A ¬ c ˙ Y d c ¬ d ˙ Y C ˙ c ˙ d
dalem44.m ˙ = meet K
dalem44.o O = LPlanes K
dalem44.y Y = P ˙ Q ˙ R
dalem44.z Z = S ˙ T ˙ U
dalem44.g G = c ˙ P ˙ d ˙ S
dalem44.h H = c ˙ Q ˙ d ˙ T
dalem44.i I = c ˙ R ˙ d ˙ U
Assertion dalem48 φ ψ ¬ c ˙ P ˙ Q

Proof

Step Hyp Ref Expression
1 dalem.ph φ K HL C Base K P A Q A R A S A T A U A Y O Z O ¬ C ˙ P ˙ Q ¬ C ˙ Q ˙ R ¬ C ˙ R ˙ P ¬ C ˙ S ˙ T ¬ C ˙ T ˙ U ¬ C ˙ U ˙ S C ˙ P ˙ S C ˙ Q ˙ T C ˙ R ˙ U
2 dalem.l ˙ = K
3 dalem.j ˙ = join K
4 dalem.a A = Atoms K
5 dalem.ps ψ c A d A ¬ c ˙ Y d c ¬ d ˙ Y C ˙ c ˙ d
6 dalem44.m ˙ = meet K
7 dalem44.o O = LPlanes K
8 dalem44.y Y = P ˙ Q ˙ R
9 dalem44.z Z = S ˙ T ˙ U
10 dalem44.g G = c ˙ P ˙ d ˙ S
11 dalem44.h H = c ˙ Q ˙ d ˙ T
12 dalem44.i I = c ˙ R ˙ d ˙ U
13 1 dalemkelat φ K Lat
14 13 adantr φ ψ K Lat
15 5 4 dalemcceb ψ c Base K
16 15 adantl φ ψ c Base K
17 1 3 4 dalempjqeb φ P ˙ Q Base K
18 17 adantr φ ψ P ˙ Q Base K
19 1 4 dalemreb φ R Base K
20 19 adantr φ ψ R Base K
21 5 dalem-ccly ψ ¬ c ˙ Y
22 8 breq2i c ˙ Y c ˙ P ˙ Q ˙ R
23 21 22 sylnib ψ ¬ c ˙ P ˙ Q ˙ R
24 23 adantl φ ψ ¬ c ˙ P ˙ Q ˙ R
25 eqid Base K = Base K
26 25 2 3 latnlej2l K Lat c Base K P ˙ Q Base K R Base K ¬ c ˙ P ˙ Q ˙ R ¬ c ˙ P ˙ Q
27 14 16 18 20 24 26 syl131anc φ ψ ¬ c ˙ P ˙ Q