Metamath Proof Explorer


Theorem dalem11

Description: Lemma for dath . Analogue of dalem10 for E . (Contributed by NM, 23-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
dalem11.m ˙ = meet K
dalem11.o O = LPlanes K
dalem11.y Y = P ˙ Q ˙ R
dalem11.z Z = S ˙ T ˙ U
dalem11.x X = Y ˙ Z
dalem11.e E = Q ˙ R ˙ T ˙ U
Assertion dalem11 φ E ˙ X

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 dalem11.m ˙ = meet K
6 dalem11.o O = LPlanes K
7 dalem11.y Y = P ˙ Q ˙ R
8 dalem11.z Z = S ˙ T ˙ U
9 dalem11.x X = Y ˙ Z
10 dalem11.e E = Q ˙ R ˙ T ˙ U
11 1 2 3 4 7 8 dalemrot φ K HL C Base K Q A R A P A T A U A S A Q ˙ R ˙ P O T ˙ U ˙ S O ¬ C ˙ Q ˙ R ¬ C ˙ R ˙ P ¬ C ˙ P ˙ Q ¬ C ˙ T ˙ U ¬ C ˙ U ˙ S ¬ C ˙ S ˙ T C ˙ Q ˙ T C ˙ R ˙ U C ˙ P ˙ S
12 biid K HL C Base K Q A R A P A T A U A S A Q ˙ R ˙ P O T ˙ U ˙ S O ¬ C ˙ Q ˙ R ¬ C ˙ R ˙ P ¬ C ˙ P ˙ Q ¬ C ˙ T ˙ U ¬ C ˙ U ˙ S ¬ C ˙ S ˙ T C ˙ Q ˙ T C ˙ R ˙ U C ˙ P ˙ S K HL C Base K Q A R A P A T A U A S A Q ˙ R ˙ P O T ˙ U ˙ S O ¬ C ˙ Q ˙ R ¬ C ˙ R ˙ P ¬ C ˙ P ˙ Q ¬ C ˙ T ˙ U ¬ C ˙ U ˙ S ¬ C ˙ S ˙ T C ˙ Q ˙ T C ˙ R ˙ U C ˙ P ˙ S
13 eqid Q ˙ R ˙ P = Q ˙ R ˙ P
14 eqid T ˙ U ˙ S = T ˙ U ˙ S
15 eqid Q ˙ R ˙ P ˙ T ˙ U ˙ S = Q ˙ R ˙ P ˙ T ˙ U ˙ S
16 12 2 3 4 5 6 13 14 15 10 dalem10 K HL C Base K Q A R A P A T A U A S A Q ˙ R ˙ P O T ˙ U ˙ S O ¬ C ˙ Q ˙ R ¬ C ˙ R ˙ P ¬ C ˙ P ˙ Q ¬ C ˙ T ˙ U ¬ C ˙ U ˙ S ¬ C ˙ S ˙ T C ˙ Q ˙ T C ˙ R ˙ U C ˙ P ˙ S E ˙ Q ˙ R ˙ P ˙ T ˙ U ˙ S
17 11 16 syl φ E ˙ Q ˙ R ˙ P ˙ T ˙ U ˙ S
18 1 3 4 dalemqrprot φ Q ˙ R ˙ P = P ˙ Q ˙ R
19 7 18 eqtr4id φ Y = Q ˙ R ˙ P
20 1 dalemkehl φ K HL
21 1 dalemtea φ T A
22 1 dalemuea φ U A
23 1 dalemsea φ S A
24 3 4 hlatjrot K HL T A U A S A T ˙ U ˙ S = S ˙ T ˙ U
25 20 21 22 23 24 syl13anc φ T ˙ U ˙ S = S ˙ T ˙ U
26 8 25 eqtr4id φ Z = T ˙ U ˙ S
27 19 26 oveq12d φ Y ˙ Z = Q ˙ R ˙ P ˙ T ˙ U ˙ S
28 9 27 syl5eq φ X = Q ˙ R ˙ P ˙ T ˙ U ˙ S
29 17 28 breqtrrd φ E ˙ X