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=\left(P\underset{\dot{}}{\vee }R\left(g\right)\right)\underset{\dot{}}{\wedge }\left(Z\underset{\dot{}}{\vee }R\left(g\circ b^{-1}\right)\right)$$
Assertion	cdlemk41	$$⊢G\in T\to ⦋G/g⦌Y=\left(P\underset{\dot{}}{\vee }R\left(G\right)\right)\underset{\dot{}}{\wedge }\left(Z\underset{\dot{}}{\vee }R\left(G\circ b^{-1}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		cdlemk41.y	$$⊢Y=\left(P\underset{\dot{}}{\vee }R\left(g\right)\right)\underset{\dot{}}{\wedge }\left(Z\underset{\dot{}}{\vee }R\left(g\circ b^{-1}\right)\right)$$
2		nfcvd	$$⊢G\in T\to \underset{\_}{Ⅎ}g\left(\left(P\underset{\dot{}}{\vee }R\left(G\right)\right)\underset{\dot{}}{\wedge }\left(Z\underset{\dot{}}{\vee }R\left(G\circ b^{-1}\right)\right)\right)$$
3		fveq2	$$⊢g=G\to R\left(g\right)=R\left(G\right)$$
4	3	oveq2d	$$⊢g=G\to P\underset{\dot{}}{\vee }R\left(g\right)=P\underset{\dot{}}{\vee }R\left(G\right)$$
5		coeq1	$$⊢g=G\to g\circ b^{-1}=G\circ b^{-1}$$
6	5	fveq2d	$$⊢g=G\to R\left(g\circ b^{-1}\right)=R\left(G\circ b^{-1}\right)$$
7	6	oveq2d	$$⊢g=G\to Z\underset{\dot{}}{\vee }R\left(g\circ b^{-1}\right)=Z\underset{\dot{}}{\vee }R\left(G\circ b^{-1}\right)$$
8	4 7	oveq12d	$$⊢g=G\to \left(P\underset{\dot{}}{\vee }R\left(g\right)\right)\underset{\dot{}}{\wedge }\left(Z\underset{\dot{}}{\vee }R\left(g\circ b^{-1}\right)\right)=\left(P\underset{\dot{}}{\vee }R\left(G\right)\right)\underset{\dot{}}{\wedge }\left(Z\underset{\dot{}}{\vee }R\left(G\circ b^{-1}\right)\right)$$
9	1 8	syl5eq	$$⊢g=G\to Y=\left(P\underset{\dot{}}{\vee }R\left(G\right)\right)\underset{\dot{}}{\wedge }\left(Z\underset{\dot{}}{\vee }R\left(G\circ b^{-1}\right)\right)$$
10	2 9	csbiegf	$$⊢G\in T\to ⦋G/g⦌Y=\left(P\underset{\dot{}}{\vee }R\left(G\right)\right)\underset{\dot{}}{\wedge }\left(Z\underset{\dot{}}{\vee }R\left(G\circ b^{-1}\right)\right)$$