Metamath Proof Explorer


Theorem isatl

Description: The predicate "is an atomic lattice." Every nonzero element is less than or equal to an atom. (Contributed by NM, 18-Sep-2011) (Revised by NM, 14-Sep-2018)

Ref Expression
Hypotheses isatlat.b 𝐵 = ( Base ‘ 𝐾 )
isatlat.g 𝐺 = ( glb ‘ 𝐾 )
isatlat.l = ( le ‘ 𝐾 )
isatlat.z 0 = ( 0. ‘ 𝐾 )
isatlat.a 𝐴 = ( Atoms ‘ 𝐾 )
Assertion isatl ( 𝐾 ∈ AtLat ↔ ( 𝐾 ∈ Lat ∧ 𝐵 ∈ dom 𝐺 ∧ ∀ 𝑥𝐵 ( 𝑥0 → ∃ 𝑦𝐴 𝑦 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 isatlat.b 𝐵 = ( Base ‘ 𝐾 )
2 isatlat.g 𝐺 = ( glb ‘ 𝐾 )
3 isatlat.l = ( le ‘ 𝐾 )
4 isatlat.z 0 = ( 0. ‘ 𝐾 )
5 isatlat.a 𝐴 = ( Atoms ‘ 𝐾 )
6 fveq2 ( 𝑘 = 𝐾 → ( Base ‘ 𝑘 ) = ( Base ‘ 𝐾 ) )
7 6 1 eqtr4di ( 𝑘 = 𝐾 → ( Base ‘ 𝑘 ) = 𝐵 )
8 fveq2 ( 𝑘 = 𝐾 → ( glb ‘ 𝑘 ) = ( glb ‘ 𝐾 ) )
9 8 2 eqtr4di ( 𝑘 = 𝐾 → ( glb ‘ 𝑘 ) = 𝐺 )
10 9 dmeqd ( 𝑘 = 𝐾 → dom ( glb ‘ 𝑘 ) = dom 𝐺 )
11 7 10 eleq12d ( 𝑘 = 𝐾 → ( ( Base ‘ 𝑘 ) ∈ dom ( glb ‘ 𝑘 ) ↔ 𝐵 ∈ dom 𝐺 ) )
12 fveq2 ( 𝑘 = 𝐾 → ( 0. ‘ 𝑘 ) = ( 0. ‘ 𝐾 ) )
13 12 4 eqtr4di ( 𝑘 = 𝐾 → ( 0. ‘ 𝑘 ) = 0 )
14 13 neeq2d ( 𝑘 = 𝐾 → ( 𝑥 ≠ ( 0. ‘ 𝑘 ) ↔ 𝑥0 ) )
15 fveq2 ( 𝑘 = 𝐾 → ( Atoms ‘ 𝑘 ) = ( Atoms ‘ 𝐾 ) )
16 15 5 eqtr4di ( 𝑘 = 𝐾 → ( Atoms ‘ 𝑘 ) = 𝐴 )
17 fveq2 ( 𝑘 = 𝐾 → ( le ‘ 𝑘 ) = ( le ‘ 𝐾 ) )
18 17 3 eqtr4di ( 𝑘 = 𝐾 → ( le ‘ 𝑘 ) = )
19 18 breqd ( 𝑘 = 𝐾 → ( 𝑦 ( le ‘ 𝑘 ) 𝑥𝑦 𝑥 ) )
20 16 19 rexeqbidv ( 𝑘 = 𝐾 → ( ∃ 𝑦 ∈ ( Atoms ‘ 𝑘 ) 𝑦 ( le ‘ 𝑘 ) 𝑥 ↔ ∃ 𝑦𝐴 𝑦 𝑥 ) )
21 14 20 imbi12d ( 𝑘 = 𝐾 → ( ( 𝑥 ≠ ( 0. ‘ 𝑘 ) → ∃ 𝑦 ∈ ( Atoms ‘ 𝑘 ) 𝑦 ( le ‘ 𝑘 ) 𝑥 ) ↔ ( 𝑥0 → ∃ 𝑦𝐴 𝑦 𝑥 ) ) )
22 7 21 raleqbidv ( 𝑘 = 𝐾 → ( ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ≠ ( 0. ‘ 𝑘 ) → ∃ 𝑦 ∈ ( Atoms ‘ 𝑘 ) 𝑦 ( le ‘ 𝑘 ) 𝑥 ) ↔ ∀ 𝑥𝐵 ( 𝑥0 → ∃ 𝑦𝐴 𝑦 𝑥 ) ) )
23 11 22 anbi12d ( 𝑘 = 𝐾 → ( ( ( Base ‘ 𝑘 ) ∈ dom ( glb ‘ 𝑘 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ≠ ( 0. ‘ 𝑘 ) → ∃ 𝑦 ∈ ( Atoms ‘ 𝑘 ) 𝑦 ( le ‘ 𝑘 ) 𝑥 ) ) ↔ ( 𝐵 ∈ dom 𝐺 ∧ ∀ 𝑥𝐵 ( 𝑥0 → ∃ 𝑦𝐴 𝑦 𝑥 ) ) ) )
24 df-atl AtLat = { 𝑘 ∈ Lat ∣ ( ( Base ‘ 𝑘 ) ∈ dom ( glb ‘ 𝑘 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ≠ ( 0. ‘ 𝑘 ) → ∃ 𝑦 ∈ ( Atoms ‘ 𝑘 ) 𝑦 ( le ‘ 𝑘 ) 𝑥 ) ) }
25 23 24 elrab2 ( 𝐾 ∈ AtLat ↔ ( 𝐾 ∈ Lat ∧ ( 𝐵 ∈ dom 𝐺 ∧ ∀ 𝑥𝐵 ( 𝑥0 → ∃ 𝑦𝐴 𝑦 𝑥 ) ) ) )
26 3anass ( ( 𝐾 ∈ Lat ∧ 𝐵 ∈ dom 𝐺 ∧ ∀ 𝑥𝐵 ( 𝑥0 → ∃ 𝑦𝐴 𝑦 𝑥 ) ) ↔ ( 𝐾 ∈ Lat ∧ ( 𝐵 ∈ dom 𝐺 ∧ ∀ 𝑥𝐵 ( 𝑥0 → ∃ 𝑦𝐴 𝑦 𝑥 ) ) ) )
27 25 26 bitr4i ( 𝐾 ∈ AtLat ↔ ( 𝐾 ∈ Lat ∧ 𝐵 ∈ dom 𝐺 ∧ ∀ 𝑥𝐵 ( 𝑥0 → ∃ 𝑦𝐴 𝑦 𝑥 ) ) )