Metamath Proof Explorer


Theorem dalemdea

Description: Lemma for dath . Frequently-used utility lemma. (Contributed by NM, 11-Aug-2012)

Ref Expression
Hypotheses dalema.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
dalemc.l ˙ = K
dalemc.j ˙ = join K
dalemc.a A = Atoms K
dalemdea.m ˙ = meet K
dalemdea.o O = LPlanes K
dalemdea.y Y = P ˙ Q ˙ R
dalemdea.z Z = S ˙ T ˙ U
dalemdea.d D = P ˙ Q ˙ S ˙ T
Assertion dalemdea φ D A

Proof

Step Hyp Ref Expression
1 dalema.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 dalemc.l ˙ = K
3 dalemc.j ˙ = join K
4 dalemc.a A = Atoms K
5 dalemdea.m ˙ = meet K
6 dalemdea.o O = LPlanes K
7 dalemdea.y Y = P ˙ Q ˙ R
8 dalemdea.z Z = S ˙ T ˙ U
9 dalemdea.d D = P ˙ Q ˙ S ˙ T
10 1 2 3 4 6 7 dalem2 φ P ˙ Q ˙ S ˙ T O
11 1 dalemkehl φ K HL
12 1 dalempea φ P A
13 1 dalemqea φ Q A
14 1 dalemrea φ R A
15 1 dalemyeo φ Y O
16 3 4 6 7 lplnri1 K HL P A Q A R A Y O P Q
17 11 12 13 14 15 16 syl131anc φ P Q
18 eqid LLines K = LLines K
19 3 4 18 llni2 K HL P A Q A P Q P ˙ Q LLines K
20 11 12 13 17 19 syl31anc φ P ˙ Q LLines K
21 1 dalemsea φ S A
22 1 dalemtea φ T A
23 1 dalemuea φ U A
24 1 dalemzeo φ Z O
25 3 4 6 8 lplnri1 K HL S A T A U A Z O S T
26 11 21 22 23 24 25 syl131anc φ S T
27 3 4 18 llni2 K HL S A T A S T S ˙ T LLines K
28 11 21 22 26 27 syl31anc φ S ˙ T LLines K
29 3 5 4 18 6 2llnmj K HL P ˙ Q LLines K S ˙ T LLines K P ˙ Q ˙ S ˙ T A P ˙ Q ˙ S ˙ T O
30 11 20 28 29 syl3anc φ P ˙ Q ˙ S ˙ T A P ˙ Q ˙ S ˙ T O
31 10 30 mpbird φ P ˙ Q ˙ S ˙ T A
32 9 31 eqeltrid φ D A