Metamath Proof Explorer


Theorem dalem58

Description: Lemma for dath . Analogue of dalem57 for E . (Contributed by NM, 10-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
dalem58.m ˙ = meet K
dalem58.o O = LPlanes K
dalem58.y Y = P ˙ Q ˙ R
dalem58.z Z = S ˙ T ˙ U
dalem58.e E = Q ˙ R ˙ T ˙ U
dalem58.g G = c ˙ P ˙ d ˙ S
dalem58.h H = c ˙ Q ˙ d ˙ T
dalem58.i I = c ˙ R ˙ d ˙ U
dalem58.b1 B = G ˙ H ˙ I ˙ Y
Assertion dalem58 φ Y = Z ψ E ˙ B

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 dalem58.m ˙ = meet K
7 dalem58.o O = LPlanes K
8 dalem58.y Y = P ˙ Q ˙ R
9 dalem58.z Z = S ˙ T ˙ U
10 dalem58.e E = Q ˙ R ˙ T ˙ U
11 dalem58.g G = c ˙ P ˙ d ˙ S
12 dalem58.h H = c ˙ Q ˙ d ˙ T
13 dalem58.i I = c ˙ R ˙ d ˙ U
14 dalem58.b1 B = G ˙ H ˙ I ˙ Y
15 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
16 15 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
17 1 2 3 4 8 9 dalemrotyz φ Y = Z Q ˙ R ˙ P = T ˙ U ˙ S
18 17 3adant3 φ Y = Z ψ Q ˙ R ˙ P = T ˙ U ˙ S
19 1 2 3 4 5 8 dalemrotps φ ψ c A d A ¬ c ˙ Q ˙ R ˙ P d c ¬ d ˙ Q ˙ R ˙ P C ˙ c ˙ d
20 19 3adant2 φ Y = Z ψ c A d A ¬ c ˙ Q ˙ R ˙ P d c ¬ d ˙ Q ˙ R ˙ P C ˙ c ˙ d
21 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
22 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
23 eqid Q ˙ R ˙ P = Q ˙ R ˙ P
24 eqid T ˙ U ˙ S = T ˙ U ˙ S
25 eqid H ˙ I ˙ G ˙ Q ˙ R ˙ P = H ˙ I ˙ G ˙ Q ˙ R ˙ P
26 21 2 3 4 22 6 7 23 24 10 12 13 11 25 dalem57 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 E ˙ H ˙ I ˙ G ˙ Q ˙ R ˙ P
27 16 18 20 26 syl3anc φ Y = Z ψ E ˙ H ˙ I ˙ G ˙ Q ˙ R ˙ P
28 1 dalemkehl φ K HL
29 28 3ad2ant1 φ Y = Z ψ K HL
30 1 2 3 4 5 6 7 8 9 12 dalem29 φ Y = Z ψ H A
31 1 2 3 4 5 6 7 8 9 13 dalem34 φ Y = Z ψ I A
32 1 2 3 4 5 6 7 8 9 11 dalem23 φ Y = Z ψ G A
33 3 4 hlatjrot K HL H A I A G A H ˙ I ˙ G = G ˙ H ˙ I
34 29 30 31 32 33 syl13anc φ Y = Z ψ H ˙ I ˙ G = G ˙ H ˙ I
35 1 3 4 dalemqrprot φ Q ˙ R ˙ P = P ˙ Q ˙ R
36 35 8 eqtr4di φ Q ˙ R ˙ P = Y
37 36 3ad2ant1 φ Y = Z ψ Q ˙ R ˙ P = Y
38 34 37 oveq12d φ Y = Z ψ H ˙ I ˙ G ˙ Q ˙ R ˙ P = G ˙ H ˙ I ˙ Y
39 38 14 eqtr4di φ Y = Z ψ H ˙ I ˙ G ˙ Q ˙ R ˙ P = B
40 27 39 breqtrd φ Y = Z ψ E ˙ B