Metamath Proof Explorer


Theorem 3atlem4

Description: Lemma for 3at . (Contributed by NM, 23-Jun-2012)

Ref Expression
Hypotheses 3at.l ˙ = K
3at.j ˙ = join K
3at.a A = Atoms K
Assertion 3atlem4 K HL P A Q A R A S A T A ¬ R ˙ P ˙ Q P Q P ˙ Q ˙ R ˙ S ˙ T ˙ R P ˙ Q ˙ R = S ˙ T ˙ R

Proof

Step Hyp Ref Expression
1 3at.l ˙ = K
2 3at.j ˙ = join K
3 3at.a A = Atoms K
4 simp11 K HL P A Q A R A S A T A ¬ R ˙ P ˙ Q P Q P ˙ Q ˙ R ˙ S ˙ T ˙ R K HL
5 simp12 K HL P A Q A R A S A T A ¬ R ˙ P ˙ Q P Q P ˙ Q ˙ R ˙ S ˙ T ˙ R P A Q A R A
6 simp13l K HL P A Q A R A S A T A ¬ R ˙ P ˙ Q P Q P ˙ Q ˙ R ˙ S ˙ T ˙ R S A
7 simp13r K HL P A Q A R A S A T A ¬ R ˙ P ˙ Q P Q P ˙ Q ˙ R ˙ S ˙ T ˙ R T A
8 simp123 K HL P A Q A R A S A T A ¬ R ˙ P ˙ Q P Q P ˙ Q ˙ R ˙ S ˙ T ˙ R R A
9 6 7 8 3jca K HL P A Q A R A S A T A ¬ R ˙ P ˙ Q P Q P ˙ Q ˙ R ˙ S ˙ T ˙ R S A T A R A
10 simp2l K HL P A Q A R A S A T A ¬ R ˙ P ˙ Q P Q P ˙ Q ˙ R ˙ S ˙ T ˙ R ¬ R ˙ P ˙ Q
11 4 hllatd K HL P A Q A R A S A T A ¬ R ˙ P ˙ Q P Q P ˙ Q ˙ R ˙ S ˙ T ˙ R K Lat
12 eqid Base K = Base K
13 12 3 atbase R A R Base K
14 8 13 syl K HL P A Q A R A S A T A ¬ R ˙ P ˙ Q P Q P ˙ Q ˙ R ˙ S ˙ T ˙ R R Base K
15 simp121 K HL P A Q A R A S A T A ¬ R ˙ P ˙ Q P Q P ˙ Q ˙ R ˙ S ˙ T ˙ R P A
16 12 3 atbase P A P Base K
17 15 16 syl K HL P A Q A R A S A T A ¬ R ˙ P ˙ Q P Q P ˙ Q ˙ R ˙ S ˙ T ˙ R P Base K
18 simp122 K HL P A Q A R A S A T A ¬ R ˙ P ˙ Q P Q P ˙ Q ˙ R ˙ S ˙ T ˙ R Q A
19 12 3 atbase Q A Q Base K
20 18 19 syl K HL P A Q A R A S A T A ¬ R ˙ P ˙ Q P Q P ˙ Q ˙ R ˙ S ˙ T ˙ R Q Base K
21 12 1 2 latnlej1l K Lat R Base K P Base K Q Base K ¬ R ˙ P ˙ Q R P
22 11 14 17 20 10 21 syl131anc K HL P A Q A R A S A T A ¬ R ˙ P ˙ Q P Q P ˙ Q ˙ R ˙ S ˙ T ˙ R R P
23 22 necomd K HL P A Q A R A S A T A ¬ R ˙ P ˙ Q P Q P ˙ Q ˙ R ˙ S ˙ T ˙ R P R
24 simp2r K HL P A Q A R A S A T A ¬ R ˙ P ˙ Q P Q P ˙ Q ˙ R ˙ S ˙ T ˙ R P Q
25 24 necomd K HL P A Q A R A S A T A ¬ R ˙ P ˙ Q P Q P ˙ Q ˙ R ˙ S ˙ T ˙ R Q P
26 1 2 3 hlatexch1 K HL Q A R A P A Q P Q ˙ P ˙ R R ˙ P ˙ Q
27 4 18 8 15 25 26 syl131anc K HL P A Q A R A S A T A ¬ R ˙ P ˙ Q P Q P ˙ Q ˙ R ˙ S ˙ T ˙ R Q ˙ P ˙ R R ˙ P ˙ Q
28 10 27 mtod K HL P A Q A R A S A T A ¬ R ˙ P ˙ Q P Q P ˙ Q ˙ R ˙ S ˙ T ˙ R ¬ Q ˙ P ˙ R
29 simp3 K HL P A Q A R A S A T A ¬ R ˙ P ˙ Q P Q P ˙ Q ˙ R ˙ S ˙ T ˙ R P ˙ Q ˙ R ˙ S ˙ T ˙ R
30 1 2 3 3atlem3 K HL P A Q A R A S A T A R A ¬ R ˙ P ˙ Q P R ¬ Q ˙ P ˙ R P ˙ Q ˙ R ˙ S ˙ T ˙ R P ˙ Q ˙ R = S ˙ T ˙ R
31 4 5 9 10 23 28 29 30 syl331anc K HL P A Q A R A S A T A ¬ R ˙ P ˙ Q P Q P ˙ Q ˙ R ˙ S ˙ T ˙ R P ˙ Q ˙ R = S ˙ T ˙ R