Metamath Proof Explorer


Theorem dalem7

Description: Lemma for dath . Analogue of dalem5 for T . (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
dalem6.o O = LPlanes K
dalem6.y Y = P ˙ Q ˙ R
dalem6.z Z = S ˙ T ˙ U
dalem6.w W = Y ˙ C
Assertion dalem7 φ T ˙ 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 dalem6.o O = LPlanes K
6 dalem6.y Y = P ˙ Q ˙ R
7 dalem6.z Z = S ˙ T ˙ U
8 dalem6.w W = Y ˙ C
9 1 2 3 4 6 7 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
10 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
11 eqid Q ˙ R ˙ P = Q ˙ R ˙ P
12 eqid T ˙ U ˙ S = T ˙ U ˙ S
13 eqid Q ˙ R ˙ P ˙ C = Q ˙ R ˙ P ˙ C
14 10 2 3 4 5 11 12 13 dalem6 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 T ˙ Q ˙ R ˙ P ˙ C
15 9 14 syl φ T ˙ Q ˙ R ˙ P ˙ C
16 1 3 4 dalemqrprot φ Q ˙ R ˙ P = P ˙ Q ˙ R
17 6 16 eqtr4id φ Y = Q ˙ R ˙ P
18 17 oveq1d φ Y ˙ C = Q ˙ R ˙ P ˙ C
19 8 18 syl5eq φ W = Q ˙ R ˙ P ˙ C
20 15 19 breqtrrd φ T ˙ W