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

Metamath Proof Explorer

Theorem lplni2

Description: The join of 3 different atoms is a lattice plane. (Contributed by NM, 4-Jul-2012)

Ref Expression
Hypotheses lplni2.l ⊢ ≤ = ( le ‘ 𝐾 )
lplni2.j ⊢ ∨ = ( join ‘ 𝐾 )
lplni2.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
lplni2.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
Assertion lplni2 ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑃 )

Proof

Step Hyp Ref Expression
1 lplni2.l ⊢ ≤ = ( le ‘ 𝐾 )
2 lplni2.j ⊢ ∨ = ( join ‘ 𝐾 )
3 lplni2.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 lplni2.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
5 simp2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) )
6 simp3l ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑄 ≠ 𝑅 )
7 simp3r ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) )
8 eqidd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) = ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) )
9 neeq1 ⊢ ( 𝑞 = 𝑄 → ( 𝑞 ≠ 𝑟 ↔ 𝑄 ≠ 𝑟 ) )
10 oveq1 ⊢ ( 𝑞 = 𝑄 → ( 𝑞 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) )
11 10 breq2d ⊢ ( 𝑞 = 𝑄 → ( 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ↔ 𝑠 ≤ ( 𝑄 ∨ 𝑟 ) ) )
12 11 notbid ⊢ ( 𝑞 = 𝑄 → ( ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ↔ ¬ 𝑠 ≤ ( 𝑄 ∨ 𝑟 ) ) )
13 10 oveq1d ⊢ ( 𝑞 = 𝑄 → ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) = ( ( 𝑄 ∨ 𝑟 ) ∨ 𝑠 ) )
14 13 eqeq2d ⊢ ( 𝑞 = 𝑄 → ( ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ↔ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) = ( ( 𝑄 ∨ 𝑟 ) ∨ 𝑠 ) ) )
15 9 12 14 3anbi123d ⊢ ( 𝑞 = 𝑄 → ( ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ↔ ( 𝑄 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑄 ∨ 𝑟 ) ∧ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) = ( ( 𝑄 ∨ 𝑟 ) ∨ 𝑠 ) ) ) )
16 neeq2 ⊢ ( 𝑟 = 𝑅 → ( 𝑄 ≠ 𝑟 ↔ 𝑄 ≠ 𝑅 ) )
17 oveq2 ⊢ ( 𝑟 = 𝑅 → ( 𝑄 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑅 ) )
18 17 breq2d ⊢ ( 𝑟 = 𝑅 → ( 𝑠 ≤ ( 𝑄 ∨ 𝑟 ) ↔ 𝑠 ≤ ( 𝑄 ∨ 𝑅 ) ) )
19 18 notbid ⊢ ( 𝑟 = 𝑅 → ( ¬ 𝑠 ≤ ( 𝑄 ∨ 𝑟 ) ↔ ¬ 𝑠 ≤ ( 𝑄 ∨ 𝑅 ) ) )
20 17 oveq1d ⊢ ( 𝑟 = 𝑅 → ( ( 𝑄 ∨ 𝑟 ) ∨ 𝑠 ) = ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑠 ) )
21 20 eqeq2d ⊢ ( 𝑟 = 𝑅 → ( ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) = ( ( 𝑄 ∨ 𝑟 ) ∨ 𝑠 ) ↔ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) = ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑠 ) ) )
22 16 19 21 3anbi123d ⊢ ( 𝑟 = 𝑅 → ( ( 𝑄 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑄 ∨ 𝑟 ) ∧ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) = ( ( 𝑄 ∨ 𝑟 ) ∨ 𝑠 ) ) ↔ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑠 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) = ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑠 ) ) ) )
23 breq1 ⊢ ( 𝑠 = 𝑆 → ( 𝑠 ≤ ( 𝑄 ∨ 𝑅 ) ↔ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) )
24 23 notbid ⊢ ( 𝑠 = 𝑆 → ( ¬ 𝑠 ≤ ( 𝑄 ∨ 𝑅 ) ↔ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) )
25 oveq2 ⊢ ( 𝑠 = 𝑆 → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑠 ) = ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) )
26 25 eqeq2d ⊢ ( 𝑠 = 𝑆 → ( ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) = ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑠 ) ↔ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) = ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) )
27 24 26 3anbi23d ⊢ ( 𝑠 = 𝑆 → ( ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑠 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) = ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑠 ) ) ↔ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) = ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) )
28 15 22 27 rspc3ev ⊢ ( ( ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) = ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) )
29 5 6 7 8 28 syl13anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) )
30 simp1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝐾 ∈ HL )
31 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
32 31 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝐾 ∈ Lat )
33 simp21 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑄 ∈ 𝐴 )
34 simp22 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑅 ∈ 𝐴 )
35 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
36 35 2 3 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
37 30 33 34 36 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
38 simp23 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑆 ∈ 𝐴 )
39 35 3 atbase ⊢ ( 𝑆 ∈ 𝐴 → 𝑆 ∈ ( Base ‘ 𝐾 ) )
40 38 39 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑆 ∈ ( Base ‘ 𝐾 ) )
41 35 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
42 32 37 40 41 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
43 35 1 2 3 4 islpln5 ⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑃 ↔ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) )
44 30 42 43 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑃 ↔ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ∨ 𝑟 ) ∧ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) = ( ( 𝑞 ∨ 𝑟 ) ∨ 𝑠 ) ) ) )
45 29 44 mpbird ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑃 )