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 ˙ = K
lplni2.j ˙ = join K
lplni2.a A = Atoms K
lplni2.p P = LPlanes K
Assertion lplni2 K HL Q A R A S A Q R ¬ S ˙ Q ˙ R Q ˙ R ˙ S P

Proof

Step Hyp Ref Expression
1 lplni2.l ˙ = K
2 lplni2.j ˙ = join K
3 lplni2.a A = Atoms K
4 lplni2.p P = LPlanes K
5 simp2 K HL Q A R A S A Q R ¬ S ˙ Q ˙ R Q A R A S A
6 simp3l K HL Q A R A S A Q R ¬ S ˙ Q ˙ R Q R
7 simp3r K HL Q A R A S A Q R ¬ S ˙ Q ˙ R ¬ S ˙ Q ˙ R
8 eqidd K HL Q A R A S A Q R ¬ S ˙ Q ˙ R Q ˙ R ˙ S = Q ˙ R ˙ S
9 neeq1 q = Q q r Q r
10 oveq1 q = Q q ˙ r = Q ˙ r
11 10 breq2d q = Q s ˙ q ˙ r s ˙ Q ˙ r
12 11 notbid q = Q ¬ s ˙ q ˙ r ¬ s ˙ Q ˙ r
13 10 oveq1d q = Q q ˙ r ˙ s = Q ˙ r ˙ s
14 13 eqeq2d q = Q Q ˙ R ˙ S = q ˙ r ˙ s Q ˙ R ˙ S = Q ˙ r ˙ s
15 9 12 14 3anbi123d q = Q q r ¬ s ˙ q ˙ r Q ˙ R ˙ S = q ˙ r ˙ s Q r ¬ s ˙ Q ˙ r Q ˙ R ˙ S = Q ˙ r ˙ s
16 neeq2 r = R Q r Q R
17 oveq2 r = R Q ˙ r = Q ˙ R
18 17 breq2d r = R s ˙ Q ˙ r s ˙ Q ˙ R
19 18 notbid r = R ¬ s ˙ Q ˙ r ¬ s ˙ Q ˙ R
20 17 oveq1d r = R Q ˙ r ˙ s = Q ˙ R ˙ s
21 20 eqeq2d r = R Q ˙ R ˙ S = Q ˙ r ˙ s Q ˙ R ˙ S = Q ˙ R ˙ s
22 16 19 21 3anbi123d r = R Q r ¬ s ˙ Q ˙ r Q ˙ R ˙ S = Q ˙ r ˙ s Q R ¬ s ˙ Q ˙ R Q ˙ R ˙ S = Q ˙ R ˙ s
23 breq1 s = S s ˙ Q ˙ R S ˙ Q ˙ R
24 23 notbid s = S ¬ s ˙ Q ˙ R ¬ S ˙ Q ˙ R
25 oveq2 s = S Q ˙ R ˙ s = Q ˙ R ˙ S
26 25 eqeq2d s = S Q ˙ R ˙ S = Q ˙ R ˙ s Q ˙ R ˙ S = Q ˙ R ˙ S
27 24 26 3anbi23d s = S Q R ¬ s ˙ Q ˙ R Q ˙ R ˙ S = Q ˙ R ˙ s Q R ¬ S ˙ Q ˙ R Q ˙ R ˙ S = Q ˙ R ˙ S
28 15 22 27 rspc3ev Q A R A S A Q R ¬ S ˙ Q ˙ R Q ˙ R ˙ S = Q ˙ R ˙ S q A r A s A q r ¬ s ˙ q ˙ r Q ˙ R ˙ S = q ˙ r ˙ s
29 5 6 7 8 28 syl13anc K HL Q A R A S A Q R ¬ S ˙ Q ˙ R q A r A s A q r ¬ s ˙ q ˙ r Q ˙ R ˙ S = q ˙ r ˙ s
30 simp1 K HL Q A R A S A Q R ¬ S ˙ Q ˙ R K HL
31 hllat K HL K Lat
32 31 3ad2ant1 K HL Q A R A S A Q R ¬ S ˙ Q ˙ R K Lat
33 simp21 K HL Q A R A S A Q R ¬ S ˙ Q ˙ R Q A
34 simp22 K HL Q A R A S A Q R ¬ S ˙ Q ˙ R R A
35 eqid Base K = Base K
36 35 2 3 hlatjcl K HL Q A R A Q ˙ R Base K
37 30 33 34 36 syl3anc K HL Q A R A S A Q R ¬ S ˙ Q ˙ R Q ˙ R Base K
38 simp23 K HL Q A R A S A Q R ¬ S ˙ Q ˙ R S A
39 35 3 atbase S A S Base K
40 38 39 syl K HL Q A R A S A Q R ¬ S ˙ Q ˙ R S Base K
41 35 2 latjcl K Lat Q ˙ R Base K S Base K Q ˙ R ˙ S Base K
42 32 37 40 41 syl3anc K HL Q A R A S A Q R ¬ S ˙ Q ˙ R Q ˙ R ˙ S Base K
43 35 1 2 3 4 islpln5 K HL Q ˙ R ˙ S Base K Q ˙ R ˙ S P q A r A s A q r ¬ s ˙ q ˙ r Q ˙ R ˙ S = q ˙ r ˙ s
44 30 42 43 syl2anc K HL Q A R A S A Q R ¬ S ˙ Q ˙ R Q ˙ R ˙ S P q A r A s A q r ¬ s ˙ q ˙ r Q ˙ R ˙ S = q ˙ r ˙ s
45 29 44 mpbird K HL Q A R A S A Q R ¬ S ˙ Q ˙ R Q ˙ R ˙ S P