Metamath Proof Explorer


Theorem cdleme40v

Description: Part of proof of Lemma E in Crawley p. 113. Change bound variables in [_ S / u ]_ V (but we use [_ R / u ]_ V for convenience since we have its hypotheses available). (Contributed by NM, 18-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
cdleme40r.t T = v ˙ U ˙ Q ˙ P ˙ v ˙ W
cdleme40r.x X = P ˙ Q ˙ T ˙ u ˙ v ˙ W
cdleme40r.o O = ι z B | v A ¬ v ˙ W ¬ v ˙ P ˙ Q z = X
cdleme40r.v V = if u ˙ P ˙ Q O Y
Assertion cdleme40v R A R / s N = R / u V

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 cdleme40r.t T = v ˙ U ˙ Q ˙ P ˙ v ˙ W
15 cdleme40r.x X = P ˙ Q ˙ T ˙ u ˙ v ˙ W
16 cdleme40r.o O = ι z B | v A ¬ v ˙ W ¬ v ˙ P ˙ Q z = X
17 cdleme40r.v V = if u ˙ P ˙ Q O Y
18 breq1 s = u s ˙ P ˙ Q u ˙ P ˙ Q
19 oveq1 s = u s ˙ t = u ˙ t
20 19 oveq1d s = u s ˙ t ˙ W = u ˙ t ˙ W
21 20 oveq2d s = u E ˙ s ˙ t ˙ W = E ˙ u ˙ t ˙ W
22 21 oveq2d s = u P ˙ Q ˙ E ˙ s ˙ t ˙ W = P ˙ Q ˙ E ˙ u ˙ t ˙ W
23 9 22 syl5eq s = u G = P ˙ Q ˙ E ˙ u ˙ t ˙ W
24 23 eqeq2d s = u y = G y = P ˙ Q ˙ E ˙ u ˙ t ˙ W
25 24 imbi2d s = u ¬ t ˙ W ¬ t ˙ P ˙ Q y = G ¬ t ˙ W ¬ t ˙ P ˙ Q y = P ˙ Q ˙ E ˙ u ˙ t ˙ W
26 25 ralbidv s = u t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = G t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = P ˙ Q ˙ E ˙ u ˙ t ˙ W
27 26 riotabidv s = u ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = G = ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = P ˙ Q ˙ E ˙ u ˙ t ˙ W
28 eqeq1 y = z y = P ˙ Q ˙ E ˙ u ˙ t ˙ W z = P ˙ Q ˙ E ˙ u ˙ t ˙ W
29 28 imbi2d y = z ¬ t ˙ W ¬ t ˙ P ˙ Q y = P ˙ Q ˙ E ˙ u ˙ t ˙ W ¬ t ˙ W ¬ t ˙ P ˙ Q z = P ˙ Q ˙ E ˙ u ˙ t ˙ W
30 29 ralbidv y = z t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = P ˙ Q ˙ E ˙ u ˙ t ˙ W t A ¬ t ˙ W ¬ t ˙ P ˙ Q z = P ˙ Q ˙ E ˙ u ˙ t ˙ W
31 breq1 t = v t ˙ W v ˙ W
32 31 notbid t = v ¬ t ˙ W ¬ v ˙ W
33 breq1 t = v t ˙ P ˙ Q v ˙ P ˙ Q
34 33 notbid t = v ¬ t ˙ P ˙ Q ¬ v ˙ P ˙ Q
35 32 34 anbi12d t = v ¬ t ˙ W ¬ t ˙ P ˙ Q ¬ v ˙ W ¬ v ˙ P ˙ Q
36 oveq1 t = v t ˙ U = v ˙ U
37 oveq2 t = v P ˙ t = P ˙ v
38 37 oveq1d t = v P ˙ t ˙ W = P ˙ v ˙ W
39 38 oveq2d t = v Q ˙ P ˙ t ˙ W = Q ˙ P ˙ v ˙ W
40 36 39 oveq12d t = v t ˙ U ˙ Q ˙ P ˙ t ˙ W = v ˙ U ˙ Q ˙ P ˙ v ˙ W
41 40 8 14 3eqtr4g t = v E = T
42 oveq2 t = v u ˙ t = u ˙ v
43 42 oveq1d t = v u ˙ t ˙ W = u ˙ v ˙ W
44 41 43 oveq12d t = v E ˙ u ˙ t ˙ W = T ˙ u ˙ v ˙ W
45 44 oveq2d t = v P ˙ Q ˙ E ˙ u ˙ t ˙ W = P ˙ Q ˙ T ˙ u ˙ v ˙ W
46 45 15 eqtr4di t = v P ˙ Q ˙ E ˙ u ˙ t ˙ W = X
47 46 eqeq2d t = v z = P ˙ Q ˙ E ˙ u ˙ t ˙ W z = X
48 35 47 imbi12d t = v ¬ t ˙ W ¬ t ˙ P ˙ Q z = P ˙ Q ˙ E ˙ u ˙ t ˙ W ¬ v ˙ W ¬ v ˙ P ˙ Q z = X
49 48 cbvralvw t A ¬ t ˙ W ¬ t ˙ P ˙ Q z = P ˙ Q ˙ E ˙ u ˙ t ˙ W v A ¬ v ˙ W ¬ v ˙ P ˙ Q z = X
50 30 49 bitrdi y = z t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = P ˙ Q ˙ E ˙ u ˙ t ˙ W v A ¬ v ˙ W ¬ v ˙ P ˙ Q z = X
51 50 cbvriotavw ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = P ˙ Q ˙ E ˙ u ˙ t ˙ W = ι z B | v A ¬ v ˙ W ¬ v ˙ P ˙ Q z = X
52 27 51 eqtrdi s = u ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = G = ι z B | v A ¬ v ˙ W ¬ v ˙ P ˙ Q z = X
53 52 10 16 3eqtr4g s = u I = O
54 oveq1 s = u s ˙ U = u ˙ U
55 oveq2 s = u P ˙ s = P ˙ u
56 55 oveq1d s = u P ˙ s ˙ W = P ˙ u ˙ W
57 56 oveq2d s = u Q ˙ P ˙ s ˙ W = Q ˙ P ˙ u ˙ W
58 54 57 oveq12d s = u s ˙ U ˙ Q ˙ P ˙ s ˙ W = u ˙ U ˙ Q ˙ P ˙ u ˙ W
59 58 12 13 3eqtr4g s = u D = Y
60 18 53 59 ifbieq12d s = u if s ˙ P ˙ Q I D = if u ˙ P ˙ Q O Y
61 60 11 17 3eqtr4g s = u N = V
62 61 cbvcsbv R / s N = R / u V
63 62 a1i R A R / s N = R / u V