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 ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐵 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 𝐶 𝑋 ) ) → 𝑃 ∈ 𝐴 )