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 )