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

Metamath Proof Explorer

Theorem lncvrat

Description: A line covers the atoms it contains. (Contributed by NM, 30-Apr-2012)

Ref Expression
Hypotheses lncvrat.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
lncvrat.l ⊢ ≤ = ( le ‘ 𝐾 )
lncvrat.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
lncvrat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
lncvrat.n ⊢ 𝑁 = ( Lines ‘ 𝐾 )
lncvrat.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
Assertion lncvrat ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋 ) ) → 𝑃 𝐶 𝑋 )

Proof

Step Hyp Ref Expression
1 lncvrat.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 lncvrat.l ⊢ ≤ = ( le ‘ 𝐾 )
3 lncvrat.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
4 lncvrat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 lncvrat.n ⊢ 𝑁 = ( Lines ‘ 𝐾 )
6 lncvrat.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
7 simprl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋 ) ) → ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 )
8 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋 ) ) → 𝐾 ∈ HL )
9 simpl2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋 ) ) → 𝑋 ∈ 𝐵 )
10 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
11 1 10 4 5 6 isline3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ↔ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) )
12 8 9 11 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋 ) ) → ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ↔ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) )
13 7 12 mpbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋 ) ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) )
14 simp1l1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) → 𝐾 ∈ HL )
15 simp1l3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) → 𝑃 ∈ 𝐴 )
16 simp2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) → 𝑞 ∈ 𝐴 )
17 simp2r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) → 𝑟 ∈ 𝐴 )
18 simp3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) → 𝑞 ≠ 𝑟 )
19 simp1rr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) → 𝑃 ≤ 𝑋 )
20 simp3r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) → 𝑋 = ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) )
21 19 20 breqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) → 𝑃 ≤ ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) )
22 2 10 3 4 atcvrj2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑃 ≤ ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) → 𝑃 𝐶 ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) )
23 14 15 16 17 18 21 22 syl132anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) → 𝑃 𝐶 ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) )
24 23 20 breqtrrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) → 𝑃 𝐶 𝑋 )
25 24 3exp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋 ) ) → ( ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) → ( ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) → 𝑃 𝐶 𝑋 ) ) )
26 25 rexlimdvv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋 ) ) → ( ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) → 𝑃 𝐶 𝑋 ) )
27 13 26 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑀 ‘ 𝑋 ) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋 ) ) → 𝑃 𝐶 𝑋 )