Metamath Proof Explorer

Theorem 2lplnm2N

Description: The meet of two different lattice planes in a lattice volume is a lattice line. (Contributed by NM, 12-Jul-2012) (New usage is discouraged.)

Ref Expression
Hypotheses 2lplnm2.l ⊢ ≤ = ( le ‘ 𝐾 )
2lplnm2.m ⊢ ∧ = ( meet ‘ 𝐾 )
2lplnm2.a ⊢ 𝑁 = ( LLines ‘ 𝐾 )
2lplnm2.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
2lplnm2.v ⊢ 𝑉 = ( LVols ‘ 𝐾 )
Assertion 2lplnm2N ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝑁 )

Proof

Step Hyp Ref Expression
1 2lplnm2.l ⊢ ≤ = ( le ‘ 𝐾 )
2 2lplnm2.m ⊢ ∧ = ( meet ‘ 𝐾 )
3 2lplnm2.a ⊢ 𝑁 = ( LLines ‘ 𝐾 )
4 2lplnm2.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
5 2lplnm2.v ⊢ 𝑉 = ( LVols ‘ 𝐾 )
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 lplnbase ⊢ ( 𝑋 ∈ 𝑃 → 𝑋 ∈ ( Base ‘ 𝐾 ) )
13 10 12 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
14 11 4 lplnbase ⊢ ( 𝑌 ∈ 𝑃 → 𝑌 ∈ ( 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 2lplnj ⊢ ( ( 𝐾 ∈ 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 lplncvrlvol2 ⊢ ( ( ( 𝐾 ∈ 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 llncvrlpln ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∧ 𝑌 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑋 ∧ 𝑌 ) ( ⋖ ‘ 𝐾 ) 𝑌 ) → ( ( 𝑋 ∧ 𝑌 ) ∈ 𝑁 ↔ 𝑌 ∈ 𝑃 ) )
31 7 17 15 29 30 syl31anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( ( 𝑋 ∧ 𝑌 ) ∈ 𝑁 ↔ 𝑌 ∈ 𝑃 ) )
32 6 31 mpbird ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝑁 )