Step |
Hyp |
Ref |
Expression |
1 |
|
cdleme40.b |
|- B = ( Base ` K ) |
2 |
|
cdleme40.l |
|- .<_ = ( le ` 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 = ( iota_ y e. B A. t e. 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 = ( iota_ z e. B A. v e. 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 -> ( A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = G ) <-> A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = ( ( P .\/ Q ) ./\ ( E .\/ ( ( u .\/ t ) ./\ W ) ) ) ) ) ) |
27 |
26
|
riotabidv |
|- ( s = u -> ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = G ) ) = ( iota_ y e. B A. t e. 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 -> ( A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = ( ( P .\/ Q ) ./\ ( E .\/ ( ( u .\/ t ) ./\ W ) ) ) ) <-> A. t e. 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 |
|- ( A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> z = ( ( P .\/ Q ) ./\ ( E .\/ ( ( u .\/ t ) ./\ W ) ) ) ) <-> A. v e. A ( ( -. v .<_ W /\ -. v .<_ ( P .\/ Q ) ) -> z = X ) ) |
50 |
30 49
|
bitrdi |
|- ( y = z -> ( A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = ( ( P .\/ Q ) ./\ ( E .\/ ( ( u .\/ t ) ./\ W ) ) ) ) <-> A. v e. A ( ( -. v .<_ W /\ -. v .<_ ( P .\/ Q ) ) -> z = X ) ) ) |
51 |
50
|
cbvriotavw |
|- ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = ( ( P .\/ Q ) ./\ ( E .\/ ( ( u .\/ t ) ./\ W ) ) ) ) ) = ( iota_ z e. B A. v e. A ( ( -. v .<_ W /\ -. v .<_ ( P .\/ Q ) ) -> z = X ) ) |
52 |
27 51
|
eqtrdi |
|- ( s = u -> ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = G ) ) = ( iota_ z e. B A. v e. 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 e. A -> [_ R / s ]_ N = [_ R / u ]_ V ) |