Metamath Proof Explorer


Theorem lncvrelatN

Description: A lattice element covered by a line is an atom. (Contributed by NM, 28-Apr-2012) (New usage is discouraged.)

Ref Expression
Hypotheses lncvrelat.b B = Base K
lncvrelat.c C = K
lncvrelat.a A = Atoms K
lncvrelat.n N = Lines K
lncvrelat.m M = pmap K
Assertion lncvrelatN K HL X B P B M X N P C X P A

Proof

Step Hyp Ref Expression
1 lncvrelat.b B = Base K
2 lncvrelat.c C = K
3 lncvrelat.a A = Atoms K
4 lncvrelat.n N = Lines K
5 lncvrelat.m M = pmap K
6 hllat K HL K Lat
7 6 3ad2ant1 K HL X B P B K Lat
8 eqid join K = join K
9 8 3 4 5 isline2 K Lat M X N q A r A q r M X = M q join K r
10 7 9 syl K HL X B P B M X N q A r A q r M X = M q join K r
11 simpll1 K HL X B P B q A r A q r K HL
12 simpll2 K HL X B P B q A r A q r X B
13 11 6 syl K HL X B P B q A r A q r K Lat
14 simplrl K HL X B P B q A r A q r q A
15 1 3 atbase q A q B
16 14 15 syl K HL X B P B q A r A q r q B
17 simplrr K HL X B P B q A r A q r r A
18 1 3 atbase r A r B
19 17 18 syl K HL X B P B q A r A q r r B
20 1 8 latjcl K Lat q B r B q join K r B
21 13 16 19 20 syl3anc K HL X B P B q A r A q r q join K r B
22 1 5 pmap11 K HL X B q join K r B M X = M q join K r X = q join K r
23 11 12 21 22 syl3anc K HL X B P B q A r A q r M X = M q join K r X = q join K r
24 breq2 X = q join K r P C X P C q join K r
25 24 biimpd X = q join K r P C X P C q join K r
26 11 adantr K HL X B P B q A r A q r P C q join K r K HL
27 simpll3 K HL X B P B q A r A q r P B
28 27 14 17 3jca K HL X B P B q A r A q r P B q A r A
29 28 adantr K HL X B P B q A r A q r P C q join K r P B q A r A
30 simplr K HL X B P B q A r A q r P C q join K r q r
31 simpr K HL X B P B q A r A q r P C q join K r P C q join K r
32 1 8 2 3 cvrat2 K HL P B q A r A q r P C q join K r P A
33 26 29 30 31 32 syl112anc K HL X B P B q A r A q r P C q join K r P A
34 33 ex K HL X B P B q A r A q r P C q join K r P A
35 25 34 syl9r K HL X B P B q A r A q r X = q join K r P C X P A
36 23 35 sylbid K HL X B P B q A r A q r M X = M q join K r P C X P A
37 36 expimpd K HL X B P B q A r A q r M X = M q join K r P C X P A
38 37 rexlimdvva K HL X B P B q A r A q r M X = M q join K r P C X P A
39 10 38 sylbid K HL X B P B M X N P C X P A
40 39 imp32 K HL X B P B M X N P C X P A