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 ∧ 𝑋𝐵𝑃𝐴 ) ∧ ( ( 𝑀𝑋 ) ∈ 𝑁𝑃 𝑋 ) ) → ∃ 𝑞𝐴 ( 𝑞𝑃𝑋 = ( 𝑃 𝑞 ) ) )