Metamath Proof Explorer

Theorem lnatexN

Description: There is an atom in a line different from any other. (Contributed by NM, 30-Apr-2012) (New usage is discouraged.)

Ref Expression
Hypotheses lnatex.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
lnatex.l ⊢ ≤ = ( le ‘ 𝐾 )
lnatex.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
lnatex.n ⊢ 𝑁 = ( Lines ‘ 𝐾 )
lnatex.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
Assertion lnatexN ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≤ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 lnatex.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 lnatex.l ⊢ ≤ = ( le ‘ 𝐾 )
3 lnatex.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 lnatex.n ⊢ 𝑁 = ( Lines ‘ 𝐾 )
5 lnatex.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
6 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
7 1 6 3 4 5 isline3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ↔ ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ) ) )
8 7 biimp3a ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) → ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ) )
9 simpl2r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ) ) ∧ 𝑟 = 𝑃 ) → 𝑠 ∈ 𝐴 )
10 simpl3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ) ) ∧ 𝑟 = 𝑃 ) → 𝑟 ≠ 𝑠 )
11 10 necomd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ) ) ∧ 𝑟 = 𝑃 ) → 𝑠 ≠ 𝑟 )
12 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ) ) ∧ 𝑟 = 𝑃 ) → 𝑟 = 𝑃 )
13 11 12 neeqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ) ) ∧ 𝑟 = 𝑃 ) → 𝑠 ≠ 𝑃 )
14 simpl11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ) ) ∧ 𝑟 = 𝑃 ) → 𝐾 ∈ HL )
15 simpl2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ) ) ∧ 𝑟 = 𝑃 ) → 𝑟 ∈ 𝐴 )
16 2 6 3 hlatlej2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ≤ ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) )
17 14 15 9 16 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ) ) ∧ 𝑟 = 𝑃 ) → 𝑠 ≤ ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) )
18 simpl3r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ) ) ∧ 𝑟 = 𝑃 ) → 𝑋 = ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) )
19 17 18 breqtrrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ) ) ∧ 𝑟 = 𝑃 ) → 𝑠 ≤ 𝑋 )
20 neeq1 ⊢ ( 𝑞 = 𝑠 → ( 𝑞 ≠ 𝑃 ↔ 𝑠 ≠ 𝑃 ) )
21 breq1 ⊢ ( 𝑞 = 𝑠 → ( 𝑞 ≤ 𝑋 ↔ 𝑠 ≤ 𝑋 ) )
22 20 21 anbi12d ⊢ ( 𝑞 = 𝑠 → ( ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≤ 𝑋 ) ↔ ( 𝑠 ≠ 𝑃 ∧ 𝑠 ≤ 𝑋 ) ) )
23 22 rspcev ⊢ ( ( 𝑠 ∈ 𝐴 ∧ ( 𝑠 ≠ 𝑃 ∧ 𝑠 ≤ 𝑋 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≤ 𝑋 ) )
24 9 13 19 23 syl12anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ) ) ∧ 𝑟 = 𝑃 ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≤ 𝑋 ) )
25 simpl2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ) ) ∧ 𝑟 ≠ 𝑃 ) → 𝑟 ∈ 𝐴 )
26 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ) ) ∧ 𝑟 ≠ 𝑃 ) → 𝑟 ≠ 𝑃 )
27 simpl11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ) ) ∧ 𝑟 ≠ 𝑃 ) → 𝐾 ∈ HL )
28 simpl2r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ) ) ∧ 𝑟 ≠ 𝑃 ) → 𝑠 ∈ 𝐴 )
29 2 6 3 hlatlej1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) → 𝑟 ≤ ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) )
30 27 25 28 29 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ) ) ∧ 𝑟 ≠ 𝑃 ) → 𝑟 ≤ ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) )
31 simpl3r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ) ) ∧ 𝑟 ≠ 𝑃 ) → 𝑋 = ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) )
32 30 31 breqtrrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ) ) ∧ 𝑟 ≠ 𝑃 ) → 𝑟 ≤ 𝑋 )
33 neeq1 ⊢ ( 𝑞 = 𝑟 → ( 𝑞 ≠ 𝑃 ↔ 𝑟 ≠ 𝑃 ) )
34 breq1 ⊢ ( 𝑞 = 𝑟 → ( 𝑞 ≤ 𝑋 ↔ 𝑟 ≤ 𝑋 ) )
35 33 34 anbi12d ⊢ ( 𝑞 = 𝑟 → ( ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≤ 𝑋 ) ↔ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≤ 𝑋 ) ) )
36 35 rspcev ⊢ ( ( 𝑟 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≤ 𝑋 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≤ 𝑋 ) )
37 25 26 32 36 syl12anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ) ) ∧ 𝑟 ≠ 𝑃 ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≤ 𝑋 ) )
38 24 37 pm2.61dane ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≤ 𝑋 ) )
39 38 3exp ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) → ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≤ 𝑋 ) ) ) )
40 39 rexlimdvv ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) → ( ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑟 ≠ 𝑠 ∧ 𝑋 = ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≤ 𝑋 ) ) )
41 8 40 mpd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≤ 𝑋 ) )