Metamath Proof Explorer


Theorem dalawlem15

Description: Lemma for dalaw . Swap variable triples P Q R and S T U in dalawlem14 , to obtain the elimination of the remaining conditions in dalawlem1 . (Contributed by NM, 6-Oct-2012)

Ref Expression
Hypotheses dalawlem.l ˙ = K
dalawlem.j ˙ = join K
dalawlem.m ˙ = meet K
dalawlem.a A = Atoms K
dalawlem2.o O = LPlanes K
Assertion dalawlem15 K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S

Proof

Step Hyp Ref Expression
1 dalawlem.l ˙ = K
2 dalawlem.j ˙ = join K
3 dalawlem.m ˙ = meet K
4 dalawlem.a A = Atoms K
5 dalawlem2.o O = LPlanes K
6 simp11 K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A K HL
7 simp12 K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S
8 simp21 K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P A
9 simp31 K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A S A
10 2 4 hlatjcom K HL P A S A P ˙ S = S ˙ P
11 6 8 9 10 syl3anc K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ S = S ˙ P
12 simp22 K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q A
13 simp32 K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A T A
14 2 4 hlatjcom K HL Q A T A Q ˙ T = T ˙ Q
15 6 12 13 14 syl3anc K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ T = T ˙ Q
16 11 15 oveq12d K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ S ˙ Q ˙ T = S ˙ P ˙ T ˙ Q
17 16 breq1d K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ S ˙ Q ˙ T ˙ S ˙ T S ˙ P ˙ T ˙ Q ˙ S ˙ T
18 17 notbid K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ S ˙ P ˙ T ˙ Q ˙ S ˙ T
19 16 breq1d K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ S ˙ Q ˙ T ˙ T ˙ U S ˙ P ˙ T ˙ Q ˙ T ˙ U
20 19 notbid K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ S ˙ P ˙ T ˙ Q ˙ T ˙ U
21 16 breq1d K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ S ˙ Q ˙ T ˙ U ˙ S S ˙ P ˙ T ˙ Q ˙ U ˙ S
22 21 notbid K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S ¬ S ˙ P ˙ T ˙ Q ˙ U ˙ S
23 18 20 22 3anbi123d K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S ¬ S ˙ P ˙ T ˙ Q ˙ S ˙ T ¬ S ˙ P ˙ T ˙ Q ˙ T ˙ U ¬ S ˙ P ˙ T ˙ Q ˙ U ˙ S
24 23 anbi2d K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S S ˙ T ˙ U O ¬ S ˙ P ˙ T ˙ Q ˙ S ˙ T ¬ S ˙ P ˙ T ˙ Q ˙ T ˙ U ¬ S ˙ P ˙ T ˙ Q ˙ U ˙ S
25 7 24 mtbid K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A ¬ S ˙ T ˙ U O ¬ S ˙ P ˙ T ˙ Q ˙ S ˙ T ¬ S ˙ P ˙ T ˙ Q ˙ T ˙ U ¬ S ˙ P ˙ T ˙ Q ˙ U ˙ S
26 simp13 K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ S ˙ Q ˙ T ˙ R ˙ U
27 2 4 hlatjcom K HL S A P A S ˙ P = P ˙ S
28 6 9 8 27 syl3anc K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A S ˙ P = P ˙ S
29 2 4 hlatjcom K HL T A Q A T ˙ Q = Q ˙ T
30 6 13 12 29 syl3anc K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A T ˙ Q = Q ˙ T
31 28 30 oveq12d K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A S ˙ P ˙ T ˙ Q = P ˙ S ˙ Q ˙ T
32 simp33 K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A U A
33 simp23 K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A R A
34 2 4 hlatjcom K HL U A R A U ˙ R = R ˙ U
35 6 32 33 34 syl3anc K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A U ˙ R = R ˙ U
36 26 31 35 3brtr4d K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A S ˙ P ˙ T ˙ Q ˙ U ˙ R
37 simp3 K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A S A T A U A
38 simp2 K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P A Q A R A
39 1 2 3 4 5 dalawlem14 K HL ¬ S ˙ T ˙ U O ¬ S ˙ P ˙ T ˙ Q ˙ S ˙ T ¬ S ˙ P ˙ T ˙ Q ˙ T ˙ U ¬ S ˙ P ˙ T ˙ Q ˙ U ˙ S S ˙ P ˙ T ˙ Q ˙ U ˙ R S A T A U A P A Q A R A S ˙ T ˙ P ˙ Q ˙ T ˙ U ˙ Q ˙ R ˙ U ˙ S ˙ R ˙ P
40 6 25 36 37 38 39 syl311anc K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A S ˙ T ˙ P ˙ Q ˙ T ˙ U ˙ Q ˙ R ˙ U ˙ S ˙ R ˙ P
41 6 hllatd K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A K Lat
42 eqid Base K = Base K
43 42 2 4 hlatjcl K HL P A Q A P ˙ Q Base K
44 6 8 12 43 syl3anc K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q Base K
45 42 2 4 hlatjcl K HL S A T A S ˙ T Base K
46 6 9 13 45 syl3anc K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A S ˙ T Base K
47 42 3 latmcom K Lat P ˙ Q Base K S ˙ T Base K P ˙ Q ˙ S ˙ T = S ˙ T ˙ P ˙ Q
48 41 44 46 47 syl3anc K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T = S ˙ T ˙ P ˙ Q
49 42 2 4 hlatjcl K HL Q A R A Q ˙ R Base K
50 6 12 33 49 syl3anc K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ R Base K
51 42 2 4 hlatjcl K HL T A U A T ˙ U Base K
52 6 13 32 51 syl3anc K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A T ˙ U Base K
53 42 3 latmcom K Lat Q ˙ R Base K T ˙ U Base K Q ˙ R ˙ T ˙ U = T ˙ U ˙ Q ˙ R
54 41 50 52 53 syl3anc K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ R ˙ T ˙ U = T ˙ U ˙ Q ˙ R
55 42 2 4 hlatjcl K HL R A P A R ˙ P Base K
56 6 33 8 55 syl3anc K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A R ˙ P Base K
57 42 2 4 hlatjcl K HL U A S A U ˙ S Base K
58 6 32 9 57 syl3anc K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A U ˙ S Base K
59 42 3 latmcom K Lat R ˙ P Base K U ˙ S Base K R ˙ P ˙ U ˙ S = U ˙ S ˙ R ˙ P
60 41 56 58 59 syl3anc K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A R ˙ P ˙ U ˙ S = U ˙ S ˙ R ˙ P
61 54 60 oveq12d K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S = T ˙ U ˙ Q ˙ R ˙ U ˙ S ˙ R ˙ P
62 40 48 61 3brtr4d K HL ¬ S ˙ T ˙ U O ¬ P ˙ S ˙ Q ˙ T ˙ S ˙ T ¬ P ˙ S ˙ Q ˙ T ˙ T ˙ U ¬ P ˙ S ˙ Q ˙ T ˙ U ˙ S P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S