Metamath Proof Explorer


Theorem cdleme41snaw

Description: Part of proof of Lemma E in Crawley p. 113. Show that f(r) is for combined cases; compare cdleme32snaw . TODO: FIX COMMENT. (Contributed by NM, 18-Mar-2013)

Ref Expression
Hypotheses cdleme41.b B = Base K
cdleme41.l ˙ = K
cdleme41.j ˙ = join K
cdleme41.m ˙ = meet K
cdleme41.a A = Atoms K
cdleme41.h H = LHyp K
cdleme41.u U = P ˙ Q ˙ W
cdleme41.d D = s ˙ U ˙ Q ˙ P ˙ s ˙ W
cdleme41.e E = t ˙ U ˙ Q ˙ P ˙ t ˙ W
cdleme41.g G = P ˙ Q ˙ E ˙ s ˙ t ˙ W
cdleme41.i I = ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = G
cdleme41.n N = if s ˙ P ˙ Q I D
Assertion cdleme41snaw K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S R / s N S / s N

Proof

Step Hyp Ref Expression
1 cdleme41.b B = Base K
2 cdleme41.l ˙ = K
3 cdleme41.j ˙ = join K
4 cdleme41.m ˙ = meet K
5 cdleme41.a A = Atoms K
6 cdleme41.h H = LHyp K
7 cdleme41.u U = P ˙ Q ˙ W
8 cdleme41.d D = s ˙ U ˙ Q ˙ P ˙ s ˙ W
9 cdleme41.e E = t ˙ U ˙ Q ˙ P ˙ t ˙ W
10 cdleme41.g G = P ˙ Q ˙ E ˙ s ˙ t ˙ W
11 cdleme41.i I = ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = G
12 cdleme41.n N = if s ˙ P ˙ Q I D
13 simpl1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S R ˙ P ˙ Q S ˙ P ˙ Q K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W
14 simpl21 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S R ˙ P ˙ Q S ˙ P ˙ Q P Q
15 simpl22 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S R ˙ P ˙ Q S ˙ P ˙ Q R A ¬ R ˙ W
16 simpl23 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S R ˙ P ˙ Q S ˙ P ˙ Q S A ¬ S ˙ W
17 simprl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S R ˙ P ˙ Q S ˙ P ˙ Q R ˙ P ˙ Q
18 simprr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S R ˙ P ˙ Q S ˙ P ˙ Q S ˙ P ˙ Q
19 simpl3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S R ˙ P ˙ Q S ˙ P ˙ Q R S
20 eqid u ˙ U ˙ Q ˙ P ˙ u ˙ W = u ˙ U ˙ Q ˙ P ˙ u ˙ W
21 1 2 3 4 5 6 7 9 10 11 12 8 20 cdleme40w K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R ˙ P ˙ Q S ˙ P ˙ Q R S R / s N S / s N
22 13 14 15 16 17 18 19 21 syl133anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S R ˙ P ˙ Q S ˙ P ˙ Q R / s N S / s N
23 simpl1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S R ˙ P ˙ Q ¬ S ˙ P ˙ Q K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W
24 simpl21 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S R ˙ P ˙ Q ¬ S ˙ P ˙ Q P Q
25 simpl22 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S R ˙ P ˙ Q ¬ S ˙ P ˙ Q R A ¬ R ˙ W
26 simpl23 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S R ˙ P ˙ Q ¬ S ˙ P ˙ Q S A ¬ S ˙ W
27 simprl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S R ˙ P ˙ Q ¬ S ˙ P ˙ Q R ˙ P ˙ Q
28 simprr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S R ˙ P ˙ Q ¬ S ˙ P ˙ Q ¬ S ˙ P ˙ Q
29 simpl3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S R ˙ P ˙ Q ¬ S ˙ P ˙ Q R S
30 1 2 3 4 5 6 7 8 9 10 11 12 cdleme41sn3aw K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R ˙ P ˙ Q ¬ S ˙ P ˙ Q R S R / s N S / s N
31 23 24 25 26 27 28 29 30 syl133anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S R ˙ P ˙ Q ¬ S ˙ P ˙ Q R / s N S / s N
32 simpl1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S ¬ R ˙ P ˙ Q S ˙ P ˙ Q K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W
33 simpl21 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S ¬ R ˙ P ˙ Q S ˙ P ˙ Q P Q
34 simpl22 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S ¬ R ˙ P ˙ Q S ˙ P ˙ Q R A ¬ R ˙ W
35 simpl23 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S ¬ R ˙ P ˙ Q S ˙ P ˙ Q S A ¬ S ˙ W
36 simprl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S ¬ R ˙ P ˙ Q S ˙ P ˙ Q ¬ R ˙ P ˙ Q
37 simprr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S ¬ R ˙ P ˙ Q S ˙ P ˙ Q S ˙ P ˙ Q
38 simpl3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S ¬ R ˙ P ˙ Q S ˙ P ˙ Q R S
39 1 2 3 4 5 6 7 8 9 10 11 12 cdleme41sn4aw K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W ¬ R ˙ P ˙ Q S ˙ P ˙ Q R S R / s N S / s N
40 32 33 34 35 36 37 38 39 syl133anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S ¬ R ˙ P ˙ Q S ˙ P ˙ Q R / s N S / s N
41 simpl1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W
42 simpl21 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q P Q
43 simpl22 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q R A ¬ R ˙ W
44 simpl23 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q S A ¬ S ˙ W
45 simprl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ¬ R ˙ P ˙ Q
46 simprr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q ¬ S ˙ P ˙ Q
47 simpl3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q R S
48 1 2 3 4 5 6 7 8 12 cdleme35sn2aw K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q R S R / s N S / s N
49 41 42 43 44 45 46 47 48 syl133anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S ¬ R ˙ P ˙ Q ¬ S ˙ P ˙ Q R / s N S / s N
50 22 31 40 49 4casesdan K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W S A ¬ S ˙ W R S R / s N S / s N