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

Metamath Proof Explorer

Theorem cdleme31se2

Description: Part of proof of Lemma D in Crawley p. 113. (Contributed by NM, 3-Apr-2013)

Ref Expression
Hypotheses cdleme31se2.e 
|- E = ( ( P .\/ Q ) ./\ ( D .\/ ( ( R .\/ t ) ./\ W ) ) )
cdleme31se2.y 
|- Y = ( ( P .\/ Q ) ./\ ( [_ S / t ]_ D .\/ ( ( R .\/ S ) ./\ W ) ) )
Assertion cdleme31se2 
|- ( S e. A -> [_ S / t ]_ E = Y )

Proof

Step Hyp Ref Expression
1 cdleme31se2.e 
 |-  E = ( ( P .\/ Q ) ./\ ( D .\/ ( ( R .\/ t ) ./\ W ) ) )
2 cdleme31se2.y 
 |-  Y = ( ( P .\/ Q ) ./\ ( [_ S / t ]_ D .\/ ( ( R .\/ S ) ./\ W ) ) )
3 nfcv 
 |-  F/_ t ( P .\/ Q )
4 nfcv 
 |-  F/_ t ./\
5 nfcsb1v 
 |-  F/_ t [_ S / t ]_ D
6 nfcv 
 |-  F/_ t .\/
7 nfcv 
 |-  F/_ t ( ( R .\/ S ) ./\ W )
8 5 6 7 nfov 
 |-  F/_ t ( [_ S / t ]_ D .\/ ( ( R .\/ S ) ./\ W ) )
9 3 4 8 nfov 
 |-  F/_ t ( ( P .\/ Q ) ./\ ( [_ S / t ]_ D .\/ ( ( R .\/ S ) ./\ W ) ) )
10 9 a1i 
 |-  ( S e. A -> F/_ t ( ( P .\/ Q ) ./\ ( [_ S / t ]_ D .\/ ( ( R .\/ S ) ./\ W ) ) ) )
11 csbeq1a 
 |-  ( t = S -> D = [_ S / t ]_ D )
12 oveq2 
 |-  ( t = S -> ( R .\/ t ) = ( R .\/ S ) )
13 12 oveq1d 
 |-  ( t = S -> ( ( R .\/ t ) ./\ W ) = ( ( R .\/ S ) ./\ W ) )
14 11 13 oveq12d 
 |-  ( t = S -> ( D .\/ ( ( R .\/ t ) ./\ W ) ) = ( [_ S / t ]_ D .\/ ( ( R .\/ S ) ./\ W ) ) )
15 14 oveq2d 
 |-  ( t = S -> ( ( P .\/ Q ) ./\ ( D .\/ ( ( R .\/ t ) ./\ W ) ) ) = ( ( P .\/ Q ) ./\ ( [_ S / t ]_ D .\/ ( ( R .\/ S ) ./\ W ) ) ) )
16 10 15 csbiegf 
 |-  ( S e. A -> [_ S / t ]_ ( ( P .\/ Q ) ./\ ( D .\/ ( ( R .\/ t ) ./\ W ) ) ) = ( ( P .\/ Q ) ./\ ( [_ S / t ]_ D .\/ ( ( R .\/ S ) ./\ W ) ) ) )
17 1 csbeq2i 
 |-  [_ S / t ]_ E = [_ S / t ]_ ( ( P .\/ Q ) ./\ ( D .\/ ( ( R .\/ t ) ./\ W ) ) )
18 16 17 2 3eqtr4g 
 |-  ( S e. A -> [_ S / t ]_ E = Y )