Metamath Proof Explorer


Theorem 3atlem5

Description: Lemma for 3at . (Contributed by NM, 23-Jun-2012)

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

Proof

Step Hyp Ref Expression
1 3at.l ˙ = K
2 3at.j ˙ = join K
3 3at.a A = Atoms K
4 oveq2 U = P S ˙ T ˙ U = S ˙ T ˙ P
5 4 eqcoms P = U S ˙ T ˙ U = S ˙ T ˙ P
6 5 breq2d P = U P ˙ Q ˙ R ˙ S ˙ T ˙ U P ˙ Q ˙ R ˙ S ˙ T ˙ P
7 5 eqeq2d P = U P ˙ Q ˙ R = S ˙ T ˙ U P ˙ Q ˙ R = S ˙ T ˙ P
8 6 7 imbi12d P = U P ˙ Q ˙ R ˙ S ˙ T ˙ U P ˙ Q ˙ R = S ˙ T ˙ U P ˙ Q ˙ R ˙ S ˙ T ˙ P P ˙ Q ˙ R = S ˙ T ˙ P
9 simp1l K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U P U P ˙ Q ˙ R ˙ S ˙ T ˙ U K HL P A Q A R A S A T A U A
10 simp1r1 K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U P U P ˙ Q ˙ R ˙ S ˙ T ˙ U ¬ R ˙ P ˙ Q
11 simp2 K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U P U P ˙ Q ˙ R ˙ S ˙ T ˙ U P U
12 simp1r3 K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U P U P ˙ Q ˙ R ˙ S ˙ T ˙ U ¬ Q ˙ P ˙ U
13 simp3 K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U P U P ˙ Q ˙ R ˙ S ˙ T ˙ U P ˙ Q ˙ R ˙ S ˙ T ˙ U
14 1 2 3 3atlem3 K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P U ¬ Q ˙ P ˙ U P ˙ Q ˙ R ˙ S ˙ T ˙ U P ˙ Q ˙ R = S ˙ T ˙ U
15 9 10 11 12 13 14 syl131anc K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U P U P ˙ Q ˙ R ˙ S ˙ T ˙ U P ˙ Q ˙ R = S ˙ T ˙ U
16 15 3expia K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U P U P ˙ Q ˙ R ˙ S ˙ T ˙ U P ˙ Q ˙ R = S ˙ T ˙ U
17 simp11 K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U R ˙ Q ˙ P ˙ S ˙ T ˙ P K HL
18 simp123 K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U R ˙ Q ˙ P ˙ S ˙ T ˙ P R A
19 simp122 K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U R ˙ Q ˙ P ˙ S ˙ T ˙ P Q A
20 simp121 K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U R ˙ Q ˙ P ˙ S ˙ T ˙ P P A
21 18 19 20 3jca K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U R ˙ Q ˙ P ˙ S ˙ T ˙ P R A Q A P A
22 simp131 K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U R ˙ Q ˙ P ˙ S ˙ T ˙ P S A
23 simp132 K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U R ˙ Q ˙ P ˙ S ˙ T ˙ P T A
24 22 23 jca K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U R ˙ Q ˙ P ˙ S ˙ T ˙ P S A T A
25 simp21 K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U R ˙ Q ˙ P ˙ S ˙ T ˙ P ¬ R ˙ P ˙ Q
26 simp22 K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U R ˙ Q ˙ P ˙ S ˙ T ˙ P P Q
27 1 2 3 hlatexch2 K HL P A R A Q A P Q P ˙ R ˙ Q R ˙ P ˙ Q
28 17 20 18 19 26 27 syl131anc K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U R ˙ Q ˙ P ˙ S ˙ T ˙ P P ˙ R ˙ Q R ˙ P ˙ Q
29 25 28 mtod K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U R ˙ Q ˙ P ˙ S ˙ T ˙ P ¬ P ˙ R ˙ Q
30 17 hllatd K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U R ˙ Q ˙ P ˙ S ˙ T ˙ P K Lat
31 eqid Base K = Base K
32 31 3 atbase R A R Base K
33 18 32 syl K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U R ˙ Q ˙ P ˙ S ˙ T ˙ P R Base K
34 31 3 atbase P A P Base K
35 20 34 syl K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U R ˙ Q ˙ P ˙ S ˙ T ˙ P P Base K
36 31 3 atbase Q A Q Base K
37 19 36 syl K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U R ˙ Q ˙ P ˙ S ˙ T ˙ P Q Base K
38 31 1 2 latnlej1r K Lat R Base K P Base K Q Base K ¬ R ˙ P ˙ Q R Q
39 30 33 35 37 25 38 syl131anc K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U R ˙ Q ˙ P ˙ S ˙ T ˙ P R Q
40 simp3 K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U R ˙ Q ˙ P ˙ S ˙ T ˙ P R ˙ Q ˙ P ˙ S ˙ T ˙ P
41 1 2 3 3atlem4 K HL R A Q A P A S A T A ¬ P ˙ R ˙ Q R Q R ˙ Q ˙ P ˙ S ˙ T ˙ P R ˙ Q ˙ P = S ˙ T ˙ P
42 17 21 24 29 39 40 41 syl321anc K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U R ˙ Q ˙ P ˙ S ˙ T ˙ P R ˙ Q ˙ P = S ˙ T ˙ P
43 42 3expia K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U R ˙ Q ˙ P ˙ S ˙ T ˙ P R ˙ Q ˙ P = S ˙ T ˙ P
44 simpl1 K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U K HL
45 44 hllatd K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U K Lat
46 simpl21 K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U P A
47 46 34 syl K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U P Base K
48 simpl22 K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U Q A
49 48 36 syl K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U Q Base K
50 simpl23 K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U R A
51 50 32 syl K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U R Base K
52 31 2 latj31 K Lat P Base K Q Base K R Base K P ˙ Q ˙ R = R ˙ Q ˙ P
53 45 47 49 51 52 syl13anc K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U P ˙ Q ˙ R = R ˙ Q ˙ P
54 53 breq1d K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U P ˙ Q ˙ R ˙ S ˙ T ˙ P R ˙ Q ˙ P ˙ S ˙ T ˙ P
55 53 eqeq1d K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U P ˙ Q ˙ R = S ˙ T ˙ P R ˙ Q ˙ P = S ˙ T ˙ P
56 43 54 55 3imtr4d K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U P ˙ Q ˙ R ˙ S ˙ T ˙ P P ˙ Q ˙ R = S ˙ T ˙ P
57 8 16 56 pm2.61ne K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U P ˙ Q ˙ R ˙ S ˙ T ˙ U P ˙ Q ˙ R = S ˙ T ˙ U
58 57 3impia K HL P A Q A R A S A T A U A ¬ R ˙ P ˙ Q P Q ¬ Q ˙ P ˙ U P ˙ Q ˙ R ˙ S ˙ T ˙ U P ˙ Q ˙ R = S ˙ T ˙ U