Metamath Proof Explorer


Theorem dalem12

Description: Lemma for dath . Analogue of dalem10 for F . (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
dalem12.m ˙ = meet K
dalem12.o O = LPlanes K
dalem12.y Y = P ˙ Q ˙ R
dalem12.z Z = S ˙ T ˙ U
dalem12.x X = Y ˙ Z
dalem12.f F = R ˙ P ˙ U ˙ S
Assertion dalem12 φ F ˙ 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 dalem12.m ˙ = meet K
6 dalem12.o O = LPlanes K
7 dalem12.y Y = P ˙ Q ˙ R
8 dalem12.z Z = S ˙ T ˙ U
9 dalem12.x X = Y ˙ Z
10 dalem12.f F = R ˙ P ˙ U ˙ S
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 dalem11 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 F ˙ Q ˙ R ˙ P ˙ T ˙ U ˙ S
17 11 16 syl φ F ˙ 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 φ F ˙ X