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 )