Metamath Proof Explorer


Theorem dalem35

Description: Lemma for dath . Analogue of dalem24 for I . (Contributed by NM, 3-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
dalem34.m ˙ = meet K
dalem34.o O = LPlanes K
dalem34.y Y = P ˙ Q ˙ R
dalem34.z Z = S ˙ T ˙ U
dalem34.i I = c ˙ R ˙ d ˙ U
Assertion dalem35 φ Y = Z ψ ¬ I ˙ Y

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 dalem34.m ˙ = meet K
7 dalem34.o O = LPlanes K
8 dalem34.y Y = P ˙ Q ˙ R
9 dalem34.z Z = S ˙ T ˙ U
10 dalem34.i I = c ˙ R ˙ d ˙ U
11 1 2 3 4 8 9 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 11 3ad2ant1 φ Y = Z ψ 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 1 2 3 4 8 9 dalemrotyz φ Y = Z Q ˙ R ˙ P = T ˙ U ˙ S
14 13 3adant3 φ Y = Z ψ Q ˙ R ˙ P = T ˙ U ˙ S
15 1 2 3 4 5 8 dalemrotps φ ψ c A d A ¬ c ˙ Q ˙ R ˙ P d c ¬ d ˙ Q ˙ R ˙ P C ˙ c ˙ d
16 15 3adant2 φ Y = Z ψ c A d A ¬ c ˙ Q ˙ R ˙ P d c ¬ d ˙ Q ˙ R ˙ P C ˙ c ˙ d
17 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
18 biid c A d A ¬ c ˙ Q ˙ R ˙ P d c ¬ d ˙ Q ˙ R ˙ P C ˙ c ˙ d c A d A ¬ c ˙ Q ˙ R ˙ P d c ¬ d ˙ Q ˙ R ˙ P C ˙ c ˙ d
19 eqid Q ˙ R ˙ P = Q ˙ R ˙ P
20 eqid T ˙ U ˙ S = T ˙ U ˙ S
21 17 2 3 4 18 6 7 19 20 10 dalem30 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 Q ˙ R ˙ P = T ˙ U ˙ S c A d A ¬ c ˙ Q ˙ R ˙ P d c ¬ d ˙ Q ˙ R ˙ P C ˙ c ˙ d ¬ I ˙ Q ˙ R ˙ P
22 12 14 16 21 syl3anc φ Y = Z ψ ¬ I ˙ Q ˙ R ˙ P
23 1 3 4 dalemqrprot φ Q ˙ R ˙ P = P ˙ Q ˙ R
24 8 23 eqtr4id φ Y = Q ˙ R ˙ P
25 24 breq2d φ I ˙ Y I ˙ Q ˙ R ˙ P
26 25 3ad2ant1 φ Y = Z ψ I ˙ Y I ˙ Q ˙ R ˙ P
27 22 26 mtbird φ Y = Z ψ ¬ I ˙ Y