Metamath Proof Explorer


Theorem cdleme31sde

Description: Part of proof of Lemma D in Crawley p. 113. (Contributed by NM, 31-Mar-2013)

Ref Expression
Hypotheses cdleme31sde.c
|- D = ( ( t .\/ U ) ./\ ( Q .\/ ( ( P .\/ t ) ./\ W ) ) )
cdleme31sde.e
|- E = ( ( P .\/ Q ) ./\ ( D .\/ ( ( s .\/ t ) ./\ W ) ) )
cdleme31sde.x
|- Y = ( ( S .\/ U ) ./\ ( Q .\/ ( ( P .\/ S ) ./\ W ) ) )
cdleme31sde.z
|- Z = ( ( P .\/ Q ) ./\ ( Y .\/ ( ( R .\/ S ) ./\ W ) ) )
Assertion cdleme31sde
|- ( ( R e. A /\ S e. A ) -> [_ R / s ]_ [_ S / t ]_ E = Z )

Proof

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 )