This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cdleme31sn2

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

Ref Expression
Hypotheses cdleme32sn2.d 
|- D = ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) )
cdleme31sn2.n 
|- N = if ( s .<_ ( P .\/ Q ) , I , D )
cdleme31sn2.c 
|- C = ( ( R .\/ U ) ./\ ( Q .\/ ( ( P .\/ R ) ./\ W ) ) )
Assertion cdleme31sn2 
|- ( ( R e. A /\ -. R .<_ ( P .\/ Q ) ) -> [_ R / s ]_ N = C )

Proof

Step Hyp Ref Expression
1 cdleme32sn2.d 
 |-  D = ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) )
2 cdleme31sn2.n 
 |-  N = if ( s .<_ ( P .\/ Q ) , I , D )
3 cdleme31sn2.c 
 |-  C = ( ( R .\/ U ) ./\ ( Q .\/ ( ( P .\/ R ) ./\ W ) ) )
4 eqid 
 |-  if ( R .<_ ( P .\/ Q ) , [_ R / s ]_ I , [_ R / s ]_ D ) = if ( R .<_ ( P .\/ Q ) , [_ R / s ]_ I , [_ R / s ]_ D )
5 2 4 cdleme31sn 
 |-  ( R e. A -> [_ R / s ]_ N = if ( R .<_ ( P .\/ Q ) , [_ R / s ]_ I , [_ R / s ]_ D ) )
6 5 adantr 
 |-  ( ( R e. A /\ -. R .<_ ( P .\/ Q ) ) -> [_ R / s ]_ N = if ( R .<_ ( P .\/ Q ) , [_ R / s ]_ I , [_ R / s ]_ D ) )
7 iffalse 
 |-  ( -. R .<_ ( P .\/ Q ) -> if ( R .<_ ( P .\/ Q ) , [_ R / s ]_ I , [_ R / s ]_ D ) = [_ R / s ]_ D )
8 1 csbeq2i 
 |-  [_ R / s ]_ D = [_ R / s ]_ ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) )
9 7 8 eqtrdi 
 |-  ( -. R .<_ ( P .\/ Q ) -> if ( R .<_ ( P .\/ Q ) , [_ R / s ]_ I , [_ R / s ]_ D ) = [_ R / s ]_ ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) ) )
10 nfcvd 
 |-  ( R e. A -> F/_ s ( ( R .\/ U ) ./\ ( Q .\/ ( ( P .\/ R ) ./\ W ) ) ) )
11 oveq1 
 |-  ( s = R -> ( s .\/ U ) = ( R .\/ U ) )
12 oveq2 
 |-  ( s = R -> ( P .\/ s ) = ( P .\/ R ) )
13 12 oveq1d 
 |-  ( s = R -> ( ( P .\/ s ) ./\ W ) = ( ( P .\/ R ) ./\ W ) )
14 13 oveq2d 
 |-  ( s = R -> ( Q .\/ ( ( P .\/ s ) ./\ W ) ) = ( Q .\/ ( ( P .\/ R ) ./\ W ) ) )
15 11 14 oveq12d 
 |-  ( s = R -> ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) ) = ( ( R .\/ U ) ./\ ( Q .\/ ( ( P .\/ R ) ./\ W ) ) ) )
16 10 15 csbiegf 
 |-  ( R e. A -> [_ R / s ]_ ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) ) = ( ( R .\/ U ) ./\ ( Q .\/ ( ( P .\/ R ) ./\ W ) ) ) )
17 9 16 sylan9eqr 
 |-  ( ( R e. A /\ -. R .<_ ( P .\/ Q ) ) -> if ( R .<_ ( P .\/ Q ) , [_ R / s ]_ I , [_ R / s ]_ D ) = ( ( R .\/ U ) ./\ ( Q .\/ ( ( P .\/ R ) ./\ W ) ) ) )
18 6 17 eqtrd 
 |-  ( ( R e. A /\ -. R .<_ ( P .\/ Q ) ) -> [_ R / s ]_ N = ( ( R .\/ U ) ./\ ( Q .\/ ( ( P .\/ R ) ./\ W ) ) ) )
19 18 3 eqtr4di 
 |-  ( ( R e. A /\ -. R .<_ ( P .\/ Q ) ) -> [_ R / s ]_ N = C )