Metamath Proof Explorer

Theorem 2lplnmN

Description: If the join of two lattice planes covers one of them, their meet is a lattice line. (Contributed by NM, 30-Jun-2012) (New usage is discouraged.)

Ref Expression
Hypotheses 2lplnm.j ⊢ ∨ = ( join ‘ 𝐾 )
2lplnm.m ⊢ ∧ = ( meet ‘ 𝐾 )
2lplnm.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
2lplnm.n ⊢ 𝑁 = ( LLines ‘ 𝐾 )
2lplnm.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
Assertion 2lplnmN ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 𝐶 ( 𝑋 ∨ 𝑌 ) ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝑁 )

Proof

Step Hyp Ref Expression
1 2lplnm.j ⊢ ∨ = ( join ‘ 𝐾 )
2 2lplnm.m ⊢ ∧ = ( meet ‘ 𝐾 )
3 2lplnm.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
4 2lplnm.n ⊢ 𝑁 = ( LLines ‘ 𝐾 )
5 2lplnm.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
6 simpl3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 𝐶 ( 𝑋 ∨ 𝑌 ) ) → 𝑌 ∈ 𝑃 )
7 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 𝐶 ( 𝑋 ∨ 𝑌 ) ) → 𝐾 ∈ HL )
8 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
9 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
10 9 5 lplnbase ⊢ ( 𝑋 ∈ 𝑃 → 𝑋 ∈ ( Base ‘ 𝐾 ) )
11 9 5 lplnbase ⊢ ( 𝑌 ∈ 𝑃 → 𝑌 ∈ ( Base ‘ 𝐾 ) )
12 9 2 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋 ∧ 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
13 8 10 11 12 syl3an ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑋 ∧ 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
14 13 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 𝐶 ( 𝑋 ∨ 𝑌 ) ) → ( 𝑋 ∧ 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
15 11 3ad2ant3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → 𝑌 ∈ ( Base ‘ 𝐾 ) )
16 15 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 𝐶 ( 𝑋 ∨ 𝑌 ) ) → 𝑌 ∈ ( Base ‘ 𝐾 ) )
17 simp1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → 𝐾 ∈ HL )
18 10 3ad2ant2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
19 9 1 2 3 cvrexch ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 ↔ 𝑋 𝐶 ( 𝑋 ∨ 𝑌 ) ) )
20 17 18 15 19 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 ↔ 𝑋 𝐶 ( 𝑋 ∨ 𝑌 ) ) )
21 20 biimpar ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 𝐶 ( 𝑋 ∨ 𝑌 ) ) → ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 )
22 9 3 4 5 llncvrlpln ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∧ 𝑌 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) ∧ ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 ) → ( ( 𝑋 ∧ 𝑌 ) ∈ 𝑁 ↔ 𝑌 ∈ 𝑃 ) )
23 7 14 16 21 22 syl31anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 𝐶 ( 𝑋 ∨ 𝑌 ) ) → ( ( 𝑋 ∧ 𝑌 ) ∈ 𝑁 ↔ 𝑌 ∈ 𝑃 ) )
24 6 23 mpbird ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 𝐶 ( 𝑋 ∨ 𝑌 ) ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝑁 )