Metamath Proof Explorer


Theorem cdleme17d2

Description: Part of proof of Lemma E in Crawley p. 114, first part of 4th paragraph. F , G represent f(s), f_s(p) respectively. We show, in their notation, f_s(p)=q. TODO: FIX COMMENT. (Contributed by NM, 5-Apr-2013)

Ref Expression
Hypotheses cdlemef46.b B = Base K
cdlemef46.l ˙ = K
cdlemef46.j ˙ = join K
cdlemef46.m ˙ = meet K
cdlemef46.a A = Atoms K
cdlemef46.h H = LHyp K
cdlemef46.u U = P ˙ Q ˙ W
cdlemef46.d D = t ˙ U ˙ Q ˙ P ˙ t ˙ W
cdlemefs46.e E = P ˙ Q ˙ D ˙ s ˙ t ˙ W
cdlemef46.f F = x B if P Q ¬ x ˙ W ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = if s ˙ P ˙ Q ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E s / t D ˙ x ˙ W x
Assertion cdleme17d2 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q F P = Q

Proof

Step Hyp Ref Expression
1 cdlemef46.b B = Base K
2 cdlemef46.l ˙ = K
3 cdlemef46.j ˙ = join K
4 cdlemef46.m ˙ = meet K
5 cdlemef46.a A = Atoms K
6 cdlemef46.h H = LHyp K
7 cdlemef46.u U = P ˙ Q ˙ W
8 cdlemef46.d D = t ˙ U ˙ Q ˙ P ˙ t ˙ W
9 cdlemefs46.e E = P ˙ Q ˙ D ˙ s ˙ t ˙ W
10 cdlemef46.f F = x B if P Q ¬ x ˙ W ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = if s ˙ P ˙ Q ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E s / t D ˙ x ˙ W x
11 simp1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W
12 simp2l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q P Q
13 simp12 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q P A ¬ P ˙ W
14 simp2r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q S A ¬ S ˙ W
15 simp11l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q K HL
16 simp12l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q P A
17 simp13l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q Q A
18 2 3 5 hlatlej1 K HL P A Q A P ˙ P ˙ Q
19 15 16 17 18 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q P ˙ P ˙ Q
20 simp3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q ¬ S ˙ P ˙ Q
21 1 2 3 4 5 6 7 8 10 9 cdlemefs45 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q P A ¬ P ˙ W S A ¬ S ˙ W P ˙ P ˙ Q ¬ S ˙ P ˙ Q F P = P / s S / t E
22 11 12 13 14 19 20 21 syl132anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q F P = P / s S / t E
23 simp2rl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q S A
24 eqid S ˙ U ˙ Q ˙ P ˙ S ˙ W = S ˙ U ˙ Q ˙ P ˙ S ˙ W
25 eqid P ˙ Q ˙ S ˙ U ˙ Q ˙ P ˙ S ˙ W ˙ P ˙ S ˙ W = P ˙ Q ˙ S ˙ U ˙ Q ˙ P ˙ S ˙ W ˙ P ˙ S ˙ W
26 8 9 24 25 cdleme31sde P A S A P / s S / t E = P ˙ Q ˙ S ˙ U ˙ Q ˙ P ˙ S ˙ W ˙ P ˙ S ˙ W
27 16 23 26 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q P / s S / t E = P ˙ Q ˙ S ˙ U ˙ Q ˙ P ˙ S ˙ W ˙ P ˙ S ˙ W
28 simp11 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q K HL W H
29 2 3 4 5 6 7 24 25 cdleme17d1 K HL W H P A ¬ P ˙ W Q A S A ¬ S ˙ W ¬ S ˙ P ˙ Q P ˙ Q ˙ S ˙ U ˙ Q ˙ P ˙ S ˙ W ˙ P ˙ S ˙ W = Q
30 28 13 17 14 20 29 syl131anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q P ˙ Q ˙ S ˙ U ˙ Q ˙ P ˙ S ˙ W ˙ P ˙ S ˙ W = Q
31 22 27 30 3eqtrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q S A ¬ S ˙ W ¬ S ˙ P ˙ Q F P = Q