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

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 eqtrid 
 |-  ( 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 ) ) ) ) )