Metamath Proof Explorer

Theorem 2llnm2N

Description: The meet of two different lattice lines in a lattice plane is an atom. (Contributed by NM, 5-Jul-2012) (New usage is discouraged.)

Ref Expression
Hypotheses 2llnm2.l ⊢ ≤ = ( le ‘ 𝐾 )
2llnm2.m ⊢ ∧ = ( meet ‘ 𝐾 )
2llnm2.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2llnm2.n ⊢ 𝑁 = ( LLines ‘ 𝐾 )
2llnm2.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
Assertion 2llnm2N ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 2llnm2.l ⊢ ≤ = ( le ‘ 𝐾 )
2 2llnm2.m ⊢ ∧ = ( meet ‘ 𝐾 )
3 2llnm2.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 2llnm2.n ⊢ 𝑁 = ( LLines ‘ 𝐾 )
5 2llnm2.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
6 simp22 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → 𝑌 ∈ 𝑁 )
7 simp1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → 𝐾 ∈ HL )
8 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
9 8 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → 𝐾 ∈ Lat )
10 simp21 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → 𝑋 ∈ 𝑁 )
11 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
12 11 4 llnbase ⊢ ( 𝑋 ∈ 𝑁 → 𝑋 ∈ ( Base ‘ 𝐾 ) )
13 10 12 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
14 11 4 llnbase ⊢ ( 𝑌 ∈ 𝑁 → 𝑌 ∈ ( Base ‘ 𝐾 ) )
15 6 14 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → 𝑌 ∈ ( Base ‘ 𝐾 ) )
16 11 2 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋 ∧ 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
17 9 13 15 16 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝑋 ∧ 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
18 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
19 1 18 4 5 2llnjN ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) = 𝑊 )
20 simp23 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → 𝑊 ∈ 𝑃 )
21 19 20 eqeltrd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ∈ 𝑃 )
22 11 1 18 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) → 𝑋 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) )
23 9 13 15 22 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → 𝑋 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) )
24 eqid ⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
25 1 24 4 5 llncvrlpln2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ∈ 𝑃 ) ∧ 𝑋 ≤ ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) → 𝑋 ( ⋖ ‘ 𝐾 ) ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) )
26 7 10 21 23 25 syl31anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → 𝑋 ( ⋖ ‘ 𝐾 ) ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) )
27 11 18 2 24 cvrexch ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑋 ∧ 𝑌 ) ( ⋖ ‘ 𝐾 ) 𝑌 ↔ 𝑋 ( ⋖ ‘ 𝐾 ) ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) )
28 7 13 15 27 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( ( 𝑋 ∧ 𝑌 ) ( ⋖ ‘ 𝐾 ) 𝑌 ↔ 𝑋 ( ⋖ ‘ 𝐾 ) ( 𝑋 ( join ‘ 𝐾 ) 𝑌 ) ) )
29 26 28 mpbird ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝑋 ∧ 𝑌 ) ( ⋖ ‘ 𝐾 ) 𝑌 )
30 11 24 3 4 atcvrlln ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∧ 𝑌 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑋 ∧ 𝑌 ) ( ⋖ ‘ 𝐾 ) 𝑌 ) → ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ↔ 𝑌 ∈ 𝑁 ) )
31 7 17 15 29 30 syl31anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ↔ 𝑌 ∈ 𝑁 ) )
32 6 31 mpbird ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 )