Step |
Hyp |
Ref |
Expression |
1 |
|
cdleme31sde.c |
|- D = ( ( t .\/ U ) ./\ ( Q .\/ ( ( P .\/ t ) ./\ W ) ) ) |
2 |
|
cdleme31sde.e |
|- E = ( ( P .\/ Q ) ./\ ( D .\/ ( ( s .\/ t ) ./\ W ) ) ) |
3 |
|
cdleme31sde.x |
|- Y = ( ( S .\/ U ) ./\ ( Q .\/ ( ( P .\/ S ) ./\ W ) ) ) |
4 |
|
cdleme31sde.z |
|- Z = ( ( P .\/ Q ) ./\ ( Y .\/ ( ( R .\/ S ) ./\ W ) ) ) |
5 |
2
|
csbeq2i |
|- [_ S / t ]_ E = [_ S / t ]_ ( ( P .\/ Q ) ./\ ( D .\/ ( ( s .\/ t ) ./\ W ) ) ) |
6 |
|
nfcvd |
|- ( S e. A -> F/_ t ( ( P .\/ Q ) ./\ ( Y .\/ ( ( s .\/ S ) ./\ W ) ) ) ) |
7 |
|
oveq1 |
|- ( t = S -> ( t .\/ U ) = ( S .\/ U ) ) |
8 |
|
oveq2 |
|- ( t = S -> ( P .\/ t ) = ( P .\/ S ) ) |
9 |
8
|
oveq1d |
|- ( t = S -> ( ( P .\/ t ) ./\ W ) = ( ( P .\/ S ) ./\ W ) ) |
10 |
9
|
oveq2d |
|- ( t = S -> ( Q .\/ ( ( P .\/ t ) ./\ W ) ) = ( Q .\/ ( ( P .\/ S ) ./\ W ) ) ) |
11 |
7 10
|
oveq12d |
|- ( t = S -> ( ( t .\/ U ) ./\ ( Q .\/ ( ( P .\/ t ) ./\ W ) ) ) = ( ( S .\/ U ) ./\ ( Q .\/ ( ( P .\/ S ) ./\ W ) ) ) ) |
12 |
11 1 3
|
3eqtr4g |
|- ( t = S -> D = Y ) |
13 |
|
oveq2 |
|- ( t = S -> ( s .\/ t ) = ( s .\/ S ) ) |
14 |
13
|
oveq1d |
|- ( t = S -> ( ( s .\/ t ) ./\ W ) = ( ( s .\/ S ) ./\ W ) ) |
15 |
12 14
|
oveq12d |
|- ( t = S -> ( D .\/ ( ( s .\/ t ) ./\ W ) ) = ( Y .\/ ( ( s .\/ S ) ./\ W ) ) ) |
16 |
15
|
oveq2d |
|- ( t = S -> ( ( P .\/ Q ) ./\ ( D .\/ ( ( s .\/ t ) ./\ W ) ) ) = ( ( P .\/ Q ) ./\ ( Y .\/ ( ( s .\/ S ) ./\ W ) ) ) ) |
17 |
6 16
|
csbiegf |
|- ( S e. A -> [_ S / t ]_ ( ( P .\/ Q ) ./\ ( D .\/ ( ( s .\/ t ) ./\ W ) ) ) = ( ( P .\/ Q ) ./\ ( Y .\/ ( ( s .\/ S ) ./\ W ) ) ) ) |
18 |
5 17
|
syl5eq |
|- ( S e. A -> [_ S / t ]_ E = ( ( P .\/ Q ) ./\ ( Y .\/ ( ( s .\/ S ) ./\ W ) ) ) ) |
19 |
18
|
csbeq2dv |
|- ( S e. A -> [_ R / s ]_ [_ S / t ]_ E = [_ R / s ]_ ( ( P .\/ Q ) ./\ ( Y .\/ ( ( s .\/ S ) ./\ W ) ) ) ) |
20 |
|
eqid |
|- ( ( P .\/ Q ) ./\ ( Y .\/ ( ( s .\/ S ) ./\ W ) ) ) = ( ( P .\/ Q ) ./\ ( Y .\/ ( ( s .\/ S ) ./\ W ) ) ) |
21 |
20 4
|
cdleme31se |
|- ( R e. A -> [_ R / s ]_ ( ( P .\/ Q ) ./\ ( Y .\/ ( ( s .\/ S ) ./\ W ) ) ) = Z ) |
22 |
19 21
|
sylan9eqr |
|- ( ( R e. A /\ S e. A ) -> [_ R / s ]_ [_ S / t ]_ E = Z ) |