# Metamath Proof Explorer

## Theorem lplnexllnN

Description: Given an atom on a lattice plane, there is a lattice line whose join with the atom equals the plane. (Contributed by NM, 26-Jun-2012) (New usage is discouraged.)

Ref Expression
Hypotheses lplnexat.l
lplnexat.j
lplnexat.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
lplnexat.n ${⊢}{N}=\mathrm{LLines}\left({K}\right)$
lplnexat.p ${⊢}{P}=\mathrm{LPlanes}\left({K}\right)$
Assertion lplnexllnN

### Proof

Step Hyp Ref Expression
1 lplnexat.l
2 lplnexat.j
3 lplnexat.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
4 lplnexat.n ${⊢}{N}=\mathrm{LLines}\left({K}\right)$
5 lplnexat.p ${⊢}{P}=\mathrm{LPlanes}\left({K}\right)$
6 simpl2
7 simpl1
8 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
9 8 5 lplnbase ${⊢}{X}\in {P}\to {X}\in {\mathrm{Base}}_{{K}}$
10 6 9 syl
11 8 1 2 3 4 5 islpln3
12 7 10 11 syl2anc
13 6 12 mpbid
14 simpll1
15 simpr2l
16 simpll3
17 simpr1
18 1 2 3 4 llnexatN
19 14 15 16 17 18 syl31anc
20 simp1l1
21 simp22r
22 simp3l
23 simp1l3
24 simp23l
25 simp3rr
26 25 breq2d
27 24 26 mtbid
28 1 2 3 atnlej2
29 20 21 23 22 27 28 syl131anc
30 2 3 4 llni2
31 20 21 22 29 30 syl31anc
32 simp3rl
33 1 2 3 hlatcon2
34 20 23 22 21 32 27 33 syl132anc
35 simp23r
36 25 oveq1d
37 20 hllatd
38 8 3 atbase ${⊢}{Q}\in {A}\to {Q}\in {\mathrm{Base}}_{{K}}$
39 23 38 syl
40 8 3 atbase ${⊢}{s}\in {A}\to {s}\in {\mathrm{Base}}_{{K}}$
41 22 40 syl
42 8 3 atbase ${⊢}{r}\in {A}\to {r}\in {\mathrm{Base}}_{{K}}$
43 21 42 syl
44 8 2 latj31
45 37 39 41 43 44 syl13anc
46 35 36 45 3eqtrd
47 breq2
48 47 notbid
49 oveq1
50 49 eqeq2d
51 48 50 anbi12d
52 51 rspcev
53 31 34 46 52 syl12anc
54 53 3expia
55 54 expd
56 55 rexlimdv
57 19 56 mpd
58 57 3exp2
59 simpr2l
60 simpr1
61 simpll1
62 61 hllatd
63 8 4 llnbase ${⊢}{z}\in {N}\to {z}\in {\mathrm{Base}}_{{K}}$
64 59 63 syl
65 simpr2r
66 65 42 syl
67 8 1 2 latlej1
68 62 64 66 67 syl3anc
69 simpr3r
70 68 69 breqtrrd
71 simplr
72 simpll3
73 72 38 syl
74 simpll2
75 74 9 syl
76 8 1 2 latjle12
77 62 64 73 75 76 syl13anc
78 70 71 77 mpbi2and
79 8 2 latjcl
80 62 64 73 79 syl3anc
81 eqid ${⊢}{⋖}_{{K}}={⋖}_{{K}}$
82 8 1 2 81 3 cvr1
83 61 64 72 82 syl3anc
84 60 83 mpbid
85 8 81 4 5 lplni
86 61 80 59 84 85 syl31anc
87 1 5 lplncmp
88 61 86 74 87 syl3anc
89 78 88 mpbid
90 89 eqcomd
91 breq2
92 91 notbid
93 oveq1
94 93 eqeq2d
95 92 94 anbi12d
96 95 rspcev
97 59 60 90 96 syl12anc
98 97 3exp2
99 58 98 pm2.61d
100 99 rexlimdvv
101 13 100 mpd