Metamath Proof Explorer

Theorem cdleme31sn1

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

Ref Expression
Hypotheses cdleme31sn1.i 
|- I = ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = G ) )
cdleme31sn1.n 
|- N = if ( s .<_ ( P .\/ Q ) , I , D )
cdleme31sn1.c 
|- C = ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = [_ R / s ]_ G ) )
Assertion cdleme31sn1 
|- ( ( R e. A /\ R .<_ ( P .\/ Q ) ) -> [_ R / s ]_ N = C )

Proof

Step Hyp Ref Expression
1 cdleme31sn1.i 
 |-  I = ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = G ) )
2 cdleme31sn1.n 
 |-  N = if ( s .<_ ( P .\/ Q ) , I , D )
3 cdleme31sn1.c 
 |-  C = ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = [_ R / s ]_ G ) )
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 iftrue 
 |-  ( R .<_ ( P .\/ Q ) -> if ( R .<_ ( P .\/ Q ) , [_ R / s ]_ I , [_ R / s ]_ D ) = [_ R / s ]_ I )
8 1 csbeq2i 
 |-  [_ R / s ]_ I = [_ R / s ]_ ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = G ) )
9 7 8 eqtrdi 
 |-  ( R .<_ ( P .\/ Q ) -> if ( R .<_ ( P .\/ Q ) , [_ R / s ]_ I , [_ R / s ]_ D ) = [_ R / s ]_ ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = G ) ) )
10 nfcv 
 |-  F/_ s A
11 nfv 
 |-  F/ s ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) )
12 nfcsb1v 
 |-  F/_ s [_ R / s ]_ G
13 12 nfeq2 
 |-  F/ s y = [_ R / s ]_ G
14 11 13 nfim 
 |-  F/ s ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = [_ R / s ]_ G )
15 10 14 nfralw 
 |-  F/ s A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = [_ R / s ]_ G )
16 nfcv 
 |-  F/_ s B
17 15 16 nfriota 
 |-  F/_ s ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = [_ R / s ]_ G ) )
18 17 a1i 
 |-  ( R e. A -> F/_ s ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = [_ R / s ]_ G ) ) )
19 csbeq1a 
 |-  ( s = R -> G = [_ R / s ]_ G )
20 19 eqeq2d 
 |-  ( s = R -> ( y = G <-> y = [_ R / s ]_ G ) )
21 20 imbi2d 
 |-  ( s = R -> ( ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = G ) <-> ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = [_ R / s ]_ G ) ) )
22 21 ralbidv 
 |-  ( s = R -> ( A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = G ) <-> A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = [_ R / s ]_ G ) ) )
23 22 riotabidv 
 |-  ( s = R -> ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = G ) ) = ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = [_ R / s ]_ G ) ) )
24 18 23 csbiegf 
 |-  ( R e. A -> [_ R / s ]_ ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = G ) ) = ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = [_ R / s ]_ G ) ) )
25 9 24 sylan9eqr 
 |-  ( ( R e. A /\ R .<_ ( P .\/ Q ) ) -> if ( R .<_ ( P .\/ Q ) , [_ R / s ]_ I , [_ R / s ]_ D ) = ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = [_ R / s ]_ G ) ) )
26 25 3 eqtr4di 
 |-  ( ( R e. A /\ R .<_ ( P .\/ Q ) ) -> if ( R .<_ ( P .\/ Q ) , [_ R / s ]_ I , [_ R / s ]_ D ) = C )
27 6 26 eqtrd 
 |-  ( ( R e. A /\ R .<_ ( P .\/ Q ) ) -> [_ R / s ]_ N = C )