Metamath Proof Explorer


Theorem cdleme27b

Description: Lemma for cdleme27N . (Contributed by NM, 3-Feb-2013)

Ref Expression
Hypotheses cdleme26.b B = Base K
cdleme26.l ˙ = K
cdleme26.j ˙ = join K
cdleme26.m ˙ = meet K
cdleme26.a A = Atoms K
cdleme26.h H = LHyp K
cdleme27.u U = P ˙ Q ˙ W
cdleme27.f F = s ˙ U ˙ Q ˙ P ˙ s ˙ W
cdleme27.z Z = z ˙ U ˙ Q ˙ P ˙ z ˙ W
cdleme27.n N = P ˙ Q ˙ Z ˙ s ˙ z ˙ W
cdleme27.d D = ι u B | z A ¬ z ˙ W ¬ z ˙ P ˙ Q u = N
cdleme27.c C = if s ˙ P ˙ Q D F
cdleme27.g G = t ˙ U ˙ Q ˙ P ˙ t ˙ W
cdleme27.o O = P ˙ Q ˙ Z ˙ t ˙ z ˙ W
cdleme27.e E = ι u B | z A ¬ z ˙ W ¬ z ˙ P ˙ Q u = O
cdleme27.y Y = if t ˙ P ˙ Q E G
Assertion cdleme27b s = t C = Y

Proof

Step Hyp Ref Expression
1 cdleme26.b B = Base K
2 cdleme26.l ˙ = K
3 cdleme26.j ˙ = join K
4 cdleme26.m ˙ = meet K
5 cdleme26.a A = Atoms K
6 cdleme26.h H = LHyp K
7 cdleme27.u U = P ˙ Q ˙ W
8 cdleme27.f F = s ˙ U ˙ Q ˙ P ˙ s ˙ W
9 cdleme27.z Z = z ˙ U ˙ Q ˙ P ˙ z ˙ W
10 cdleme27.n N = P ˙ Q ˙ Z ˙ s ˙ z ˙ W
11 cdleme27.d D = ι u B | z A ¬ z ˙ W ¬ z ˙ P ˙ Q u = N
12 cdleme27.c C = if s ˙ P ˙ Q D F
13 cdleme27.g G = t ˙ U ˙ Q ˙ P ˙ t ˙ W
14 cdleme27.o O = P ˙ Q ˙ Z ˙ t ˙ z ˙ W
15 cdleme27.e E = ι u B | z A ¬ z ˙ W ¬ z ˙ P ˙ Q u = O
16 cdleme27.y Y = if t ˙ P ˙ Q E G
17 breq1 s = t s ˙ P ˙ Q t ˙ P ˙ Q
18 oveq1 s = t s ˙ z = t ˙ z
19 18 oveq1d s = t s ˙ z ˙ W = t ˙ z ˙ W
20 19 oveq2d s = t Z ˙ s ˙ z ˙ W = Z ˙ t ˙ z ˙ W
21 20 oveq2d s = t P ˙ Q ˙ Z ˙ s ˙ z ˙ W = P ˙ Q ˙ Z ˙ t ˙ z ˙ W
22 21 10 14 3eqtr4g s = t N = O
23 22 eqeq2d s = t u = N u = O
24 23 imbi2d s = t ¬ z ˙ W ¬ z ˙ P ˙ Q u = N ¬ z ˙ W ¬ z ˙ P ˙ Q u = O
25 24 ralbidv s = t z A ¬ z ˙ W ¬ z ˙ P ˙ Q u = N z A ¬ z ˙ W ¬ z ˙ P ˙ Q u = O
26 25 riotabidv s = t ι u B | z A ¬ z ˙ W ¬ z ˙ P ˙ Q u = N = ι u B | z A ¬ z ˙ W ¬ z ˙ P ˙ Q u = O
27 26 11 15 3eqtr4g s = t D = E
28 oveq1 s = t s ˙ U = t ˙ U
29 oveq2 s = t P ˙ s = P ˙ t
30 29 oveq1d s = t P ˙ s ˙ W = P ˙ t ˙ W
31 30 oveq2d s = t Q ˙ P ˙ s ˙ W = Q ˙ P ˙ t ˙ W
32 28 31 oveq12d s = t s ˙ U ˙ Q ˙ P ˙ s ˙ W = t ˙ U ˙ Q ˙ P ˙ t ˙ W
33 32 8 13 3eqtr4g s = t F = G
34 17 27 33 ifbieq12d s = t if s ˙ P ˙ Q D F = if t ˙ P ˙ Q E G
35 34 12 16 3eqtr4g s = t C = Y