Metamath Proof Explorer

Theorem atnle

Description: Two ways of expressing "an atom is not less than or equal to a lattice element." ( atnssm0 analog.) (Contributed by NM, 5-Nov-2012)

Ref Expression
Hypotheses atnle.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
atnle.l ⊢ ≤ = ( le ‘ 𝐾 )
atnle.m ⊢ ∧ = ( meet ‘ 𝐾 )
atnle.z ⊢ 0 = ( 0. ‘ 𝐾 )
atnle.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion atnle ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( ¬ 𝑃 ≤ 𝑋 ↔ ( 𝑃 ∧ 𝑋 ) = 0 ) )

Proof

Step Hyp Ref Expression
1 atnle.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 atnle.l ⊢ ≤ = ( le ‘ 𝐾 )
3 atnle.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 atnle.z ⊢ 0 = ( 0. ‘ 𝐾 )
5 atnle.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6 simpl1 ⊢ ( ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∧ 𝑋 ) ≠ 0 ) → 𝐾 ∈ AtLat )
7 atllat ⊢ ( 𝐾 ∈ AtLat → 𝐾 ∈ Lat )
8 7 3ad2ant1 ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → 𝐾 ∈ Lat )
9 1 5 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵 )
10 9 3ad2ant2 ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → 𝑃 ∈ 𝐵 )
11 simp3 ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
12 1 3 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑃 ∧ 𝑋 ) ∈ 𝐵 )
13 8 10 11 12 syl3anc ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑃 ∧ 𝑋 ) ∈ 𝐵 )
14 13 adantr ⊢ ( ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∧ 𝑋 ) ≠ 0 ) → ( 𝑃 ∧ 𝑋 ) ∈ 𝐵 )
15 simpr ⊢ ( ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∧ 𝑋 ) ≠ 0 ) → ( 𝑃 ∧ 𝑋 ) ≠ 0 )
16 1 2 4 5 atlex ⊢ ( ( 𝐾 ∈ AtLat ∧ ( 𝑃 ∧ 𝑋 ) ∈ 𝐵 ∧ ( 𝑃 ∧ 𝑋 ) ≠ 0 ) → ∃ 𝑦 ∈ 𝐴 𝑦 ≤ ( 𝑃 ∧ 𝑋 ) )
17 6 14 15 16 syl3anc ⊢ ( ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∧ 𝑋 ) ≠ 0 ) → ∃ 𝑦 ∈ 𝐴 𝑦 ≤ ( 𝑃 ∧ 𝑋 ) )
18 simpl1 ⊢ ( ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) → 𝐾 ∈ AtLat )
19 18 7 syl ⊢ ( ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) → 𝐾 ∈ Lat )
20 1 5 atbase ⊢ ( 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵 )
21 20 adantl ⊢ ( ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ 𝐵 )
22 simpl2 ⊢ ( ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑃 ∈ 𝐴 )
23 22 9 syl ⊢ ( ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑃 ∈ 𝐵 )
24 simpl3 ⊢ ( ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
25 1 2 3 latlem12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑃 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑦 ≤ 𝑃 ∧ 𝑦 ≤ 𝑋 ) ↔ 𝑦 ≤ ( 𝑃 ∧ 𝑋 ) ) )
26 19 21 23 24 25 syl13anc ⊢ ( ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑦 ≤ 𝑃 ∧ 𝑦 ≤ 𝑋 ) ↔ 𝑦 ≤ ( 𝑃 ∧ 𝑋 ) ) )
27 simpr ⊢ ( ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 )
28 2 5 atcmp ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑦 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑦 ≤ 𝑃 ↔ 𝑦 = 𝑃 ) )
29 18 27 22 28 syl3anc ⊢ ( ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 ≤ 𝑃 ↔ 𝑦 = 𝑃 ) )
30 breq1 ⊢ ( 𝑦 = 𝑃 → ( 𝑦 ≤ 𝑋 ↔ 𝑃 ≤ 𝑋 ) )
31 30 biimpd ⊢ ( 𝑦 = 𝑃 → ( 𝑦 ≤ 𝑋 → 𝑃 ≤ 𝑋 ) )
32 29 31 biimtrdi ⊢ ( ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 ≤ 𝑃 → ( 𝑦 ≤ 𝑋 → 𝑃 ≤ 𝑋 ) ) )
33 32 impd ⊢ ( ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑦 ≤ 𝑃 ∧ 𝑦 ≤ 𝑋 ) → 𝑃 ≤ 𝑋 ) )
34 26 33 sylbird ⊢ ( ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 ≤ ( 𝑃 ∧ 𝑋 ) → 𝑃 ≤ 𝑋 ) )
35 34 adantlr ⊢ ( ( ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∧ 𝑋 ) ≠ 0 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 ≤ ( 𝑃 ∧ 𝑋 ) → 𝑃 ≤ 𝑋 ) )
36 35 rexlimdva ⊢ ( ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∧ 𝑋 ) ≠ 0 ) → ( ∃ 𝑦 ∈ 𝐴 𝑦 ≤ ( 𝑃 ∧ 𝑋 ) → 𝑃 ≤ 𝑋 ) )
37 17 36 mpd ⊢ ( ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∧ 𝑋 ) ≠ 0 ) → 𝑃 ≤ 𝑋 )
38 37 ex ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑃 ∧ 𝑋 ) ≠ 0 → 𝑃 ≤ 𝑋 ) )
39 38 necon1bd ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( ¬ 𝑃 ≤ 𝑋 → ( 𝑃 ∧ 𝑋 ) = 0 ) )
40 4 5 atn0 ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ) → 𝑃 ≠ 0 )
41 40 3adant3 ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → 𝑃 ≠ 0 )
42 1 2 3 latleeqm1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑃 ≤ 𝑋 ↔ ( 𝑃 ∧ 𝑋 ) = 𝑃 ) )
43 8 10 11 42 syl3anc ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑃 ≤ 𝑋 ↔ ( 𝑃 ∧ 𝑋 ) = 𝑃 ) )
44 43 adantr ⊢ ( ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∧ 𝑋 ) = 0 ) → ( 𝑃 ≤ 𝑋 ↔ ( 𝑃 ∧ 𝑋 ) = 𝑃 ) )
45 eqeq1 ⊢ ( ( 𝑃 ∧ 𝑋 ) = 𝑃 → ( ( 𝑃 ∧ 𝑋 ) = 0 ↔ 𝑃 = 0 ) )
46 45 biimpcd ⊢ ( ( 𝑃 ∧ 𝑋 ) = 0 → ( ( 𝑃 ∧ 𝑋 ) = 𝑃 → 𝑃 = 0 ) )
47 46 adantl ⊢ ( ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∧ 𝑋 ) = 0 ) → ( ( 𝑃 ∧ 𝑋 ) = 𝑃 → 𝑃 = 0 ) )
48 44 47 sylbid ⊢ ( ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∧ 𝑋 ) = 0 ) → ( 𝑃 ≤ 𝑋 → 𝑃 = 0 ) )
49 48 necon3ad ⊢ ( ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∧ 𝑋 ) = 0 ) → ( 𝑃 ≠ 0 → ¬ 𝑃 ≤ 𝑋 ) )
50 49 ex ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑃 ∧ 𝑋 ) = 0 → ( 𝑃 ≠ 0 → ¬ 𝑃 ≤ 𝑋 ) ) )
51 41 50 mpid ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑃 ∧ 𝑋 ) = 0 → ¬ 𝑃 ≤ 𝑋 ) )
52 39 51 impbid ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( ¬ 𝑃 ≤ 𝑋 ↔ ( 𝑃 ∧ 𝑋 ) = 0 ) )