# Metamath Proof Explorer

## Theorem cdlemk41

Description: Part of proof of Lemma K of Crawley p. 118. TODO: fix comment. (Contributed by NM, 19-Jul-2013)

Ref Expression
Hypothesis cdlemk41.y
`|- Y = ( ( P .\/ ( R ` g ) ) ./\ ( Z .\/ ( R ` ( g o. `' b ) ) ) )`
Assertion cdlemk41
`|- ( G e. T -> [_ G / g ]_ Y = ( ( P .\/ ( R ` G ) ) ./\ ( Z .\/ ( R ` ( G o. `' b ) ) ) ) )`

### Proof

Step Hyp Ref Expression
1 cdlemk41.y
` |-  Y = ( ( P .\/ ( R ` g ) ) ./\ ( Z .\/ ( R ` ( g o. `' b ) ) ) )`
2 nfcvd
` |-  ( G e. T -> F/_ g ( ( P .\/ ( R ` G ) ) ./\ ( Z .\/ ( R ` ( G o. `' b ) ) ) ) )`
3 fveq2
` |-  ( g = G -> ( R ` g ) = ( R ` G ) )`
4 3 oveq2d
` |-  ( g = G -> ( P .\/ ( R ` g ) ) = ( P .\/ ( R ` G ) ) )`
5 coeq1
` |-  ( g = G -> ( g o. `' b ) = ( G o. `' b ) )`
6 5 fveq2d
` |-  ( g = G -> ( R ` ( g o. `' b ) ) = ( R ` ( G o. `' b ) ) )`
7 6 oveq2d
` |-  ( g = G -> ( Z .\/ ( R ` ( g o. `' b ) ) ) = ( Z .\/ ( R ` ( G o. `' b ) ) ) )`
8 4 7 oveq12d
` |-  ( g = G -> ( ( P .\/ ( R ` g ) ) ./\ ( Z .\/ ( R ` ( g o. `' b ) ) ) ) = ( ( P .\/ ( R ` G ) ) ./\ ( Z .\/ ( R ` ( G o. `' b ) ) ) ) )`
9 1 8 syl5eq
` |-  ( g = G -> Y = ( ( P .\/ ( R ` G ) ) ./\ ( Z .\/ ( R ` ( G o. `' b ) ) ) ) )`
10 2 9 csbiegf
` |-  ( G e. T -> [_ G / g ]_ Y = ( ( P .\/ ( R ` G ) ) ./\ ( Z .\/ ( R ` ( G o. `' b ) ) ) ) )`