Metamath Proof Explorer


Theorem 2dim

Description: Generate a height-3 element (2-dimensional plane) from an atom. (Contributed by NM, 3-May-2012)

Ref Expression
Hypotheses 2dim.j ˙ = join K
2dim.c C = K
2dim.a A = Atoms K
Assertion 2dim K HL P A q A r A P C P ˙ q P ˙ q C P ˙ q ˙ r

Proof

Step Hyp Ref Expression
1 2dim.j ˙ = join K
2 2dim.c C = K
3 2dim.a A = Atoms K
4 eqid K = K
5 1 4 3 3dim1 K HL P A q A r A s A P q ¬ r K P ˙ q ¬ s K P ˙ q ˙ r
6 df-3an P q ¬ r K P ˙ q ¬ s K P ˙ q ˙ r P q ¬ r K P ˙ q ¬ s K P ˙ q ˙ r
7 6 rexbii s A P q ¬ r K P ˙ q ¬ s K P ˙ q ˙ r s A P q ¬ r K P ˙ q ¬ s K P ˙ q ˙ r
8 r19.42v s A P q ¬ r K P ˙ q ¬ s K P ˙ q ˙ r P q ¬ r K P ˙ q s A ¬ s K P ˙ q ˙ r
9 7 8 bitri s A P q ¬ r K P ˙ q ¬ s K P ˙ q ˙ r P q ¬ r K P ˙ q s A ¬ s K P ˙ q ˙ r
10 9 simplbi s A P q ¬ r K P ˙ q ¬ s K P ˙ q ˙ r P q ¬ r K P ˙ q
11 simplll K HL P A q A r A K HL
12 hlatl K HL K AtLat
13 11 12 syl K HL P A q A r A K AtLat
14 simplr K HL P A q A r A q A
15 simpllr K HL P A q A r A P A
16 4 3 atncmp K AtLat q A P A ¬ q K P q P
17 13 14 15 16 syl3anc K HL P A q A r A ¬ q K P q P
18 necom q P P q
19 17 18 bitr2di K HL P A q A r A P q ¬ q K P
20 eqid Base K = Base K
21 20 3 atbase P A P Base K
22 15 21 syl K HL P A q A r A P Base K
23 20 4 1 2 3 cvr1 K HL P Base K q A ¬ q K P P C P ˙ q
24 11 22 14 23 syl3anc K HL P A q A r A ¬ q K P P C P ˙ q
25 19 24 bitrd K HL P A q A r A P q P C P ˙ q
26 20 1 3 hlatjcl K HL P A q A P ˙ q Base K
27 11 15 14 26 syl3anc K HL P A q A r A P ˙ q Base K
28 simpr K HL P A q A r A r A
29 20 4 1 2 3 cvr1 K HL P ˙ q Base K r A ¬ r K P ˙ q P ˙ q C P ˙ q ˙ r
30 11 27 28 29 syl3anc K HL P A q A r A ¬ r K P ˙ q P ˙ q C P ˙ q ˙ r
31 25 30 anbi12d K HL P A q A r A P q ¬ r K P ˙ q P C P ˙ q P ˙ q C P ˙ q ˙ r
32 10 31 syl5ib K HL P A q A r A s A P q ¬ r K P ˙ q ¬ s K P ˙ q ˙ r P C P ˙ q P ˙ q C P ˙ q ˙ r
33 32 reximdva K HL P A q A r A s A P q ¬ r K P ˙ q ¬ s K P ˙ q ˙ r r A P C P ˙ q P ˙ q C P ˙ q ˙ r
34 33 reximdva K HL P A q A r A s A P q ¬ r K P ˙ q ¬ s K P ˙ q ˙ r q A r A P C P ˙ q P ˙ q C P ˙ q ˙ r
35 5 34 mpd K HL P A q A r A P C P ˙ q P ˙ q C P ˙ q ˙ r