Metamath Proof Explorer

Theorem lplnle

Description: Any element greater than 0 and not an atom and not a lattice line majorizes a lattice plane. (Contributed by NM, 28-Jun-2012)

Ref Expression
Hypotheses lplnle.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
lplnle.l ⊢ ≤ = ( le ‘ 𝐾 )
lplnle.z ⊢ 0 = ( 0. ‘ 𝐾 )
lplnle.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
lplnle.n ⊢ 𝑁 = ( LLines ‘ 𝐾 )
lplnle.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
Assertion lplnle ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑁 ) ) → ∃ 𝑦 ∈ 𝑃 𝑦 ≤ 𝑋 )

Proof

Step Hyp Ref Expression
1 lplnle.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 lplnle.l ⊢ ≤ = ( le ‘ 𝐾 )
3 lplnle.z ⊢ 0 = ( 0. ‘ 𝐾 )
4 lplnle.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 lplnle.n ⊢ 𝑁 = ( LLines ‘ 𝐾 )
6 lplnle.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
7 1 2 3 4 5 llnle ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ) ) → ∃ 𝑧 ∈ 𝑁 𝑧 ≤ 𝑋 )
8 7 3adantr3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑁 ) ) → ∃ 𝑧 ∈ 𝑁 𝑧 ≤ 𝑋 )
9 simp1ll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑁 ) ) ∧ 𝑧 ∈ 𝑁 ∧ 𝑧 ≤ 𝑋 ) → 𝐾 ∈ HL )
10 1 5 llnbase ⊢ ( 𝑧 ∈ 𝑁 → 𝑧 ∈ 𝐵 )
11 10 3ad2ant2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑁 ) ) ∧ 𝑧 ∈ 𝑁 ∧ 𝑧 ≤ 𝑋 ) → 𝑧 ∈ 𝐵 )
12 simp1lr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑁 ) ) ∧ 𝑧 ∈ 𝑁 ∧ 𝑧 ≤ 𝑋 ) → 𝑋 ∈ 𝐵 )
13 simp3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑁 ) ) ∧ 𝑧 ∈ 𝑁 ∧ 𝑧 ≤ 𝑋 ) → 𝑧 ≤ 𝑋 )
14 simp2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑁 ) ) ∧ 𝑧 ∈ 𝑁 ∧ 𝑧 ≤ 𝑋 ) → 𝑧 ∈ 𝑁 )
15 simp1r3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑁 ) ) ∧ 𝑧 ∈ 𝑁 ∧ 𝑧 ≤ 𝑋 ) → ¬ 𝑋 ∈ 𝑁 )
16 nelne2 ⊢ ( ( 𝑧 ∈ 𝑁 ∧ ¬ 𝑋 ∈ 𝑁 ) → 𝑧 ≠ 𝑋 )
17 14 15 16 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑁 ) ) ∧ 𝑧 ∈ 𝑁 ∧ 𝑧 ≤ 𝑋 ) → 𝑧 ≠ 𝑋 )
18 eqid ⊢ ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 )
19 2 18 pltval ⊢ ( ( 𝐾 ∈ HL ∧ 𝑧 ∈ 𝑁 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑧 ( lt ‘ 𝐾 ) 𝑋 ↔ ( 𝑧 ≤ 𝑋 ∧ 𝑧 ≠ 𝑋 ) ) )
20 9 14 12 19 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑁 ) ) ∧ 𝑧 ∈ 𝑁 ∧ 𝑧 ≤ 𝑋 ) → ( 𝑧 ( lt ‘ 𝐾 ) 𝑋 ↔ ( 𝑧 ≤ 𝑋 ∧ 𝑧 ≠ 𝑋 ) ) )
21 13 17 20 mpbir2and ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑁 ) ) ∧ 𝑧 ∈ 𝑁 ∧ 𝑧 ≤ 𝑋 ) → 𝑧 ( lt ‘ 𝐾 ) 𝑋 )
22 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
23 eqid ⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
24 1 2 18 22 23 4 hlrelat3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑧 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑧 ( lt ‘ 𝐾 ) 𝑋 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑧 ( ⋖ ‘ 𝐾 ) ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ∧ ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ≤ 𝑋 ) )
25 9 11 12 21 24 syl31anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑁 ) ) ∧ 𝑧 ∈ 𝑁 ∧ 𝑧 ≤ 𝑋 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑧 ( ⋖ ‘ 𝐾 ) ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ∧ ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ≤ 𝑋 ) )
26 simp1ll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑁 ) ) ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑧 ≤ 𝑋 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑧 ( ⋖ ‘ 𝐾 ) ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ∧ ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ≤ 𝑋 ) ) → 𝐾 ∈ HL )
27 26 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑁 ) ) ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑧 ≤ 𝑋 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑧 ( ⋖ ‘ 𝐾 ) ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ∧ ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ≤ 𝑋 ) ) → 𝐾 ∈ Lat )
28 simp21 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑁 ) ) ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑧 ≤ 𝑋 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑧 ( ⋖ ‘ 𝐾 ) ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ∧ ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ≤ 𝑋 ) ) → 𝑧 ∈ 𝑁 )
29 28 10 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑁 ) ) ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑧 ≤ 𝑋 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑧 ( ⋖ ‘ 𝐾 ) ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ∧ ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ≤ 𝑋 ) ) → 𝑧 ∈ 𝐵 )
30 simp23 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑁 ) ) ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑧 ≤ 𝑋 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑧 ( ⋖ ‘ 𝐾 ) ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ∧ ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ≤ 𝑋 ) ) → 𝑝 ∈ 𝐴 )
31 1 4 atbase ⊢ ( 𝑝 ∈ 𝐴 → 𝑝 ∈ 𝐵 )
32 30 31 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑁 ) ) ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑧 ≤ 𝑋 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑧 ( ⋖ ‘ 𝐾 ) ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ∧ ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ≤ 𝑋 ) ) → 𝑝 ∈ 𝐵 )
33 1 22 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑧 ∈ 𝐵 ∧ 𝑝 ∈ 𝐵 ) → ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ∈ 𝐵 )
34 27 29 32 33 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑁 ) ) ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑧 ≤ 𝑋 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑧 ( ⋖ ‘ 𝐾 ) ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ∧ ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ≤ 𝑋 ) ) → ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ∈ 𝐵 )
35 simp3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑁 ) ) ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑧 ≤ 𝑋 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑧 ( ⋖ ‘ 𝐾 ) ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ∧ ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ≤ 𝑋 ) ) → 𝑧 ( ⋖ ‘ 𝐾 ) ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) )
36 1 23 5 6 lplni ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ∈ 𝐵 ∧ 𝑧 ∈ 𝑁 ) ∧ 𝑧 ( ⋖ ‘ 𝐾 ) ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ) → ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ∈ 𝑃 )
37 26 34 28 35 36 syl31anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑁 ) ) ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑧 ≤ 𝑋 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑧 ( ⋖ ‘ 𝐾 ) ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ∧ ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ≤ 𝑋 ) ) → ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ∈ 𝑃 )
38 simp3r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑁 ) ) ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑧 ≤ 𝑋 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑧 ( ⋖ ‘ 𝐾 ) ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ∧ ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ≤ 𝑋 ) ) → ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ≤ 𝑋 )
39 breq1 ⊢ ( 𝑦 = ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) → ( 𝑦 ≤ 𝑋 ↔ ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ≤ 𝑋 ) )
40 39 rspcev ⊢ ( ( ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ∈ 𝑃 ∧ ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ≤ 𝑋 ) → ∃ 𝑦 ∈ 𝑃 𝑦 ≤ 𝑋 )
41 37 38 40 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑁 ) ) ∧ ( 𝑧 ∈ 𝑁 ∧ 𝑧 ≤ 𝑋 ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝑧 ( ⋖ ‘ 𝐾 ) ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ∧ ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ≤ 𝑋 ) ) → ∃ 𝑦 ∈ 𝑃 𝑦 ≤ 𝑋 )
42 41 3exp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑁 ) ) → ( ( 𝑧 ∈ 𝑁 ∧ 𝑧 ≤ 𝑋 ∧ 𝑝 ∈ 𝐴 ) → ( ( 𝑧 ( ⋖ ‘ 𝐾 ) ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ∧ ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ≤ 𝑋 ) → ∃ 𝑦 ∈ 𝑃 𝑦 ≤ 𝑋 ) ) )
43 42 3expd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑁 ) ) → ( 𝑧 ∈ 𝑁 → ( 𝑧 ≤ 𝑋 → ( 𝑝 ∈ 𝐴 → ( ( 𝑧 ( ⋖ ‘ 𝐾 ) ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ∧ ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ≤ 𝑋 ) → ∃ 𝑦 ∈ 𝑃 𝑦 ≤ 𝑋 ) ) ) ) )
44 43 3imp ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑁 ) ) ∧ 𝑧 ∈ 𝑁 ∧ 𝑧 ≤ 𝑋 ) → ( 𝑝 ∈ 𝐴 → ( ( 𝑧 ( ⋖ ‘ 𝐾 ) ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ∧ ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ≤ 𝑋 ) → ∃ 𝑦 ∈ 𝑃 𝑦 ≤ 𝑋 ) ) )
45 44 rexlimdv ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑁 ) ) ∧ 𝑧 ∈ 𝑁 ∧ 𝑧 ≤ 𝑋 ) → ( ∃ 𝑝 ∈ 𝐴 ( 𝑧 ( ⋖ ‘ 𝐾 ) ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ∧ ( 𝑧 ( join ‘ 𝐾 ) 𝑝 ) ≤ 𝑋 ) → ∃ 𝑦 ∈ 𝑃 𝑦 ≤ 𝑋 ) )
46 25 45 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑁 ) ) ∧ 𝑧 ∈ 𝑁 ∧ 𝑧 ≤ 𝑋 ) → ∃ 𝑦 ∈ 𝑃 𝑦 ≤ 𝑋 )
47 46 3exp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑁 ) ) → ( 𝑧 ∈ 𝑁 → ( 𝑧 ≤ 𝑋 → ∃ 𝑦 ∈ 𝑃 𝑦 ≤ 𝑋 ) ) )
48 47 rexlimdv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑁 ) ) → ( ∃ 𝑧 ∈ 𝑁 𝑧 ≤ 𝑋 → ∃ 𝑦 ∈ 𝑃 𝑦 ≤ 𝑋 ) )
49 8 48 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ ¬ 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑁 ) ) → ∃ 𝑦 ∈ 𝑃 𝑦 ≤ 𝑋 )