Metamath Proof Explorer


Theorem 3dim0

Description: There exists a 3-dimensional (height-4) element i.e. a volume. (Contributed by NM, 25-Jul-2012)

Ref Expression
Hypotheses 3dim0.j ˙ = join K
3dim0.l ˙ = K
3dim0.a A = Atoms K
Assertion 3dim0 K HL p A q A r A s A p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r

Proof

Step Hyp Ref Expression
1 3dim0.j ˙ = join K
2 3dim0.l ˙ = K
3 3dim0.a A = Atoms K
4 eqid K = K
5 1 4 3 athgt K HL p A q A p K p ˙ q r A p ˙ q K p ˙ q ˙ r s A p ˙ q ˙ r K p ˙ q ˙ r ˙ s
6 df-3an p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r
7 simpll1 K HL p A q A r A s A K HL
8 eqid Base K = Base K
9 8 1 3 hlatjcl K HL p A q A p ˙ q Base K
10 9 ad2antrr K HL p A q A r A s A p ˙ q Base K
11 simplr K HL p A q A r A s A r A
12 8 2 1 4 3 cvr1 K HL p ˙ q Base K r A ¬ r ˙ p ˙ q p ˙ q K p ˙ q ˙ r
13 7 10 11 12 syl3anc K HL p A q A r A s A ¬ r ˙ p ˙ q p ˙ q K p ˙ q ˙ r
14 13 anbi2d K HL p A q A r A s A p q ¬ r ˙ p ˙ q p q p ˙ q K p ˙ q ˙ r
15 7 hllatd K HL p A q A r A s A K Lat
16 8 3 atbase r A r Base K
17 16 ad2antlr K HL p A q A r A s A r Base K
18 8 1 latjcl K Lat p ˙ q Base K r Base K p ˙ q ˙ r Base K
19 15 10 17 18 syl3anc K HL p A q A r A s A p ˙ q ˙ r Base K
20 simpr K HL p A q A r A s A s A
21 8 2 1 4 3 cvr1 K HL p ˙ q ˙ r Base K s A ¬ s ˙ p ˙ q ˙ r p ˙ q ˙ r K p ˙ q ˙ r ˙ s
22 7 19 20 21 syl3anc K HL p A q A r A s A ¬ s ˙ p ˙ q ˙ r p ˙ q ˙ r K p ˙ q ˙ r ˙ s
23 14 22 anbi12d K HL p A q A r A s A p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r p q p ˙ q K p ˙ q ˙ r p ˙ q ˙ r K p ˙ q ˙ r ˙ s
24 6 23 syl5bb K HL p A q A r A s A p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r p q p ˙ q K p ˙ q ˙ r p ˙ q ˙ r K p ˙ q ˙ r ˙ s
25 24 rexbidva K HL p A q A r A s A p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r s A p q p ˙ q K p ˙ q ˙ r p ˙ q ˙ r K p ˙ q ˙ r ˙ s
26 r19.42v s A p q p ˙ q K p ˙ q ˙ r p ˙ q ˙ r K p ˙ q ˙ r ˙ s p q p ˙ q K p ˙ q ˙ r s A p ˙ q ˙ r K p ˙ q ˙ r ˙ s
27 anass p q p ˙ q K p ˙ q ˙ r s A p ˙ q ˙ r K p ˙ q ˙ r ˙ s p q p ˙ q K p ˙ q ˙ r s A p ˙ q ˙ r K p ˙ q ˙ r ˙ s
28 26 27 bitri s A p q p ˙ q K p ˙ q ˙ r p ˙ q ˙ r K p ˙ q ˙ r ˙ s p q p ˙ q K p ˙ q ˙ r s A p ˙ q ˙ r K p ˙ q ˙ r ˙ s
29 25 28 bitrdi K HL p A q A r A s A p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r p q p ˙ q K p ˙ q ˙ r s A p ˙ q ˙ r K p ˙ q ˙ r ˙ s
30 29 rexbidva K HL p A q A r A s A p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r r A p q p ˙ q K p ˙ q ˙ r s A p ˙ q ˙ r K p ˙ q ˙ r ˙ s
31 r19.42v r A p q p ˙ q K p ˙ q ˙ r s A p ˙ q ˙ r K p ˙ q ˙ r ˙ s p q r A p ˙ q K p ˙ q ˙ r s A p ˙ q ˙ r K p ˙ q ˙ r ˙ s
32 30 31 bitrdi K HL p A q A r A s A p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r p q r A p ˙ q K p ˙ q ˙ r s A p ˙ q ˙ r K p ˙ q ˙ r ˙ s
33 1 4 3 atcvr1 K HL p A q A p q p K p ˙ q
34 33 anbi1d K HL p A q A p q r A p ˙ q K p ˙ q ˙ r s A p ˙ q ˙ r K p ˙ q ˙ r ˙ s p K p ˙ q r A p ˙ q K p ˙ q ˙ r s A p ˙ q ˙ r K p ˙ q ˙ r ˙ s
35 32 34 bitrd K HL p A q A r A s A p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r p K p ˙ q r A p ˙ q K p ˙ q ˙ r s A p ˙ q ˙ r K p ˙ q ˙ r ˙ s
36 35 3expb K HL p A q A r A s A p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r p K p ˙ q r A p ˙ q K p ˙ q ˙ r s A p ˙ q ˙ r K p ˙ q ˙ r ˙ s
37 36 2rexbidva K HL p A q A r A s A p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r p A q A p K p ˙ q r A p ˙ q K p ˙ q ˙ r s A p ˙ q ˙ r K p ˙ q ˙ r ˙ s
38 5 37 mpbird K HL p A q A r A s A p q ¬ r ˙ p ˙ q ¬ s ˙ p ˙ q ˙ r