Metamath Proof Explorer


Theorem cdleme31se

Description: Part of proof of Lemma D in Crawley p. 113. (Contributed by NM, 26-Feb-2013)

Ref Expression
Hypotheses cdleme31se.e E = P ˙ Q ˙ D ˙ s ˙ T ˙ W
cdleme31se.y Y = P ˙ Q ˙ D ˙ R ˙ T ˙ W
Assertion cdleme31se R A R / s E = Y

Proof

Step Hyp Ref Expression
1 cdleme31se.e E = P ˙ Q ˙ D ˙ s ˙ T ˙ W
2 cdleme31se.y Y = P ˙ Q ˙ D ˙ R ˙ T ˙ W
3 nfcvd R A _ s P ˙ Q ˙ D ˙ R ˙ T ˙ W
4 oveq1 s = R s ˙ T = R ˙ T
5 4 oveq1d s = R s ˙ T ˙ W = R ˙ T ˙ W
6 5 oveq2d s = R D ˙ s ˙ T ˙ W = D ˙ R ˙ T ˙ W
7 6 oveq2d s = R P ˙ Q ˙ D ˙ s ˙ T ˙ W = P ˙ Q ˙ D ˙ R ˙ T ˙ W
8 3 7 csbiegf R A R / s P ˙ Q ˙ D ˙ s ˙ T ˙ W = P ˙ Q ˙ D ˙ R ˙ T ˙ W
9 1 csbeq2i R / s E = R / s P ˙ Q ˙ D ˙ s ˙ T ˙ W
10 8 9 2 3eqtr4g R A R / s E = Y