Metamath Proof Explorer


Theorem cdleme31sde

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

Ref Expression
Hypotheses cdleme31sde.c D=t˙U˙Q˙P˙t˙W
cdleme31sde.e E=P˙Q˙D˙s˙t˙W
cdleme31sde.x Y=S˙U˙Q˙P˙S˙W
cdleme31sde.z Z=P˙Q˙Y˙R˙S˙W
Assertion cdleme31sde RASAR/sS/tE=Z

Proof

Step Hyp Ref Expression
1 cdleme31sde.c D=t˙U˙Q˙P˙t˙W
2 cdleme31sde.e E=P˙Q˙D˙s˙t˙W
3 cdleme31sde.x Y=S˙U˙Q˙P˙S˙W
4 cdleme31sde.z Z=P˙Q˙Y˙R˙S˙W
5 2 csbeq2i S/tE=S/tP˙Q˙D˙s˙t˙W
6 nfcvd SA_tP˙Q˙Y˙s˙S˙W
7 oveq1 t=St˙U=S˙U
8 oveq2 t=SP˙t=P˙S
9 8 oveq1d t=SP˙t˙W=P˙S˙W
10 9 oveq2d t=SQ˙P˙t˙W=Q˙P˙S˙W
11 7 10 oveq12d t=St˙U˙Q˙P˙t˙W=S˙U˙Q˙P˙S˙W
12 11 1 3 3eqtr4g t=SD=Y
13 oveq2 t=Ss˙t=s˙S
14 13 oveq1d t=Ss˙t˙W=s˙S˙W
15 12 14 oveq12d t=SD˙s˙t˙W=Y˙s˙S˙W
16 15 oveq2d t=SP˙Q˙D˙s˙t˙W=P˙Q˙Y˙s˙S˙W
17 6 16 csbiegf SAS/tP˙Q˙D˙s˙t˙W=P˙Q˙Y˙s˙S˙W
18 5 17 eqtrid SAS/tE=P˙Q˙Y˙s˙S˙W
19 18 csbeq2dv SAR/sS/tE=R/sP˙Q˙Y˙s˙S˙W
20 eqid P˙Q˙Y˙s˙S˙W=P˙Q˙Y˙s˙S˙W
21 20 4 cdleme31se RAR/sP˙Q˙Y˙s˙S˙W=Z
22 19 21 sylan9eqr RASAR/sS/tE=Z