Metamath Proof Explorer


Theorem cdleme21j

Description: Combine cdleme20 and cdleme21i to eliminate U .<_ ( S .\/ T ) condition. (Contributed by NM, 29-Nov-2012)

Ref Expression
Hypotheses cdleme21.l ˙ = K
cdleme21.j ˙ = join K
cdleme21.m ˙ = meet K
cdleme21.a A = Atoms K
cdleme21.h H = LHyp K
cdleme21.u U = P ˙ Q ˙ W
cdleme21.f F = S ˙ U ˙ Q ˙ P ˙ S ˙ W
cdleme21g.g G = T ˙ U ˙ Q ˙ P ˙ T ˙ W
cdleme21g.d D = R ˙ S ˙ W
cdleme21g.y Y = R ˙ T ˙ W
cdleme21g.n N = P ˙ Q ˙ F ˙ D
cdleme21g.o O = P ˙ Q ˙ G ˙ Y
Assertion cdleme21j K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q r A ¬ r ˙ W P ˙ r = Q ˙ r N = O

Proof

Step Hyp Ref Expression
1 cdleme21.l ˙ = K
2 cdleme21.j ˙ = join K
3 cdleme21.m ˙ = meet K
4 cdleme21.a A = Atoms K
5 cdleme21.h H = LHyp K
6 cdleme21.u U = P ˙ Q ˙ W
7 cdleme21.f F = S ˙ U ˙ Q ˙ P ˙ S ˙ W
8 cdleme21g.g G = T ˙ U ˙ Q ˙ P ˙ T ˙ W
9 cdleme21g.d D = R ˙ S ˙ W
10 cdleme21g.y Y = R ˙ T ˙ W
11 cdleme21g.n N = P ˙ Q ˙ F ˙ D
12 cdleme21g.o O = P ˙ Q ˙ G ˙ Y
13 simpl33 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q r A ¬ r ˙ W P ˙ r = Q ˙ r U ˙ S ˙ T r A ¬ r ˙ W P ˙ r = Q ˙ r
14 simpl1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q r A ¬ r ˙ W P ˙ r = Q ˙ r U ˙ S ˙ T K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W
15 simp22 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q r A ¬ r ˙ W P ˙ r = Q ˙ r S A ¬ S ˙ W
16 simp23 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q r A ¬ r ˙ W P ˙ r = Q ˙ r T A ¬ T ˙ W
17 simp31l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q r A ¬ r ˙ W P ˙ r = Q ˙ r P Q
18 simp321 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q r A ¬ r ˙ W P ˙ r = Q ˙ r ¬ S ˙ P ˙ Q
19 simp322 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q r A ¬ r ˙ W P ˙ r = Q ˙ r ¬ T ˙ P ˙ Q
20 17 18 19 3jca K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q r A ¬ r ˙ W P ˙ r = Q ˙ r P Q ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q
21 15 16 20 3jca K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q r A ¬ r ˙ W P ˙ r = Q ˙ r S A ¬ S ˙ W T A ¬ T ˙ W P Q ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q
22 21 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q r A ¬ r ˙ W P ˙ r = Q ˙ r U ˙ S ˙ T S A ¬ S ˙ W T A ¬ T ˙ W P Q ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q
23 simpl21 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q r A ¬ r ˙ W P ˙ r = Q ˙ r U ˙ S ˙ T R A ¬ R ˙ W
24 simp323 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q r A ¬ r ˙ W P ˙ r = Q ˙ r R ˙ P ˙ Q
25 24 anim1i K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q r A ¬ r ˙ W P ˙ r = Q ˙ r U ˙ S ˙ T R ˙ P ˙ Q U ˙ S ˙ T
26 1 2 3 4 5 6 7 8 9 10 11 12 cdleme21i K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R A ¬ R ˙ W R ˙ P ˙ Q U ˙ S ˙ T r A ¬ r ˙ W P ˙ r = Q ˙ r N = O
27 14 22 23 25 26 syl112anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q r A ¬ r ˙ W P ˙ r = Q ˙ r U ˙ S ˙ T r A ¬ r ˙ W P ˙ r = Q ˙ r N = O
28 13 27 mpd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q r A ¬ r ˙ W P ˙ r = Q ˙ r U ˙ S ˙ T N = O
29 simpl1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q r A ¬ r ˙ W P ˙ r = Q ˙ r ¬ U ˙ S ˙ T K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W
30 simpl2 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q r A ¬ r ˙ W P ˙ r = Q ˙ r ¬ U ˙ S ˙ T R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W
31 simpl31 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q r A ¬ r ˙ W P ˙ r = Q ˙ r ¬ U ˙ S ˙ T P Q S T
32 simpl32 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q r A ¬ r ˙ W P ˙ r = Q ˙ r ¬ U ˙ S ˙ T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q
33 simpr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q r A ¬ r ˙ W P ˙ r = Q ˙ r ¬ U ˙ S ˙ T ¬ U ˙ S ˙ T
34 eqid S ˙ T ˙ W = S ˙ T ˙ W
35 1 2 3 4 5 6 7 8 9 10 34 11 12 cdleme20 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q ¬ U ˙ S ˙ T N = O
36 29 30 31 32 33 35 syl113anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q r A ¬ r ˙ W P ˙ r = Q ˙ r ¬ U ˙ S ˙ T N = O
37 28 36 pm2.61dan K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q R ˙ P ˙ Q r A ¬ r ˙ W P ˙ r = Q ˙ r N = O