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