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 𝐸 = ( ( 𝑃 𝑄 ) ( 𝐷 ( ( 𝑠 𝑇 ) 𝑊 ) ) )
cdleme31se.y 𝑌 = ( ( 𝑃 𝑄 ) ( 𝐷 ( ( 𝑅 𝑇 ) 𝑊 ) ) )
Assertion cdleme31se ( 𝑅𝐴 𝑅 / 𝑠 𝐸 = 𝑌 )

Proof

Step Hyp Ref Expression
1 cdleme31se.e 𝐸 = ( ( 𝑃 𝑄 ) ( 𝐷 ( ( 𝑠 𝑇 ) 𝑊 ) ) )
2 cdleme31se.y 𝑌 = ( ( 𝑃 𝑄 ) ( 𝐷 ( ( 𝑅 𝑇 ) 𝑊 ) ) )
3 nfcvd ( 𝑅𝐴 𝑠 ( ( 𝑃 𝑄 ) ( 𝐷 ( ( 𝑅 𝑇 ) 𝑊 ) ) ) )
4 oveq1 ( 𝑠 = 𝑅 → ( 𝑠 𝑇 ) = ( 𝑅 𝑇 ) )
5 4 oveq1d ( 𝑠 = 𝑅 → ( ( 𝑠 𝑇 ) 𝑊 ) = ( ( 𝑅 𝑇 ) 𝑊 ) )
6 5 oveq2d ( 𝑠 = 𝑅 → ( 𝐷 ( ( 𝑠 𝑇 ) 𝑊 ) ) = ( 𝐷 ( ( 𝑅 𝑇 ) 𝑊 ) ) )
7 6 oveq2d ( 𝑠 = 𝑅 → ( ( 𝑃 𝑄 ) ( 𝐷 ( ( 𝑠 𝑇 ) 𝑊 ) ) ) = ( ( 𝑃 𝑄 ) ( 𝐷 ( ( 𝑅 𝑇 ) 𝑊 ) ) ) )
8 3 7 csbiegf ( 𝑅𝐴 𝑅 / 𝑠 ( ( 𝑃 𝑄 ) ( 𝐷 ( ( 𝑠 𝑇 ) 𝑊 ) ) ) = ( ( 𝑃 𝑄 ) ( 𝐷 ( ( 𝑅 𝑇 ) 𝑊 ) ) ) )
9 1 csbeq2i 𝑅 / 𝑠 𝐸 = 𝑅 / 𝑠 ( ( 𝑃 𝑄 ) ( 𝐷 ( ( 𝑠 𝑇 ) 𝑊 ) ) )
10 8 9 2 3eqtr4g ( 𝑅𝐴 𝑅 / 𝑠 𝐸 = 𝑌 )