Metamath Proof Explorer


Theorem dalem22

Description: Lemma for dath . Show that lines c d and P S determine a plane. (Contributed by NM, 2-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
dalem22.o O = LPlanes K
dalem22.y Y = P ˙ Q ˙ R
dalem22.z Z = S ˙ T ˙ U
Assertion dalem22 φ Y = Z ψ c ˙ d ˙ P ˙ S O

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 dalem22.o O = LPlanes K
7 dalem22.y Y = P ˙ Q ˙ R
8 dalem22.z Z = S ˙ T ˙ U
9 eqid meet K = meet K
10 1 2 3 4 5 9 6 7 8 dalem21 φ Y = Z ψ c ˙ d meet K P ˙ S A
11 1 dalemkehl φ K HL
12 11 adantr φ ψ K HL
13 1 2 3 4 5 dalemcjden φ ψ c ˙ d LLines K
14 1 2 3 4 6 7 dalempjsen φ P ˙ S LLines K
15 14 adantr φ ψ P ˙ S LLines K
16 eqid LLines K = LLines K
17 3 9 4 16 6 2llnmj K HL c ˙ d LLines K P ˙ S LLines K c ˙ d meet K P ˙ S A c ˙ d ˙ P ˙ S O
18 12 13 15 17 syl3anc φ ψ c ˙ d meet K P ˙ S A c ˙ d ˙ P ˙ S O
19 18 3adant2 φ Y = Z ψ c ˙ d meet K P ˙ S A c ˙ d ˙ P ˙ S O
20 10 19 mpbid φ Y = Z ψ c ˙ d ˙ P ˙ S O