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 ∧ 𝑋𝑃𝑌𝑃 ) ∧ 𝑋 𝐶 ( 𝑋 𝑌 ) ) → ( 𝑋 𝑌 ) ∈ 𝑁 )