Metamath Proof Explorer


Theorem dalem13

Description: Lemma for dalem14 . (Contributed by NM, 21-Jul-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
dalem13.o O = LPlanes K
dalem13.y Y = P ˙ Q ˙ R
dalem13.z Z = S ˙ T ˙ U
dalem13.w W = Y ˙ C
Assertion dalem13 φ Y Z Y ˙ Z = W

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 dalem13.o O = LPlanes K
6 dalem13.y Y = P ˙ Q ˙ R
7 dalem13.z Z = S ˙ T ˙ U
8 dalem13.w W = Y ˙ C
9 1 dalemkehl φ K HL
10 9 adantr φ Y Z K HL
11 1 dalemyeo φ Y O
12 11 adantr φ Y Z Y O
13 1 dalemzeo φ Z O
14 13 adantr φ Y Z Z O
15 eqid LVols K = LVols K
16 1 2 3 4 5 15 6 7 8 dalem9 φ Y Z W LVols K
17 1 dalemkelat φ K Lat
18 1 5 dalemyeb φ Y Base K
19 1 4 dalemceb φ C Base K
20 eqid Base K = Base K
21 20 2 3 latlej1 K Lat Y Base K C Base K Y ˙ Y ˙ C
22 17 18 19 21 syl3anc φ Y ˙ Y ˙ C
23 22 8 breqtrrdi φ Y ˙ W
24 23 adantr φ Y Z Y ˙ W
25 1 2 3 4 5 6 7 8 dalem8 φ Z ˙ W
26 25 adantr φ Y Z Z ˙ W
27 simpr φ Y Z Y Z
28 2 3 5 15 2lplnj K HL Y O Z O W LVols K Y ˙ W Z ˙ W Y Z Y ˙ Z = W
29 10 12 14 16 24 26 27 28 syl133anc φ Y Z Y ˙ Z = W