Metamath Proof Explorer

Theorem 1cvratlt

Description: An atom less than or equal to an element covered by 1 is less than the element. (Contributed by NM, 7-May-2012)

Ref Expression
Hypotheses 1cvratlt.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
1cvratlt.l ⊢ ≤ = ( le ‘ 𝐾 )
1cvratlt.s ⊢ < = ( lt ‘ 𝐾 )
1cvratlt.u ⊢ 1 = ( 1. ‘ 𝐾 )
1cvratlt.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
1cvratlt.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion 1cvratlt ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 1 ∧ 𝑃 ≤ 𝑋 ) ) → 𝑃 < 𝑋 )

Proof

Step Hyp Ref Expression
1 1cvratlt.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 1cvratlt.l ⊢ ≤ = ( le ‘ 𝐾 )
3 1cvratlt.s ⊢ < = ( lt ‘ 𝐾 )
4 1cvratlt.u ⊢ 1 = ( 1. ‘ 𝐾 )
5 1cvratlt.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
6 1cvratlt.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
7 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 1 ∧ 𝑃 ≤ 𝑋 ) ) → 𝐾 ∈ HL )
8 simpl3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 1 ∧ 𝑃 ≤ 𝑋 ) ) → 𝑋 ∈ 𝐵 )
9 simprl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 1 ∧ 𝑃 ≤ 𝑋 ) ) → 𝑋 𝐶 1 )
10 1 3 4 5 6 1cvratex ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) → ∃ 𝑞 ∈ 𝐴 𝑞 < 𝑋 )
11 7 8 9 10 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 1 ∧ 𝑃 ≤ 𝑋 ) ) → ∃ 𝑞 ∈ 𝐴 𝑞 < 𝑋 )
12 simp1l1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 1 ∧ 𝑃 ≤ 𝑋 ) ) ∧ 𝑞 ∈ 𝐴 ∧ 𝑞 < 𝑋 ) → 𝐾 ∈ HL )
13 simp1l2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 1 ∧ 𝑃 ≤ 𝑋 ) ) ∧ 𝑞 ∈ 𝐴 ∧ 𝑞 < 𝑋 ) → 𝑃 ∈ 𝐴 )
14 simp2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 1 ∧ 𝑃 ≤ 𝑋 ) ) ∧ 𝑞 ∈ 𝐴 ∧ 𝑞 < 𝑋 ) → 𝑞 ∈ 𝐴 )
15 simp1l3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 1 ∧ 𝑃 ≤ 𝑋 ) ) ∧ 𝑞 ∈ 𝐴 ∧ 𝑞 < 𝑋 ) → 𝑋 ∈ 𝐵 )
16 simp1rr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 1 ∧ 𝑃 ≤ 𝑋 ) ) ∧ 𝑞 ∈ 𝐴 ∧ 𝑞 < 𝑋 ) → 𝑃 ≤ 𝑋 )
17 simp3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 1 ∧ 𝑃 ≤ 𝑋 ) ) ∧ 𝑞 ∈ 𝐴 ∧ 𝑞 < 𝑋 ) → 𝑞 < 𝑋 )
18 1 2 3 6 atlelt ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑞 < 𝑋 ) ) → 𝑃 < 𝑋 )
19 12 13 14 15 16 17 18 syl132anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 1 ∧ 𝑃 ≤ 𝑋 ) ) ∧ 𝑞 ∈ 𝐴 ∧ 𝑞 < 𝑋 ) → 𝑃 < 𝑋 )
20 19 rexlimdv3a ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 1 ∧ 𝑃 ≤ 𝑋 ) ) → ( ∃ 𝑞 ∈ 𝐴 𝑞 < 𝑋 → 𝑃 < 𝑋 ) )
21 11 20 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 1 ∧ 𝑃 ≤ 𝑋 ) ) → 𝑃 < 𝑋 )