This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem llnmlplnN

Description: The intersection of a line with a plane not containing it is an atom. (Contributed by NM, 29-Jun-2012) (New usage is discouraged.)

Ref Expression
Hypotheses llnmlpln.l ⊢ ≤ = ( le ‘ 𝐾 )
llnmlpln.m ⊢ ∧ = ( meet ‘ 𝐾 )
llnmlpln.z ⊢ 0 = ( 0. ‘ 𝐾 )
llnmlpln.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
llnmlpln.n ⊢ 𝑁 = ( LLines ‘ 𝐾 )
llnmlpln.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
Assertion llnmlplnN ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 llnmlpln.l ⊢ ≤ = ( le ‘ 𝐾 )
2 llnmlpln.m ⊢ ∧ = ( meet ‘ 𝐾 )
3 llnmlpln.z ⊢ 0 = ( 0. ‘ 𝐾 )
4 llnmlpln.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 llnmlpln.n ⊢ 𝑁 = ( LLines ‘ 𝐾 )
6 llnmlpln.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
7 simprl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) → ¬ 𝑋 ≤ 𝑌 )
8 simp11 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → 𝐾 ∈ HL )
9 8 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → 𝐾 ∈ Lat )
10 simp12 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → 𝑋 ∈ 𝑁 )
11 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
12 11 5 llnbase ⊢ ( 𝑋 ∈ 𝑁 → 𝑋 ∈ ( Base ‘ 𝐾 ) )
13 10 12 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
14 simp13 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → 𝑌 ∈ 𝑃 )
15 11 6 lplnbase ⊢ ( 𝑌 ∈ 𝑃 → 𝑌 ∈ ( Base ‘ 𝐾 ) )
16 14 15 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → 𝑌 ∈ ( Base ‘ 𝐾 ) )
17 11 2 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋 ∧ 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
18 9 13 16 17 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → ( 𝑋 ∧ 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
19 simp2r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → ( 𝑋 ∧ 𝑌 ) ≠ 0 )
20 simp3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 )
21 11 1 3 4 5 llnle ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∧ 𝑌 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( 𝑋 ∧ 𝑌 ) ≠ 0 ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ) → ∃ 𝑢 ∈ 𝑁 𝑢 ≤ ( 𝑋 ∧ 𝑌 ) )
22 8 18 19 20 21 syl22anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → ∃ 𝑢 ∈ 𝑁 𝑢 ≤ ( 𝑋 ∧ 𝑌 ) )
23 9 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝑁 ∧ 𝑢 ≤ ( 𝑋 ∧ 𝑌 ) ) ) → 𝐾 ∈ Lat )
24 18 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝑁 ∧ 𝑢 ≤ ( 𝑋 ∧ 𝑌 ) ) ) → ( 𝑋 ∧ 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
25 13 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝑁 ∧ 𝑢 ≤ ( 𝑋 ∧ 𝑌 ) ) ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
26 11 1 2 latmle1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋 ∧ 𝑌 ) ≤ 𝑋 )
27 9 13 16 26 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → ( 𝑋 ∧ 𝑌 ) ≤ 𝑋 )
28 27 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝑁 ∧ 𝑢 ≤ ( 𝑋 ∧ 𝑌 ) ) ) → ( 𝑋 ∧ 𝑌 ) ≤ 𝑋 )
29 11 5 llnbase ⊢ ( 𝑢 ∈ 𝑁 → 𝑢 ∈ ( Base ‘ 𝐾 ) )
30 29 ad2antrl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝑁 ∧ 𝑢 ≤ ( 𝑋 ∧ 𝑌 ) ) ) → 𝑢 ∈ ( Base ‘ 𝐾 ) )
31 simprr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝑁 ∧ 𝑢 ≤ ( 𝑋 ∧ 𝑌 ) ) ) → 𝑢 ≤ ( 𝑋 ∧ 𝑌 ) )
32 11 1 23 30 24 25 31 28 lattrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝑁 ∧ 𝑢 ≤ ( 𝑋 ∧ 𝑌 ) ) ) → 𝑢 ≤ 𝑋 )
33 simpl11 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝑁 ∧ 𝑢 ≤ ( 𝑋 ∧ 𝑌 ) ) ) → 𝐾 ∈ HL )
34 simprl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝑁 ∧ 𝑢 ≤ ( 𝑋 ∧ 𝑌 ) ) ) → 𝑢 ∈ 𝑁 )
35 simpl12 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝑁 ∧ 𝑢 ≤ ( 𝑋 ∧ 𝑌 ) ) ) → 𝑋 ∈ 𝑁 )
36 1 5 llncmp ⊢ ( ( 𝐾 ∈ HL ∧ 𝑢 ∈ 𝑁 ∧ 𝑋 ∈ 𝑁 ) → ( 𝑢 ≤ 𝑋 ↔ 𝑢 = 𝑋 ) )
37 33 34 35 36 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝑁 ∧ 𝑢 ≤ ( 𝑋 ∧ 𝑌 ) ) ) → ( 𝑢 ≤ 𝑋 ↔ 𝑢 = 𝑋 ) )
38 32 37 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝑁 ∧ 𝑢 ≤ ( 𝑋 ∧ 𝑌 ) ) ) → 𝑢 = 𝑋 )
39 38 31 eqbrtrrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝑁 ∧ 𝑢 ≤ ( 𝑋 ∧ 𝑌 ) ) ) → 𝑋 ≤ ( 𝑋 ∧ 𝑌 ) )
40 11 1 23 24 25 28 39 latasymd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) ∧ ( 𝑢 ∈ 𝑁 ∧ 𝑢 ≤ ( 𝑋 ∧ 𝑌 ) ) ) → ( 𝑋 ∧ 𝑌 ) = 𝑋 )
41 22 40 rexlimddv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → ( 𝑋 ∧ 𝑌 ) = 𝑋 )
42 11 1 2 latleeqm1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋 ≤ 𝑌 ↔ ( 𝑋 ∧ 𝑌 ) = 𝑋 ) )
43 9 13 16 42 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → ( 𝑋 ≤ 𝑌 ↔ ( 𝑋 ∧ 𝑌 ) = 𝑋 ) )
44 41 43 mpbird ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ∧ ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ) → 𝑋 ≤ 𝑌 )
45 44 3expia ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) → ( ¬ ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 → 𝑋 ≤ 𝑌 ) )
46 7 45 mt3d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ¬ 𝑋 ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 0 ) ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 )