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𝑃 𝑋 ) ) → 𝑃 < 𝑋 )