Metamath Proof Explorer


Theorem 4atlem12b

Description: Lemma for 4at . Substitute T for P (cont.). (Contributed by NM, 11-Jul-2012)

Ref Expression
Hypotheses 4at.l ˙ = K
4at.j ˙ = join K
4at.a A = Atoms K
Assertion 4atlem12b K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W P ˙ Q ˙ R ˙ S = T ˙ U ˙ V ˙ W

Proof

Step Hyp Ref Expression
1 4at.l ˙ = K
2 4at.j ˙ = join K
3 4at.a A = Atoms K
4 simp11 K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W K HL P A Q A
5 simp121 K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W R A
6 simp122 K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W S A
7 5 6 jca K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W R A S A
8 simp13 K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W U A V A W A
9 4 7 8 3jca K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W K HL P A Q A R A S A U A V A W A
10 simp2l K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R
11 9 10 jca K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R
12 simp3lr K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W
13 simp3rl K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W
14 simp3rr K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W
15 simp111 K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W K HL
16 15 hllatd K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W K Lat
17 eqid Base K = Base K
18 17 3 atbase R A R Base K
19 5 18 syl K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W R Base K
20 17 3 atbase S A S Base K
21 6 20 syl K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W S Base K
22 simp123 K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W T A
23 simp131 K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W U A
24 17 2 3 hlatjcl K HL T A U A T ˙ U Base K
25 15 22 23 24 syl3anc K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W T ˙ U Base K
26 simp132 K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W V A
27 simp133 K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W W A
28 17 2 3 hlatjcl K HL V A W A V ˙ W Base K
29 15 26 27 28 syl3anc K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W V ˙ W Base K
30 17 2 latjcl K Lat T ˙ U Base K V ˙ W Base K T ˙ U ˙ V ˙ W Base K
31 16 25 29 30 syl3anc K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W T ˙ U ˙ V ˙ W Base K
32 17 1 2 latjle12 K Lat R Base K S Base K T ˙ U ˙ V ˙ W Base K R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W R ˙ S ˙ T ˙ U ˙ V ˙ W
33 16 19 21 31 32 syl13anc K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W R ˙ S ˙ T ˙ U ˙ V ˙ W
34 13 14 33 mpbi2and K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W R ˙ S ˙ T ˙ U ˙ V ˙ W
35 simp113 K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W Q A
36 17 3 atbase Q A Q Base K
37 35 36 syl K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W Q Base K
38 17 2 3 hlatjcl K HL R A S A R ˙ S Base K
39 15 5 6 38 syl3anc K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W R ˙ S Base K
40 17 1 2 latjle12 K Lat Q Base K R ˙ S Base K T ˙ U ˙ V ˙ W Base K Q ˙ T ˙ U ˙ V ˙ W R ˙ S ˙ T ˙ U ˙ V ˙ W Q ˙ R ˙ S ˙ T ˙ U ˙ V ˙ W
41 16 37 39 31 40 syl13anc K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ S ˙ T ˙ U ˙ V ˙ W Q ˙ R ˙ S ˙ T ˙ U ˙ V ˙ W
42 12 34 41 mpbi2and K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W Q ˙ R ˙ S ˙ T ˙ U ˙ V ˙ W
43 simp3ll K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W
44 simp112 K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W P A
45 simp2r K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W ¬ P ˙ U ˙ V ˙ W
46 1 2 3 4atlem12a K HL P A T A U A V A W A ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W P ˙ U ˙ V ˙ W = T ˙ U ˙ V ˙ W
47 15 44 22 8 45 46 syl311anc K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W P ˙ U ˙ V ˙ W = T ˙ U ˙ V ˙ W
48 43 47 mpbid K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W P ˙ U ˙ V ˙ W = T ˙ U ˙ V ˙ W
49 42 48 breqtrrd K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W Q ˙ R ˙ S ˙ P ˙ U ˙ V ˙ W
50 1 2 3 4atlem11 K HL P A Q A R A S A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R Q ˙ R ˙ S ˙ P ˙ U ˙ V ˙ W P ˙ Q ˙ R ˙ S = P ˙ U ˙ V ˙ W
51 11 49 50 sylc K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W P ˙ Q ˙ R ˙ S = P ˙ U ˙ V ˙ W
52 51 48 eqtrd K HL P A Q A R A S A T A U A V A W A P Q ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ˙ R ¬ P ˙ U ˙ V ˙ W P ˙ T ˙ U ˙ V ˙ W Q ˙ T ˙ U ˙ V ˙ W R ˙ T ˙ U ˙ V ˙ W S ˙ T ˙ U ˙ V ˙ W P ˙ Q ˙ R ˙ S = T ˙ U ˙ V ˙ W