Metamath Proof Explorer


Theorem cdleme40w

Description: Part of proof of Lemma E in Crawley p. 113. Apply cdleme40v bound variable change to [_ S / u ]_ V . TODO: FIX COMMENT. (Contributed by NM, 19-Mar-2013)

Ref Expression
Hypotheses cdleme40.b B = Base K
cdleme40.l ˙ = K
cdleme40.j ˙ = join K
cdleme40.m ˙ = meet K
cdleme40.a A = Atoms K
cdleme40.h H = LHyp K
cdleme40.u U = P ˙ Q ˙ W
cdleme40.e E = t ˙ U ˙ Q ˙ P ˙ t ˙ W
cdleme40.g G = P ˙ Q ˙ E ˙ s ˙ t ˙ W
cdleme40.i I = ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = G
cdleme40.n N = if s ˙ P ˙ Q I D
cdleme40.d D = s ˙ U ˙ Q ˙ P ˙ s ˙ W
cdleme40r.y Y = u ˙ U ˙ Q ˙ P ˙ u ˙ W
Assertion 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

Proof

Step Hyp Ref Expression
1 cdleme40.b B = Base K
2 cdleme40.l ˙ = K
3 cdleme40.j ˙ = join K
4 cdleme40.m ˙ = meet K
5 cdleme40.a A = Atoms K
6 cdleme40.h H = LHyp K
7 cdleme40.u U = P ˙ Q ˙ W
8 cdleme40.e E = t ˙ U ˙ Q ˙ P ˙ t ˙ W
9 cdleme40.g G = P ˙ Q ˙ E ˙ s ˙ t ˙ W
10 cdleme40.i I = ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = G
11 cdleme40.n N = if s ˙ P ˙ Q I D
12 cdleme40.d D = s ˙ U ˙ Q ˙ P ˙ s ˙ W
13 cdleme40r.y Y = u ˙ U ˙ Q ˙ P ˙ u ˙ W
14 eqid P ˙ Q ˙ E ˙ R ˙ t ˙ W = P ˙ Q ˙ E ˙ R ˙ t ˙ W
15 eqid ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = P ˙ Q ˙ E ˙ R ˙ t ˙ W = ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = P ˙ Q ˙ E ˙ R ˙ t ˙ W
16 eqid v ˙ U ˙ Q ˙ P ˙ v ˙ W = v ˙ U ˙ Q ˙ P ˙ v ˙ W
17 eqid P ˙ Q ˙ v ˙ U ˙ Q ˙ P ˙ v ˙ W ˙ S ˙ v ˙ W = P ˙ Q ˙ v ˙ U ˙ Q ˙ P ˙ v ˙ W ˙ S ˙ v ˙ W
18 eqid P ˙ Q ˙ v ˙ U ˙ Q ˙ P ˙ v ˙ W ˙ u ˙ v ˙ W = P ˙ Q ˙ v ˙ U ˙ Q ˙ P ˙ v ˙ W ˙ u ˙ v ˙ W
19 eqid ι z B | v A ¬ v ˙ W ¬ v ˙ P ˙ Q z = P ˙ Q ˙ v ˙ U ˙ Q ˙ P ˙ v ˙ W ˙ u ˙ v ˙ W = ι z B | v A ¬ v ˙ W ¬ v ˙ P ˙ Q z = P ˙ Q ˙ v ˙ U ˙ Q ˙ P ˙ v ˙ W ˙ u ˙ v ˙ W
20 eqid if u ˙ P ˙ Q ι z B | v A ¬ v ˙ W ¬ v ˙ P ˙ Q z = P ˙ Q ˙ v ˙ U ˙ Q ˙ P ˙ v ˙ W ˙ u ˙ v ˙ W u ˙ U ˙ Q ˙ P ˙ u ˙ W = if u ˙ P ˙ Q ι z B | v A ¬ v ˙ W ¬ v ˙ P ˙ Q z = P ˙ Q ˙ v ˙ U ˙ Q ˙ P ˙ v ˙ W ˙ u ˙ v ˙ W u ˙ U ˙ Q ˙ P ˙ u ˙ W
21 eqid ι z B | v A ¬ v ˙ W ¬ v ˙ P ˙ Q z = P ˙ Q ˙ v ˙ U ˙ Q ˙ P ˙ v ˙ W ˙ S ˙ v ˙ W = ι z B | v A ¬ v ˙ W ¬ v ˙ P ˙ Q z = P ˙ Q ˙ v ˙ U ˙ Q ˙ P ˙ v ˙ W ˙ S ˙ v ˙ W
22 1 2 3 4 5 6 7 8 9 10 11 14 15 16 17 18 19 20 21 cdleme40n 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 / u if u ˙ P ˙ Q ι z B | v A ¬ v ˙ W ¬ v ˙ P ˙ Q z = P ˙ Q ˙ v ˙ U ˙ Q ˙ P ˙ v ˙ W ˙ u ˙ v ˙ W u ˙ U ˙ Q ˙ P ˙ u ˙ W
23 simp23l 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 S A
24 eqid u ˙ U ˙ Q ˙ P ˙ u ˙ W = u ˙ U ˙ Q ˙ P ˙ u ˙ W
25 1 2 3 4 5 6 7 8 9 10 11 12 24 16 18 19 20 cdleme40v S A S / s N = S / u if u ˙ P ˙ Q ι z B | v A ¬ v ˙ W ¬ v ˙ P ˙ Q z = P ˙ Q ˙ v ˙ U ˙ Q ˙ P ˙ v ˙ W ˙ u ˙ v ˙ W u ˙ U ˙ Q ˙ P ˙ u ˙ W
26 23 25 syl 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 S / s N = S / u if u ˙ P ˙ Q ι z B | v A ¬ v ˙ W ¬ v ˙ P ˙ Q z = P ˙ Q ˙ v ˙ U ˙ Q ˙ P ˙ v ˙ W ˙ u ˙ v ˙ W u ˙ U ˙ Q ˙ P ˙ u ˙ W
27 22 26 neeqtrrd 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