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

Metamath Proof Explorer

Theorem islpln2a

Description: The predicate "is a lattice plane" for join of atoms. (Contributed by NM, 16-Jul-2012)

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

Proof

Step Hyp Ref Expression
1 islpln2a.l ⊢ ≤ = ( le ‘ 𝐾 )
2 islpln2a.j ⊢ ∨ = ( join ‘ 𝐾 )
3 islpln2a.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 islpln2a.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
5 oveq1 ⊢ ( 𝑄 = 𝑅 → ( 𝑄 ∨ 𝑅 ) = ( 𝑅 ∨ 𝑅 ) )
6 2 3 hlatjidm ⊢ ( ( 𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ) → ( 𝑅 ∨ 𝑅 ) = 𝑅 )
7 6 3ad2antr2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( 𝑅 ∨ 𝑅 ) = 𝑅 )
8 5 7 sylan9eqr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑄 = 𝑅 ) → ( 𝑄 ∨ 𝑅 ) = 𝑅 )
9 8 oveq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑄 = 𝑅 ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) = ( 𝑅 ∨ 𝑆 ) )
10 simpll ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑄 = 𝑅 ) → 𝐾 ∈ HL )
11 simplr2 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑄 = 𝑅 ) → 𝑅 ∈ 𝐴 )
12 simplr3 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑄 = 𝑅 ) → 𝑆 ∈ 𝐴 )
13 2 3 4 2atnelpln ⊢ ( ( 𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → ¬ ( 𝑅 ∨ 𝑆 ) ∈ 𝑃 )
14 10 11 12 13 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑄 = 𝑅 ) → ¬ ( 𝑅 ∨ 𝑆 ) ∈ 𝑃 )
15 9 14 eqneltrd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑄 = 𝑅 ) → ¬ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑃 )
16 15 ex ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( 𝑄 = 𝑅 → ¬ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑃 ) )
17 16 necon2ad ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑃 → 𝑄 ≠ 𝑅 ) )
18 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
19 18 adantr ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝐾 ∈ Lat )
20 simpr3 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝑆 ∈ 𝐴 )
21 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
22 21 3 atbase ⊢ ( 𝑆 ∈ 𝐴 → 𝑆 ∈ ( Base ‘ 𝐾 ) )
23 20 22 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝑆 ∈ ( Base ‘ 𝐾 ) )
24 21 2 3 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
25 24 3adant3r3 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
26 21 1 2 latleeqj2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ↔ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) = ( 𝑄 ∨ 𝑅 ) ) )
27 19 23 25 26 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ↔ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) = ( 𝑄 ∨ 𝑅 ) ) )
28 2 3 4 2atnelpln ⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ¬ ( 𝑄 ∨ 𝑅 ) ∈ 𝑃 )
29 28 3adant3r3 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ¬ ( 𝑄 ∨ 𝑅 ) ∈ 𝑃 )
30 eleq1 ⊢ ( ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) = ( 𝑄 ∨ 𝑅 ) → ( ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑃 ↔ ( 𝑄 ∨ 𝑅 ) ∈ 𝑃 ) )
31 30 notbid ⊢ ( ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) = ( 𝑄 ∨ 𝑅 ) → ( ¬ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑃 ↔ ¬ ( 𝑄 ∨ 𝑅 ) ∈ 𝑃 ) )
32 29 31 syl5ibrcom ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) = ( 𝑄 ∨ 𝑅 ) → ¬ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑃 ) )
33 27 32 sylbid ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) → ¬ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑃 ) )
34 33 con2d ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑃 → ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) )
35 17 34 jcad ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑃 → ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) )
36 1 2 3 4 lplni2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑃 )
37 36 3expia ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑃 ) )
38 35 37 impbid ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ∈ 𝑃 ↔ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) )