Metamath Proof Explorer


Theorem cdleme15c

Description: Part of proof of Lemma E in Crawley p. 113, 3rd paragraph on p. 114, showing, in their notation, ((p \/ s_1) /\ (q \/ s_1)) \/ ((p \/ t_1) /\ (q \/ t_1))=s_1 \/ t_1. C and X represent s_1 and t_1 respectively. The order of our operations is slightly different. (Contributed by NM, 10-Oct-2012)

Ref Expression
Hypotheses cdleme12.l ˙ = K
cdleme12.j ˙ = join K
cdleme12.m ˙ = meet K
cdleme12.a A = Atoms K
cdleme12.h H = LHyp K
cdleme12.u U = P ˙ Q ˙ W
cdleme12.f F = S ˙ U ˙ Q ˙ P ˙ S ˙ W
cdleme12.g G = T ˙ U ˙ Q ˙ P ˙ T ˙ W
cdleme15.c C = P ˙ S ˙ W
cdleme15.x X = P ˙ T ˙ W
Assertion cdleme15c K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q ¬ U ˙ S ˙ T P ˙ X ˙ Q ˙ X ˙ P ˙ C ˙ Q ˙ C = X ˙ C

Proof

Step Hyp Ref Expression
1 cdleme12.l ˙ = K
2 cdleme12.j ˙ = join K
3 cdleme12.m ˙ = meet K
4 cdleme12.a A = Atoms K
5 cdleme12.h H = LHyp K
6 cdleme12.u U = P ˙ Q ˙ W
7 cdleme12.f F = S ˙ U ˙ Q ˙ P ˙ S ˙ W
8 cdleme12.g G = T ˙ U ˙ Q ˙ P ˙ T ˙ W
9 cdleme15.c C = P ˙ S ˙ W
10 cdleme15.x X = P ˙ T ˙ W
11 simp11 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q ¬ U ˙ S ˙ T K HL W H
12 simp12 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q ¬ U ˙ S ˙ T P A ¬ P ˙ W
13 simp13 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q ¬ U ˙ S ˙ T Q A ¬ Q ˙ W
14 simp22 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q ¬ U ˙ S ˙ T T A ¬ T ˙ W
15 simp21 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q ¬ U ˙ S ˙ T S A ¬ S ˙ W
16 simp23l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q ¬ U ˙ S ˙ T P Q
17 simp23r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q ¬ U ˙ S ˙ T S T
18 17 necomd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q ¬ U ˙ S ˙ T T S
19 16 18 jca K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q ¬ U ˙ S ˙ T P Q T S
20 simp32 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q ¬ U ˙ S ˙ T ¬ T ˙ P ˙ Q
21 simp31 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q ¬ U ˙ S ˙ T ¬ S ˙ P ˙ Q
22 simp33 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q ¬ U ˙ S ˙ T ¬ U ˙ S ˙ T
23 simp11l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q ¬ U ˙ S ˙ T K HL
24 simp21l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q ¬ U ˙ S ˙ T S A
25 simp22l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q ¬ U ˙ S ˙ T T A
26 2 4 hlatjcom K HL S A T A S ˙ T = T ˙ S
27 23 24 25 26 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q ¬ U ˙ S ˙ T S ˙ T = T ˙ S
28 27 breq2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q ¬ U ˙ S ˙ T U ˙ S ˙ T U ˙ T ˙ S
29 22 28 mtbid K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q ¬ U ˙ S ˙ T ¬ U ˙ T ˙ S
30 1 2 3 4 5 6 8 7 10 9 cdleme15b K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W T A ¬ T ˙ W S A ¬ S ˙ W P Q T S ¬ T ˙ P ˙ Q ¬ S ˙ P ˙ Q ¬ U ˙ T ˙ S P ˙ X ˙ Q ˙ X = X
31 11 12 13 14 15 19 20 21 29 30 syl333anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q ¬ U ˙ S ˙ T P ˙ X ˙ Q ˙ X = X
32 1 2 3 4 5 6 7 8 9 10 cdleme15b K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q ¬ U ˙ S ˙ T P ˙ C ˙ Q ˙ C = C
33 31 32 oveq12d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A ¬ S ˙ W T A ¬ T ˙ W P Q S T ¬ S ˙ P ˙ Q ¬ T ˙ P ˙ Q ¬ U ˙ S ˙ T P ˙ X ˙ Q ˙ X ˙ P ˙ C ˙ Q ˙ C = X ˙ C