Metamath Proof Explorer

Theorem cdleme31sc

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

Ref Expression
Hypotheses cdleme31sc.c 
|- C = ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) )
cdleme31sc.x 
|- X = ( ( R .\/ U ) ./\ ( Q .\/ ( ( P .\/ R ) ./\ W ) ) )
Assertion cdleme31sc 
|- ( R e. A -> [_ R / s ]_ C = X )

Proof

Step Hyp Ref Expression
1 cdleme31sc.c 
 |-  C = ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) )
2 cdleme31sc.x 
 |-  X = ( ( R .\/ U ) ./\ ( Q .\/ ( ( P .\/ R ) ./\ W ) ) )
3 nfcvd 
 |-  ( R e. A -> F/_ s ( ( R .\/ U ) ./\ ( Q .\/ ( ( P .\/ R ) ./\ W ) ) ) )
4 oveq1 
 |-  ( s = R -> ( s .\/ U ) = ( R .\/ U ) )
5 oveq2 
 |-  ( s = R -> ( P .\/ s ) = ( P .\/ R ) )
6 5 oveq1d 
 |-  ( s = R -> ( ( P .\/ s ) ./\ W ) = ( ( P .\/ R ) ./\ W ) )
7 6 oveq2d 
 |-  ( s = R -> ( Q .\/ ( ( P .\/ s ) ./\ W ) ) = ( Q .\/ ( ( P .\/ R ) ./\ W ) ) )
8 4 7 oveq12d 
 |-  ( s = R -> ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) ) = ( ( R .\/ U ) ./\ ( Q .\/ ( ( P .\/ R ) ./\ W ) ) ) )
9 3 8 csbiegf 
 |-  ( R e. A -> [_ R / s ]_ ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) ) = ( ( R .\/ U ) ./\ ( Q .\/ ( ( P .\/ R ) ./\ W ) ) ) )
10 1 csbeq2i 
 |-  [_ R / s ]_ C = [_ R / s ]_ ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) )
11 9 10 2 3eqtr4g 
 |-  ( R e. A -> [_ R / s ]_ C = X )