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 𝐵 = ( Base ‘ 𝐾 )
lncvrelat.c 𝐶 = ( ⋖ ‘ 𝐾 )
lncvrelat.a 𝐴 = ( Atoms ‘ 𝐾 )
lncvrelat.n 𝑁 = ( Lines ‘ 𝐾 )
lncvrelat.m 𝑀 = ( pmap ‘ 𝐾 )
Assertion lncvrelatN ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑃𝐵 ) ∧ ( ( 𝑀𝑋 ) ∈ 𝑁𝑃 𝐶 𝑋 ) ) → 𝑃𝐴 )

Proof

Step Hyp Ref Expression
1 lncvrelat.b 𝐵 = ( Base ‘ 𝐾 )
2 lncvrelat.c 𝐶 = ( ⋖ ‘ 𝐾 )
3 lncvrelat.a 𝐴 = ( Atoms ‘ 𝐾 )
4 lncvrelat.n 𝑁 = ( Lines ‘ 𝐾 )
5 lncvrelat.m 𝑀 = ( pmap ‘ 𝐾 )
6 hllat ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
7 6 3ad2ant1 ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑃𝐵 ) → 𝐾 ∈ Lat )
8 eqid ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
9 8 3 4 5 isline2 ( 𝐾 ∈ Lat → ( ( 𝑀𝑋 ) ∈ 𝑁 ↔ ∃ 𝑞𝐴𝑟𝐴 ( 𝑞𝑟 ∧ ( 𝑀𝑋 ) = ( 𝑀 ‘ ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) ) )
10 7 9 syl ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑃𝐵 ) → ( ( 𝑀𝑋 ) ∈ 𝑁 ↔ ∃ 𝑞𝐴𝑟𝐴 ( 𝑞𝑟 ∧ ( 𝑀𝑋 ) = ( 𝑀 ‘ ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) ) )
11 simpll1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑃𝐵 ) ∧ ( 𝑞𝐴𝑟𝐴 ) ) ∧ 𝑞𝑟 ) → 𝐾 ∈ HL )
12 simpll2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑃𝐵 ) ∧ ( 𝑞𝐴𝑟𝐴 ) ) ∧ 𝑞𝑟 ) → 𝑋𝐵 )
13 11 6 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑃𝐵 ) ∧ ( 𝑞𝐴𝑟𝐴 ) ) ∧ 𝑞𝑟 ) → 𝐾 ∈ Lat )
14 simplrl ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑃𝐵 ) ∧ ( 𝑞𝐴𝑟𝐴 ) ) ∧ 𝑞𝑟 ) → 𝑞𝐴 )
15 1 3 atbase ( 𝑞𝐴𝑞𝐵 )
16 14 15 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑃𝐵 ) ∧ ( 𝑞𝐴𝑟𝐴 ) ) ∧ 𝑞𝑟 ) → 𝑞𝐵 )
17 simplrr ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑃𝐵 ) ∧ ( 𝑞𝐴𝑟𝐴 ) ) ∧ 𝑞𝑟 ) → 𝑟𝐴 )
18 1 3 atbase ( 𝑟𝐴𝑟𝐵 )
19 17 18 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑃𝐵 ) ∧ ( 𝑞𝐴𝑟𝐴 ) ) ∧ 𝑞𝑟 ) → 𝑟𝐵 )
20 1 8 latjcl ( ( 𝐾 ∈ Lat ∧ 𝑞𝐵𝑟𝐵 ) → ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ∈ 𝐵 )
21 13 16 19 20 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑃𝐵 ) ∧ ( 𝑞𝐴𝑟𝐴 ) ) ∧ 𝑞𝑟 ) → ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ∈ 𝐵 )
22 1 5 pmap11 ( ( 𝐾 ∈ HL ∧ 𝑋𝐵 ∧ ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ∈ 𝐵 ) → ( ( 𝑀𝑋 ) = ( 𝑀 ‘ ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ↔ 𝑋 = ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) )
23 11 12 21 22 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑃𝐵 ) ∧ ( 𝑞𝐴𝑟𝐴 ) ) ∧ 𝑞𝑟 ) → ( ( 𝑀𝑋 ) = ( 𝑀 ‘ ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ↔ 𝑋 = ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) )
24 breq2 ( 𝑋 = ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) → ( 𝑃 𝐶 𝑋𝑃 𝐶 ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) )
25 24 biimpd ( 𝑋 = ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) → ( 𝑃 𝐶 𝑋𝑃 𝐶 ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) )
26 11 adantr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑃𝐵 ) ∧ ( 𝑞𝐴𝑟𝐴 ) ) ∧ 𝑞𝑟 ) ∧ 𝑃 𝐶 ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) → 𝐾 ∈ HL )
27 simpll3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑃𝐵 ) ∧ ( 𝑞𝐴𝑟𝐴 ) ) ∧ 𝑞𝑟 ) → 𝑃𝐵 )
28 27 14 17 3jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑃𝐵 ) ∧ ( 𝑞𝐴𝑟𝐴 ) ) ∧ 𝑞𝑟 ) → ( 𝑃𝐵𝑞𝐴𝑟𝐴 ) )
29 28 adantr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑃𝐵 ) ∧ ( 𝑞𝐴𝑟𝐴 ) ) ∧ 𝑞𝑟 ) ∧ 𝑃 𝐶 ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) → ( 𝑃𝐵𝑞𝐴𝑟𝐴 ) )
30 simplr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑃𝐵 ) ∧ ( 𝑞𝐴𝑟𝐴 ) ) ∧ 𝑞𝑟 ) ∧ 𝑃 𝐶 ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) → 𝑞𝑟 )
31 simpr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑃𝐵 ) ∧ ( 𝑞𝐴𝑟𝐴 ) ) ∧ 𝑞𝑟 ) ∧ 𝑃 𝐶 ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) → 𝑃 𝐶 ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) )
32 1 8 2 3 cvrat2 ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐵𝑞𝐴𝑟𝐴 ) ∧ ( 𝑞𝑟𝑃 𝐶 ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) → 𝑃𝐴 )
33 26 29 30 31 32 syl112anc ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑃𝐵 ) ∧ ( 𝑞𝐴𝑟𝐴 ) ) ∧ 𝑞𝑟 ) ∧ 𝑃 𝐶 ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) → 𝑃𝐴 )
34 33 ex ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑃𝐵 ) ∧ ( 𝑞𝐴𝑟𝐴 ) ) ∧ 𝑞𝑟 ) → ( 𝑃 𝐶 ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) → 𝑃𝐴 ) )
35 25 34 syl9r ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑃𝐵 ) ∧ ( 𝑞𝐴𝑟𝐴 ) ) ∧ 𝑞𝑟 ) → ( 𝑋 = ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) → ( 𝑃 𝐶 𝑋𝑃𝐴 ) ) )
36 23 35 sylbid ( ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑃𝐵 ) ∧ ( 𝑞𝐴𝑟𝐴 ) ) ∧ 𝑞𝑟 ) → ( ( 𝑀𝑋 ) = ( 𝑀 ‘ ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) → ( 𝑃 𝐶 𝑋𝑃𝐴 ) ) )
37 36 expimpd ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑃𝐵 ) ∧ ( 𝑞𝐴𝑟𝐴 ) ) → ( ( 𝑞𝑟 ∧ ( 𝑀𝑋 ) = ( 𝑀 ‘ ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) → ( 𝑃 𝐶 𝑋𝑃𝐴 ) ) )
38 37 rexlimdvva ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑃𝐵 ) → ( ∃ 𝑞𝐴𝑟𝐴 ( 𝑞𝑟 ∧ ( 𝑀𝑋 ) = ( 𝑀 ‘ ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) → ( 𝑃 𝐶 𝑋𝑃𝐴 ) ) )
39 10 38 sylbid ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑃𝐵 ) → ( ( 𝑀𝑋 ) ∈ 𝑁 → ( 𝑃 𝐶 𝑋𝑃𝐴 ) ) )
40 39 imp32 ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵𝑃𝐵 ) ∧ ( ( 𝑀𝑋 ) ∈ 𝑁𝑃 𝐶 𝑋 ) ) → 𝑃𝐴 )