Metamath Proof Explorer

Theorem lplnexatN

Description: Given a lattice line on a lattice plane, there is an atom whose join with the line equals the plane. (Contributed by NM, 29-Jun-2012) (New usage is discouraged.)

Ref Expression
Hypotheses lplnexat.l ⊢ ≤ = ( le ‘ 𝐾 )
lplnexat.j ⊢ ∨ = ( join ‘ 𝐾 )
lplnexat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
lplnexat.n ⊢ 𝑁 = ( LLines ‘ 𝐾 )
lplnexat.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
Assertion lplnexatN ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁 ) ∧ 𝑌 ≤ 𝑋 ) → ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ≤ 𝑌 ∧ 𝑋 = ( 𝑌 ∨ 𝑞 ) ) )

Proof

Step Hyp Ref Expression
1 lplnexat.l ⊢ ≤ = ( le ‘ 𝐾 )
2 lplnexat.j ⊢ ∨ = ( join ‘ 𝐾 )
3 lplnexat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 lplnexat.n ⊢ 𝑁 = ( LLines ‘ 𝐾 )
5 lplnexat.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
6 simp1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁 ) → 𝐾 ∈ HL )
7 simp3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁 ) → 𝑌 ∈ 𝑁 )
8 simp2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁 ) → 𝑋 ∈ 𝑃 )
9 6 7 8 3jca ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁 ) → ( 𝐾 ∈ HL ∧ 𝑌 ∈ 𝑁 ∧ 𝑋 ∈ 𝑃 ) )
10 eqid ⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
11 1 10 4 5 llncvrlpln2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑌 ∈ 𝑁 ∧ 𝑋 ∈ 𝑃 ) ∧ 𝑌 ≤ 𝑋 ) → 𝑌 ( ⋖ ‘ 𝐾 ) 𝑋 )
12 9 11 sylan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁 ) ∧ 𝑌 ≤ 𝑋 ) → 𝑌 ( ⋖ ‘ 𝐾 ) 𝑋 )
13 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁 ) ∧ 𝑌 ≤ 𝑋 ) → 𝐾 ∈ HL )
14 simpl3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁 ) ∧ 𝑌 ≤ 𝑋 ) → 𝑌 ∈ 𝑁 )
15 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
16 15 4 llnbase ⊢ ( 𝑌 ∈ 𝑁 → 𝑌 ∈ ( Base ‘ 𝐾 ) )
17 14 16 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁 ) ∧ 𝑌 ≤ 𝑋 ) → 𝑌 ∈ ( Base ‘ 𝐾 ) )
18 simpl2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁 ) ∧ 𝑌 ≤ 𝑋 ) → 𝑋 ∈ 𝑃 )
19 15 5 lplnbase ⊢ ( 𝑋 ∈ 𝑃 → 𝑋 ∈ ( Base ‘ 𝐾 ) )
20 18 19 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁 ) ∧ 𝑌 ≤ 𝑋 ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
21 15 1 2 10 3 cvrval3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑌 ( ⋖ ‘ 𝐾 ) 𝑋 ↔ ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ≤ 𝑌 ∧ ( 𝑌 ∨ 𝑞 ) = 𝑋 ) ) )
22 13 17 20 21 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁 ) ∧ 𝑌 ≤ 𝑋 ) → ( 𝑌 ( ⋖ ‘ 𝐾 ) 𝑋 ↔ ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ≤ 𝑌 ∧ ( 𝑌 ∨ 𝑞 ) = 𝑋 ) ) )
23 eqcom ⊢ ( ( 𝑌 ∨ 𝑞 ) = 𝑋 ↔ 𝑋 = ( 𝑌 ∨ 𝑞 ) )
24 23 anbi2i ⊢ ( ( ¬ 𝑞 ≤ 𝑌 ∧ ( 𝑌 ∨ 𝑞 ) = 𝑋 ) ↔ ( ¬ 𝑞 ≤ 𝑌 ∧ 𝑋 = ( 𝑌 ∨ 𝑞 ) ) )
25 24 rexbii ⊢ ( ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ≤ 𝑌 ∧ ( 𝑌 ∨ 𝑞 ) = 𝑋 ) ↔ ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ≤ 𝑌 ∧ 𝑋 = ( 𝑌 ∨ 𝑞 ) ) )
26 22 25 bitrdi ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁 ) ∧ 𝑌 ≤ 𝑋 ) → ( 𝑌 ( ⋖ ‘ 𝐾 ) 𝑋 ↔ ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ≤ 𝑌 ∧ 𝑋 = ( 𝑌 ∨ 𝑞 ) ) ) )
27 12 26 mpbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁 ) ∧ 𝑌 ≤ 𝑋 ) → ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ≤ 𝑌 ∧ 𝑋 = ( 𝑌 ∨ 𝑞 ) ) )