Metamath Proof Explorer


Theorem 3dimlem4a

Description: Lemma for 3dim3 . (Contributed by NM, 27-Jul-2012)

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

Proof

Step Hyp Ref Expression
1 3dim0.j ˙ = join K
2 3dim0.l ˙ = K
3 3dim0.a A = Atoms K
4 simp33 K HL P A Q A R A S A ¬ S ˙ Q ˙ R ¬ P ˙ Q ˙ R ¬ P ˙ Q ˙ R ˙ S ¬ P ˙ Q ˙ R ˙ S
5 simp11 K HL P A Q A R A S A ¬ S ˙ Q ˙ R ¬ P ˙ Q ˙ R ¬ P ˙ Q ˙ R ˙ S K HL
6 5 hllatd K HL P A Q A R A S A ¬ S ˙ Q ˙ R ¬ P ˙ Q ˙ R ¬ P ˙ Q ˙ R ˙ S K Lat
7 simp13 K HL P A Q A R A S A ¬ S ˙ Q ˙ R ¬ P ˙ Q ˙ R ¬ P ˙ Q ˙ R ˙ S Q A
8 eqid Base K = Base K
9 8 3 atbase Q A Q Base K
10 7 9 syl K HL P A Q A R A S A ¬ S ˙ Q ˙ R ¬ P ˙ Q ˙ R ¬ P ˙ Q ˙ R ˙ S Q Base K
11 simp2l K HL P A Q A R A S A ¬ S ˙ Q ˙ R ¬ P ˙ Q ˙ R ¬ P ˙ Q ˙ R ˙ S R A
12 8 3 atbase R A R Base K
13 11 12 syl K HL P A Q A R A S A ¬ S ˙ Q ˙ R ¬ P ˙ Q ˙ R ¬ P ˙ Q ˙ R ˙ S R Base K
14 simp12 K HL P A Q A R A S A ¬ S ˙ Q ˙ R ¬ P ˙ Q ˙ R ¬ P ˙ Q ˙ R ˙ S P A
15 8 3 atbase P A P Base K
16 14 15 syl K HL P A Q A R A S A ¬ S ˙ Q ˙ R ¬ P ˙ Q ˙ R ¬ P ˙ Q ˙ R ˙ S P Base K
17 8 1 latjrot K Lat Q Base K R Base K P Base K Q ˙ R ˙ P = P ˙ Q ˙ R
18 6 10 13 16 17 syl13anc K HL P A Q A R A S A ¬ S ˙ Q ˙ R ¬ P ˙ Q ˙ R ¬ P ˙ Q ˙ R ˙ S Q ˙ R ˙ P = P ˙ Q ˙ R
19 18 breq2d K HL P A Q A R A S A ¬ S ˙ Q ˙ R ¬ P ˙ Q ˙ R ¬ P ˙ Q ˙ R ˙ S S ˙ Q ˙ R ˙ P S ˙ P ˙ Q ˙ R
20 simp2r K HL P A Q A R A S A ¬ S ˙ Q ˙ R ¬ P ˙ Q ˙ R ¬ P ˙ Q ˙ R ˙ S S A
21 8 1 latjcl K Lat Q Base K R Base K Q ˙ R Base K
22 6 10 13 21 syl3anc K HL P A Q A R A S A ¬ S ˙ Q ˙ R ¬ P ˙ Q ˙ R ¬ P ˙ Q ˙ R ˙ S Q ˙ R Base K
23 simp31 K HL P A Q A R A S A ¬ S ˙ Q ˙ R ¬ P ˙ Q ˙ R ¬ P ˙ Q ˙ R ˙ S ¬ S ˙ Q ˙ R
24 8 2 1 3 hlexch1 K HL S A P A Q ˙ R Base K ¬ S ˙ Q ˙ R S ˙ Q ˙ R ˙ P P ˙ Q ˙ R ˙ S
25 5 20 14 22 23 24 syl131anc K HL P A Q A R A S A ¬ S ˙ Q ˙ R ¬ P ˙ Q ˙ R ¬ P ˙ Q ˙ R ˙ S S ˙ Q ˙ R ˙ P P ˙ Q ˙ R ˙ S
26 19 25 sylbird K HL P A Q A R A S A ¬ S ˙ Q ˙ R ¬ P ˙ Q ˙ R ¬ P ˙ Q ˙ R ˙ S S ˙ P ˙ Q ˙ R P ˙ Q ˙ R ˙ S
27 4 26 mtod K HL P A Q A R A S A ¬ S ˙ Q ˙ R ¬ P ˙ Q ˙ R ¬ P ˙ Q ˙ R ˙ S ¬ S ˙ P ˙ Q ˙ R