Metamath Proof Explorer

Theorem atcvrlln2

Description: An atom under a line is covered by it. (Contributed by NM, 2-Jul-2012)

Ref Expression
Hypotheses atcvrlln2.l ⊢ ≤ = ( le ‘ 𝐾 )
atcvrlln2.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
atcvrlln2.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
atcvrlln2.n ⊢ 𝑁 = ( LLines ‘ 𝐾 )
Assertion atcvrlln2 ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ) ∧ 𝑃 ≤ 𝑋 ) → 𝑃 𝐶 𝑋 )

Proof

Step Hyp Ref Expression
1 atcvrlln2.l ⊢ ≤ = ( le ‘ 𝐾 )
2 atcvrlln2.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
3 atcvrlln2.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 atcvrlln2.n ⊢ 𝑁 = ( LLines ‘ 𝐾 )
5 simpl3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ) ∧ 𝑃 ≤ 𝑋 ) → 𝑋 ∈ 𝑁 )
6 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ) ∧ 𝑃 ≤ 𝑋 ) → 𝐾 ∈ HL )
7 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
8 7 4 llnbase ⊢ ( 𝑋 ∈ 𝑁 → 𝑋 ∈ ( Base ‘ 𝐾 ) )
9 5 8 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ) ∧ 𝑃 ≤ 𝑋 ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
10 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
11 7 10 3 4 islln3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋 ∈ 𝑁 ↔ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) )
12 6 9 11 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ) ∧ 𝑃 ≤ 𝑋 ) → ( 𝑋 ∈ 𝑁 ↔ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) )
13 5 12 mpbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ) ∧ 𝑃 ≤ 𝑋 ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) )
14 simp1l1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ) ∧ 𝑃 ≤ 𝑋 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) → 𝐾 ∈ HL )
15 simp1l2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ) ∧ 𝑃 ≤ 𝑋 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) → 𝑃 ∈ 𝐴 )
16 simp2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ) ∧ 𝑃 ≤ 𝑋 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) → 𝑞 ∈ 𝐴 )
17 simp2r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ) ∧ 𝑃 ≤ 𝑋 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) → 𝑟 ∈ 𝐴 )
18 simp3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ) ∧ 𝑃 ≤ 𝑋 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) → 𝑞 ≠ 𝑟 )
19 simp1r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ) ∧ 𝑃 ≤ 𝑋 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) → 𝑃 ≤ 𝑋 )
20 simp3r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ) ∧ 𝑃 ≤ 𝑋 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) → 𝑋 = ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) )
21 19 20 breqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ) ∧ 𝑃 ≤ 𝑋 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) → 𝑃 ≤ ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) )
22 1 10 2 3 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 ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ) ∧ 𝑃 ≤ 𝑋 ) → 𝑃 𝐶 𝑋 )