This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lnjatN

Description: Given an atom in a line, there is another atom which when joined equals the line. (Contributed by NM, 30-Apr-2012) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 lnjat.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 lnjat.l ⊢ ≤ = ( le ‘ 𝐾 )
3 lnjat.j ⊢ ∨ = ( join ‘ 𝐾 )
4 lnjat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 lnjat.n ⊢ 𝑁 = ( Lines ‘ 𝐾 )
6 lnjat.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
7 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋 ) ) → 𝐾 ∈ HL )
8 simpl2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋 ) ) → 𝑋 ∈ 𝐵 )
9 simprl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋 ) ) → ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 )
10 1 2 4 5 6 lnatexN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≤ 𝑋 ) )
11 7 8 9 10 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≤ 𝑋 ) )
12 simp3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≤ 𝑋 ) ) → 𝑞 ≠ 𝑃 )
13 simp1l1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≤ 𝑋 ) ) → 𝐾 ∈ HL )
14 simp1l2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≤ 𝑋 ) ) → 𝑋 ∈ 𝐵 )
15 simp1rl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≤ 𝑋 ) ) → ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 )
16 simp1l3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≤ 𝑋 ) ) → 𝑃 ∈ 𝐴 )
17 simp2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≤ 𝑋 ) ) → 𝑞 ∈ 𝐴 )
18 12 necomd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≤ 𝑋 ) ) → 𝑃 ≠ 𝑞 )
19 simp1rr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≤ 𝑋 ) ) → 𝑃 ≤ 𝑋 )
20 simp3r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≤ 𝑋 ) ) → 𝑞 ≤ 𝑋 )
21 1 2 3 4 5 6 lneq2at ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ∧ 𝑃 ≠ 𝑞 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑞 ≤ 𝑋 ) ) → 𝑋 = ( 𝑃 ∨ 𝑞 ) )
22 13 14 15 16 17 18 19 20 21 syl332anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≤ 𝑋 ) ) → 𝑋 = ( 𝑃 ∨ 𝑞 ) )
23 12 22 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋 ) ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≤ 𝑋 ) ) → ( 𝑞 ≠ 𝑃 ∧ 𝑋 = ( 𝑃 ∨ 𝑞 ) ) )
24 23 3exp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋 ) ) → ( 𝑞 ∈ 𝐴 → ( ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≤ 𝑋 ) → ( 𝑞 ≠ 𝑃 ∧ 𝑋 = ( 𝑃 ∨ 𝑞 ) ) ) ) )
25 24 reximdvai ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋 ) ) → ( ∃ 𝑞 ∈ 𝐴 ( 𝑞 ≠ 𝑃 ∧ 𝑞 ≤ 𝑋 ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ≠ 𝑃 ∧ 𝑋 = ( 𝑃 ∨ 𝑞 ) ) ) )
26 11 25 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ≠ 𝑃 ∧ 𝑋 = ( 𝑃 ∨ 𝑞 ) ) )