Metamath Proof Explorer


Theorem 3dimlem2

Description: Lemma for 3dim1 . (Contributed by NM, 25-Jul-2012)

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

Proof

Step Hyp Ref Expression
1 3dim0.j ˙ = join K
2 3dim0.l ˙ = K
3 3dim0.a A = Atoms K
4 simp3l K HL P A Q A R A ¬ S ˙ Q ˙ R ¬ T ˙ Q ˙ R ˙ S P Q P ˙ Q ˙ R P Q
5 simp22 K HL P A Q A R A ¬ S ˙ Q ˙ R ¬ T ˙ Q ˙ R ˙ S P Q P ˙ Q ˙ R ¬ S ˙ Q ˙ R
6 1 3 hlatjcom K HL P A Q A P ˙ Q = Q ˙ P
7 6 3ad2ant1 K HL P A Q A R A ¬ S ˙ Q ˙ R ¬ T ˙ Q ˙ R ˙ S P Q P ˙ Q ˙ R P ˙ Q = Q ˙ P
8 simp3r K HL P A Q A R A ¬ S ˙ Q ˙ R ¬ T ˙ Q ˙ R ˙ S P Q P ˙ Q ˙ R P ˙ Q ˙ R
9 simp11 K HL P A Q A R A ¬ S ˙ Q ˙ R ¬ T ˙ Q ˙ R ˙ S P Q P ˙ Q ˙ R K HL
10 simp12 K HL P A Q A R A ¬ S ˙ Q ˙ R ¬ T ˙ Q ˙ R ˙ S P Q P ˙ Q ˙ R P A
11 simp21 K HL P A Q A R A ¬ S ˙ Q ˙ R ¬ T ˙ Q ˙ R ˙ S P Q P ˙ Q ˙ R R A
12 simp13 K HL P A Q A R A ¬ S ˙ Q ˙ R ¬ T ˙ Q ˙ R ˙ S P Q P ˙ Q ˙ R Q A
13 2 1 3 hlatexchb1 K HL P A R A Q A P Q P ˙ Q ˙ R Q ˙ P = Q ˙ R
14 9 10 11 12 4 13 syl131anc K HL P A Q A R A ¬ S ˙ Q ˙ R ¬ T ˙ Q ˙ R ˙ S P Q P ˙ Q ˙ R P ˙ Q ˙ R Q ˙ P = Q ˙ R
15 8 14 mpbid K HL P A Q A R A ¬ S ˙ Q ˙ R ¬ T ˙ Q ˙ R ˙ S P Q P ˙ Q ˙ R Q ˙ P = Q ˙ R
16 7 15 eqtrd K HL P A Q A R A ¬ S ˙ Q ˙ R ¬ T ˙ Q ˙ R ˙ S P Q P ˙ Q ˙ R P ˙ Q = Q ˙ R
17 16 breq2d K HL P A Q A R A ¬ S ˙ Q ˙ R ¬ T ˙ Q ˙ R ˙ S P Q P ˙ Q ˙ R S ˙ P ˙ Q S ˙ Q ˙ R
18 5 17 mtbird K HL P A Q A R A ¬ S ˙ Q ˙ R ¬ T ˙ Q ˙ R ˙ S P Q P ˙ Q ˙ R ¬ S ˙ P ˙ Q
19 simp23 K HL P A Q A R A ¬ S ˙ Q ˙ R ¬ T ˙ Q ˙ R ˙ S P Q P ˙ Q ˙ R ¬ T ˙ Q ˙ R ˙ S
20 16 oveq1d K HL P A Q A R A ¬ S ˙ Q ˙ R ¬ T ˙ Q ˙ R ˙ S P Q P ˙ Q ˙ R P ˙ Q ˙ S = Q ˙ R ˙ S
21 20 breq2d K HL P A Q A R A ¬ S ˙ Q ˙ R ¬ T ˙ Q ˙ R ˙ S P Q P ˙ Q ˙ R T ˙ P ˙ Q ˙ S T ˙ Q ˙ R ˙ S
22 19 21 mtbird K HL P A Q A R A ¬ S ˙ Q ˙ R ¬ T ˙ Q ˙ R ˙ S P Q P ˙ Q ˙ R ¬ T ˙ P ˙ Q ˙ S
23 4 18 22 3jca K HL P A Q A R A ¬ S ˙ Q ˙ R ¬ T ˙ Q ˙ R ˙ S P Q P ˙ Q ˙ R P Q ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q ˙ S