Metamath Proof Explorer


Theorem 4atexlemex6

Description: Lemma for 4atexlem7 . (Contributed by NM, 25-Nov-2012)

Ref Expression
Hypotheses 4thatleme.l ˙ = K
4thatleme.j ˙ = join K
4thatleme.m ˙ = meet K
4thatleme.a A = Atoms K
4thatleme.h H = LHyp K
Assertion 4atexlemex6 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A P ˙ R = Q ˙ R P Q ¬ S ˙ P ˙ Q z A ¬ z ˙ W P ˙ z = S ˙ z

Proof

Step Hyp Ref Expression
1 4thatleme.l ˙ = K
2 4thatleme.j ˙ = join K
3 4thatleme.m ˙ = meet K
4 4thatleme.a A = Atoms K
5 4thatleme.h H = LHyp K
6 simp11l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A P ˙ R = Q ˙ R P Q ¬ S ˙ P ˙ Q K HL
7 simp11 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A P ˙ R = Q ˙ R P Q ¬ S ˙ P ˙ Q K HL W H
8 simp12 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A P ˙ R = Q ˙ R P Q ¬ S ˙ P ˙ Q P A ¬ P ˙ W
9 simp13l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A P ˙ R = Q ˙ R P Q ¬ S ˙ P ˙ Q Q A
10 simp32 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A P ˙ R = Q ˙ R P Q ¬ S ˙ P ˙ Q P Q
11 1 2 3 4 5 lhpat K HL W H P A ¬ P ˙ W Q A P Q P ˙ Q ˙ W A
12 7 8 9 10 11 syl112anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A P ˙ R = Q ˙ R P Q ¬ S ˙ P ˙ Q P ˙ Q ˙ W A
13 simp2r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A P ˙ R = Q ˙ R P Q ¬ S ˙ P ˙ Q S A
14 simp12l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A P ˙ R = Q ˙ R P Q ¬ S ˙ P ˙ Q P A
15 simp33 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A P ˙ R = Q ˙ R P Q ¬ S ˙ P ˙ Q ¬ S ˙ P ˙ Q
16 1 2 4 atnlej1 K HL S A P A Q A ¬ S ˙ P ˙ Q S P
17 6 13 14 9 15 16 syl131anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A P ˙ R = Q ˙ R P Q ¬ S ˙ P ˙ Q S P
18 17 necomd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A P ˙ R = Q ˙ R P Q ¬ S ˙ P ˙ Q P S
19 1 2 3 4 5 lhpat K HL W H P A ¬ P ˙ W S A P S P ˙ S ˙ W A
20 7 8 13 18 19 syl112anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A P ˙ R = Q ˙ R P Q ¬ S ˙ P ˙ Q P ˙ S ˙ W A
21 2 4 hlsupr2 K HL P ˙ Q ˙ W A P ˙ S ˙ W A t A P ˙ Q ˙ W ˙ t = P ˙ S ˙ W ˙ t
22 6 12 20 21 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A P ˙ R = Q ˙ R P Q ¬ S ˙ P ˙ Q t A P ˙ Q ˙ W ˙ t = P ˙ S ˙ W ˙ t
23 simp111 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A P ˙ R = Q ˙ R P Q ¬ S ˙ P ˙ Q t A P ˙ Q ˙ W ˙ t = P ˙ S ˙ W ˙ t K HL W H
24 simp112 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A P ˙ R = Q ˙ R P Q ¬ S ˙ P ˙ Q t A P ˙ Q ˙ W ˙ t = P ˙ S ˙ W ˙ t P A ¬ P ˙ W
25 simp113 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A P ˙ R = Q ˙ R P Q ¬ S ˙ P ˙ Q t A P ˙ Q ˙ W ˙ t = P ˙ S ˙ W ˙ t Q A ¬ Q ˙ W
26 simp12r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A P ˙ R = Q ˙ R P Q ¬ S ˙ P ˙ Q t A P ˙ Q ˙ W ˙ t = P ˙ S ˙ W ˙ t S A
27 simp2ll K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A P ˙ R = Q ˙ R P Q ¬ S ˙ P ˙ Q R A
28 27 3ad2ant1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A P ˙ R = Q ˙ R P Q ¬ S ˙ P ˙ Q t A P ˙ Q ˙ W ˙ t = P ˙ S ˙ W ˙ t R A
29 simp2lr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A P ˙ R = Q ˙ R P Q ¬ S ˙ P ˙ Q ¬ R ˙ W
30 29 3ad2ant1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A P ˙ R = Q ˙ R P Q ¬ S ˙ P ˙ Q t A P ˙ Q ˙ W ˙ t = P ˙ S ˙ W ˙ t ¬ R ˙ W
31 simp131 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A P ˙ R = Q ˙ R P Q ¬ S ˙ P ˙ Q t A P ˙ Q ˙ W ˙ t = P ˙ S ˙ W ˙ t P ˙ R = Q ˙ R
32 28 30 31 3jca K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A P ˙ R = Q ˙ R P Q ¬ S ˙ P ˙ Q t A P ˙ Q ˙ W ˙ t = P ˙ S ˙ W ˙ t R A ¬ R ˙ W P ˙ R = Q ˙ R
33 3simpc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A P ˙ R = Q ˙ R P Q ¬ S ˙ P ˙ Q t A P ˙ Q ˙ W ˙ t = P ˙ S ˙ W ˙ t t A P ˙ Q ˙ W ˙ t = P ˙ S ˙ W ˙ t
34 simp132 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A P ˙ R = Q ˙ R P Q ¬ S ˙ P ˙ Q t A P ˙ Q ˙ W ˙ t = P ˙ S ˙ W ˙ t P Q
35 simp133 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A P ˙ R = Q ˙ R P Q ¬ S ˙ P ˙ Q t A P ˙ Q ˙ W ˙ t = P ˙ S ˙ W ˙ t ¬ S ˙ P ˙ Q
36 biid K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A R A ¬ R ˙ W P ˙ R = Q ˙ R t A P ˙ Q ˙ W ˙ t = P ˙ S ˙ W ˙ t P Q ¬ S ˙ P ˙ Q K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A R A ¬ R ˙ W P ˙ R = Q ˙ R t A P ˙ Q ˙ W ˙ t = P ˙ S ˙ W ˙ t P Q ¬ S ˙ P ˙ Q
37 eqid P ˙ Q ˙ W = P ˙ Q ˙ W
38 eqid P ˙ S ˙ W = P ˙ S ˙ W
39 eqid Q ˙ t ˙ P ˙ S = Q ˙ t ˙ P ˙ S
40 eqid R ˙ t ˙ P ˙ S = R ˙ t ˙ P ˙ S
41 36 1 2 3 4 5 37 38 39 40 4atexlemex4 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A R A ¬ R ˙ W P ˙ R = Q ˙ R t A P ˙ Q ˙ W ˙ t = P ˙ S ˙ W ˙ t P Q ¬ S ˙ P ˙ Q Q ˙ t ˙ P ˙ S = S z A ¬ z ˙ W P ˙ z = S ˙ z
42 36 1 2 3 4 5 37 38 39 4atexlemex2 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A R A ¬ R ˙ W P ˙ R = Q ˙ R t A P ˙ Q ˙ W ˙ t = P ˙ S ˙ W ˙ t P Q ¬ S ˙ P ˙ Q Q ˙ t ˙ P ˙ S S z A ¬ z ˙ W P ˙ z = S ˙ z
43 41 42 pm2.61dane K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A R A ¬ R ˙ W P ˙ R = Q ˙ R t A P ˙ Q ˙ W ˙ t = P ˙ S ˙ W ˙ t P Q ¬ S ˙ P ˙ Q z A ¬ z ˙ W P ˙ z = S ˙ z
44 23 24 25 26 32 33 34 35 43 syl332anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A P ˙ R = Q ˙ R P Q ¬ S ˙ P ˙ Q t A P ˙ Q ˙ W ˙ t = P ˙ S ˙ W ˙ t z A ¬ z ˙ W P ˙ z = S ˙ z
45 44 rexlimdv3a K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A P ˙ R = Q ˙ R P Q ¬ S ˙ P ˙ Q t A P ˙ Q ˙ W ˙ t = P ˙ S ˙ W ˙ t z A ¬ z ˙ W P ˙ z = S ˙ z
46 22 45 mpd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A P ˙ R = Q ˙ R P Q ¬ S ˙ P ˙ Q z A ¬ z ˙ W P ˙ z = S ˙ z