Metamath Proof Explorer


Theorem lplnnlelln

Description: A lattice plane is not less than or equal to a lattice line. (Contributed by NM, 14-Jul-2012)

Ref Expression
Hypotheses lplnnlelln.l ˙=K
lplnnlelln.n N=LLinesK
lplnnlelln.p P=LPlanesK
Assertion lplnnlelln KHLXPYN¬X˙Y

Proof

Step Hyp Ref Expression
1 lplnnlelln.l ˙=K
2 lplnnlelln.n N=LLinesK
3 lplnnlelln.p P=LPlanesK
4 simp3 KHLXPYNYN
5 eqid BaseK=BaseK
6 eqid joinK=joinK
7 eqid AtomsK=AtomsK
8 5 6 7 2 islln2 KHLYNYBaseKqAtomsKrAtomsKqrY=qjoinKr
9 8 3ad2ant1 KHLXPYNYNYBaseKqAtomsKrAtomsKqrY=qjoinKr
10 4 9 mpbid KHLXPYNYBaseKqAtomsKrAtomsKqrY=qjoinKr
11 simp11 KHLXPYNqAtomsKrAtomsKqrY=qjoinKrKHL
12 simp12 KHLXPYNqAtomsKrAtomsKqrY=qjoinKrXP
13 simp2l KHLXPYNqAtomsKrAtomsKqrY=qjoinKrqAtomsK
14 simp2r KHLXPYNqAtomsKrAtomsKqrY=qjoinKrrAtomsK
15 1 6 7 3 lplnnle2at KHLXPqAtomsKrAtomsK¬X˙qjoinKr
16 11 12 13 14 15 syl13anc KHLXPYNqAtomsKrAtomsKqrY=qjoinKr¬X˙qjoinKr
17 simp3r KHLXPYNqAtomsKrAtomsKqrY=qjoinKrY=qjoinKr
18 17 breq2d KHLXPYNqAtomsKrAtomsKqrY=qjoinKrX˙YX˙qjoinKr
19 16 18 mtbird KHLXPYNqAtomsKrAtomsKqrY=qjoinKr¬X˙Y
20 19 3exp KHLXPYNqAtomsKrAtomsKqrY=qjoinKr¬X˙Y
21 20 rexlimdvv KHLXPYNqAtomsKrAtomsKqrY=qjoinKr¬X˙Y
22 21 adantld KHLXPYNYBaseKqAtomsKrAtomsKqrY=qjoinKr¬X˙Y
23 10 22 mpd KHLXPYN¬X˙Y