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 )