Metamath Proof Explorer

Theorem cvrat

Description: A nonzero Hilbert lattice element less than the join of two atoms is an atom. ( atcvati analog.) (Contributed by NM, 22-Nov-2011)

Ref Expression
Hypotheses cvrat.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cvrat.s ⊢ < = ( lt ‘ 𝐾 )
cvrat.j ⊢ ∨ = ( join ‘ 𝐾 )
cvrat.z ⊢ 0 = ( 0. ‘ 𝐾 )
cvrat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion cvrat ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( 𝑋 ≠ 0 ∧ 𝑋 < ( 𝑃 ∨ 𝑄 ) ) → 𝑋 ∈ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 cvrat.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cvrat.s ⊢ < = ( lt ‘ 𝐾 )
3 cvrat.j ⊢ ∨ = ( join ‘ 𝐾 )
4 cvrat.z ⊢ 0 = ( 0. ‘ 𝐾 )
5 cvrat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6 1 2 3 4 5 cvratlem ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ ( 𝑋 ≠ 0 ∧ 𝑋 < ( 𝑃 ∨ 𝑄 ) ) ) → ( ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 → 𝑋 ∈ 𝐴 ) )
7 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
8 7 adantr ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝐾 ∈ Lat )
9 simpr2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝑃 ∈ 𝐴 )
10 1 5 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵 )
11 9 10 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝑃 ∈ 𝐵 )
12 simpr3 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝑄 ∈ 𝐴 )
13 1 5 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵 )
14 12 13 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝑄 ∈ 𝐵 )
15 1 3 latjcom ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑄 ∨ 𝑃 ) )
16 8 11 14 15 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑄 ∨ 𝑃 ) )
17 16 breq2d ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑋 < ( 𝑃 ∨ 𝑄 ) ↔ 𝑋 < ( 𝑄 ∨ 𝑃 ) ) )
18 17 anbi2d ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( 𝑋 ≠ 0 ∧ 𝑋 < ( 𝑃 ∨ 𝑄 ) ) ↔ ( 𝑋 ≠ 0 ∧ 𝑋 < ( 𝑄 ∨ 𝑃 ) ) ) )
19 simpl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝐾 ∈ HL )
20 simpr1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝑋 ∈ 𝐵 )
21 1 2 3 4 5 cvratlem ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) ) ∧ ( 𝑋 ≠ 0 ∧ 𝑋 < ( 𝑄 ∨ 𝑃 ) ) ) → ( ¬ 𝑄 ( le ‘ 𝐾 ) 𝑋 → 𝑋 ∈ 𝐴 ) )
22 21 ex ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) ) → ( ( 𝑋 ≠ 0 ∧ 𝑋 < ( 𝑄 ∨ 𝑃 ) ) → ( ¬ 𝑄 ( le ‘ 𝐾 ) 𝑋 → 𝑋 ∈ 𝐴 ) ) )
23 19 20 12 9 22 syl13anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( 𝑋 ≠ 0 ∧ 𝑋 < ( 𝑄 ∨ 𝑃 ) ) → ( ¬ 𝑄 ( le ‘ 𝐾 ) 𝑋 → 𝑋 ∈ 𝐴 ) ) )
24 18 23 sylbid ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( 𝑋 ≠ 0 ∧ 𝑋 < ( 𝑃 ∨ 𝑄 ) ) → ( ¬ 𝑄 ( le ‘ 𝐾 ) 𝑋 → 𝑋 ∈ 𝐴 ) ) )
25 24 imp ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ ( 𝑋 ≠ 0 ∧ 𝑋 < ( 𝑃 ∨ 𝑄 ) ) ) → ( ¬ 𝑄 ( le ‘ 𝐾 ) 𝑋 → 𝑋 ∈ 𝐴 ) )
26 hlpos ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Poset )
27 26 adantr ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝐾 ∈ Poset )
28 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ) → ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 )
29 8 11 14 28 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 )
30 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
31 1 30 2 pltnle ⊢ ( ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 ) ∧ 𝑋 < ( 𝑃 ∨ 𝑄 ) ) → ¬ ( 𝑃 ∨ 𝑄 ) ( le ‘ 𝐾 ) 𝑋 )
32 31 ex ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 ) → ( 𝑋 < ( 𝑃 ∨ 𝑄 ) → ¬ ( 𝑃 ∨ 𝑄 ) ( le ‘ 𝐾 ) 𝑋 ) )
33 27 20 29 32 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑋 < ( 𝑃 ∨ 𝑄 ) → ¬ ( 𝑃 ∨ 𝑄 ) ( le ‘ 𝐾 ) 𝑋 ) )
34 1 30 3 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑃 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑄 ( le ‘ 𝐾 ) 𝑋 ) ↔ ( 𝑃 ∨ 𝑄 ) ( le ‘ 𝐾 ) 𝑋 ) )
35 8 11 14 20 34 syl13anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( 𝑃 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑄 ( le ‘ 𝐾 ) 𝑋 ) ↔ ( 𝑃 ∨ 𝑄 ) ( le ‘ 𝐾 ) 𝑋 ) )
36 35 biimpd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( 𝑃 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑄 ( le ‘ 𝐾 ) 𝑋 ) → ( 𝑃 ∨ 𝑄 ) ( le ‘ 𝐾 ) 𝑋 ) )
37 33 36 nsyld ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑋 < ( 𝑃 ∨ 𝑄 ) → ¬ ( 𝑃 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑄 ( le ‘ 𝐾 ) 𝑋 ) ) )
38 ianor ⊢ ( ¬ ( 𝑃 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑄 ( le ‘ 𝐾 ) 𝑋 ) ↔ ( ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 ∨ ¬ 𝑄 ( le ‘ 𝐾 ) 𝑋 ) )
39 37 38 imbitrdi ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑋 < ( 𝑃 ∨ 𝑄 ) → ( ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 ∨ ¬ 𝑄 ( le ‘ 𝐾 ) 𝑋 ) ) )
40 39 imp ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑋 < ( 𝑃 ∨ 𝑄 ) ) → ( ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 ∨ ¬ 𝑄 ( le ‘ 𝐾 ) 𝑋 ) )
41 40 adantrl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ ( 𝑋 ≠ 0 ∧ 𝑋 < ( 𝑃 ∨ 𝑄 ) ) ) → ( ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 ∨ ¬ 𝑄 ( le ‘ 𝐾 ) 𝑋 ) )
42 6 25 41 mpjaod ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ ( 𝑋 ≠ 0 ∧ 𝑋 < ( 𝑃 ∨ 𝑄 ) ) ) → 𝑋 ∈ 𝐴 )
43 42 ex ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( 𝑋 ≠ 0 ∧ 𝑋 < ( 𝑃 ∨ 𝑄 ) ) → 𝑋 ∈ 𝐴 ) )