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 𝐷 = ( ( 𝑡 𝑈 ) ( 𝑄 ( ( 𝑃 𝑡 ) 𝑊 ) ) )
cdleme31sde.e 𝐸 = ( ( 𝑃 𝑄 ) ( 𝐷 ( ( 𝑠 𝑡 ) 𝑊 ) ) )
cdleme31sde.x 𝑌 = ( ( 𝑆 𝑈 ) ( 𝑄 ( ( 𝑃 𝑆 ) 𝑊 ) ) )
cdleme31sde.z 𝑍 = ( ( 𝑃 𝑄 ) ( 𝑌 ( ( 𝑅 𝑆 ) 𝑊 ) ) )
Assertion cdleme31sde ( ( 𝑅𝐴𝑆𝐴 ) → 𝑅 / 𝑠 𝑆 / 𝑡 𝐸 = 𝑍 )

Proof

Step Hyp Ref Expression
1 cdleme31sde.c 𝐷 = ( ( 𝑡 𝑈 ) ( 𝑄 ( ( 𝑃 𝑡 ) 𝑊 ) ) )
2 cdleme31sde.e 𝐸 = ( ( 𝑃 𝑄 ) ( 𝐷 ( ( 𝑠 𝑡 ) 𝑊 ) ) )
3 cdleme31sde.x 𝑌 = ( ( 𝑆 𝑈 ) ( 𝑄 ( ( 𝑃 𝑆 ) 𝑊 ) ) )
4 cdleme31sde.z 𝑍 = ( ( 𝑃 𝑄 ) ( 𝑌 ( ( 𝑅 𝑆 ) 𝑊 ) ) )
5 2 csbeq2i 𝑆 / 𝑡 𝐸 = 𝑆 / 𝑡 ( ( 𝑃 𝑄 ) ( 𝐷 ( ( 𝑠 𝑡 ) 𝑊 ) ) )
6 nfcvd ( 𝑆𝐴 𝑡 ( ( 𝑃 𝑄 ) ( 𝑌 ( ( 𝑠 𝑆 ) 𝑊 ) ) ) )
7 oveq1 ( 𝑡 = 𝑆 → ( 𝑡 𝑈 ) = ( 𝑆 𝑈 ) )
8 oveq2 ( 𝑡 = 𝑆 → ( 𝑃 𝑡 ) = ( 𝑃 𝑆 ) )
9 8 oveq1d ( 𝑡 = 𝑆 → ( ( 𝑃 𝑡 ) 𝑊 ) = ( ( 𝑃 𝑆 ) 𝑊 ) )
10 9 oveq2d ( 𝑡 = 𝑆 → ( 𝑄 ( ( 𝑃 𝑡 ) 𝑊 ) ) = ( 𝑄 ( ( 𝑃 𝑆 ) 𝑊 ) ) )
11 7 10 oveq12d ( 𝑡 = 𝑆 → ( ( 𝑡 𝑈 ) ( 𝑄 ( ( 𝑃 𝑡 ) 𝑊 ) ) ) = ( ( 𝑆 𝑈 ) ( 𝑄 ( ( 𝑃 𝑆 ) 𝑊 ) ) ) )
12 11 1 3 3eqtr4g ( 𝑡 = 𝑆𝐷 = 𝑌 )
13 oveq2 ( 𝑡 = 𝑆 → ( 𝑠 𝑡 ) = ( 𝑠 𝑆 ) )
14 13 oveq1d ( 𝑡 = 𝑆 → ( ( 𝑠 𝑡 ) 𝑊 ) = ( ( 𝑠 𝑆 ) 𝑊 ) )
15 12 14 oveq12d ( 𝑡 = 𝑆 → ( 𝐷 ( ( 𝑠 𝑡 ) 𝑊 ) ) = ( 𝑌 ( ( 𝑠 𝑆 ) 𝑊 ) ) )
16 15 oveq2d ( 𝑡 = 𝑆 → ( ( 𝑃 𝑄 ) ( 𝐷 ( ( 𝑠 𝑡 ) 𝑊 ) ) ) = ( ( 𝑃 𝑄 ) ( 𝑌 ( ( 𝑠 𝑆 ) 𝑊 ) ) ) )
17 6 16 csbiegf ( 𝑆𝐴 𝑆 / 𝑡 ( ( 𝑃 𝑄 ) ( 𝐷 ( ( 𝑠 𝑡 ) 𝑊 ) ) ) = ( ( 𝑃 𝑄 ) ( 𝑌 ( ( 𝑠 𝑆 ) 𝑊 ) ) ) )
18 5 17 eqtrid ( 𝑆𝐴 𝑆 / 𝑡 𝐸 = ( ( 𝑃 𝑄 ) ( 𝑌 ( ( 𝑠 𝑆 ) 𝑊 ) ) ) )
19 18 csbeq2dv ( 𝑆𝐴 𝑅 / 𝑠 𝑆 / 𝑡 𝐸 = 𝑅 / 𝑠 ( ( 𝑃 𝑄 ) ( 𝑌 ( ( 𝑠 𝑆 ) 𝑊 ) ) ) )
20 eqid ( ( 𝑃 𝑄 ) ( 𝑌 ( ( 𝑠 𝑆 ) 𝑊 ) ) ) = ( ( 𝑃 𝑄 ) ( 𝑌 ( ( 𝑠 𝑆 ) 𝑊 ) ) )
21 20 4 cdleme31se ( 𝑅𝐴 𝑅 / 𝑠 ( ( 𝑃 𝑄 ) ( 𝑌 ( ( 𝑠 𝑆 ) 𝑊 ) ) ) = 𝑍 )
22 19 21 sylan9eqr ( ( 𝑅𝐴𝑆𝐴 ) → 𝑅 / 𝑠 𝑆 / 𝑡 𝐸 = 𝑍 )