Metamath Proof Explorer


Theorem cdleme31sn2

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

Ref Expression
Hypotheses cdleme32sn2.d 𝐷 = ( ( 𝑠 𝑈 ) ( 𝑄 ( ( 𝑃 𝑠 ) 𝑊 ) ) )
cdleme31sn2.n 𝑁 = if ( 𝑠 ( 𝑃 𝑄 ) , 𝐼 , 𝐷 )
cdleme31sn2.c 𝐶 = ( ( 𝑅 𝑈 ) ( 𝑄 ( ( 𝑃 𝑅 ) 𝑊 ) ) )
Assertion cdleme31sn2 ( ( 𝑅𝐴 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) → 𝑅 / 𝑠 𝑁 = 𝐶 )

Proof

Step Hyp Ref Expression
1 cdleme32sn2.d 𝐷 = ( ( 𝑠 𝑈 ) ( 𝑄 ( ( 𝑃 𝑠 ) 𝑊 ) ) )
2 cdleme31sn2.n 𝑁 = if ( 𝑠 ( 𝑃 𝑄 ) , 𝐼 , 𝐷 )
3 cdleme31sn2.c 𝐶 = ( ( 𝑅 𝑈 ) ( 𝑄 ( ( 𝑃 𝑅 ) 𝑊 ) ) )
4 eqid if ( 𝑅 ( 𝑃 𝑄 ) , 𝑅 / 𝑠 𝐼 , 𝑅 / 𝑠 𝐷 ) = if ( 𝑅 ( 𝑃 𝑄 ) , 𝑅 / 𝑠 𝐼 , 𝑅 / 𝑠 𝐷 )
5 2 4 cdleme31sn ( 𝑅𝐴 𝑅 / 𝑠 𝑁 = if ( 𝑅 ( 𝑃 𝑄 ) , 𝑅 / 𝑠 𝐼 , 𝑅 / 𝑠 𝐷 ) )
6 5 adantr ( ( 𝑅𝐴 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) → 𝑅 / 𝑠 𝑁 = if ( 𝑅 ( 𝑃 𝑄 ) , 𝑅 / 𝑠 𝐼 , 𝑅 / 𝑠 𝐷 ) )
7 iffalse ( ¬ 𝑅 ( 𝑃 𝑄 ) → if ( 𝑅 ( 𝑃 𝑄 ) , 𝑅 / 𝑠 𝐼 , 𝑅 / 𝑠 𝐷 ) = 𝑅 / 𝑠 𝐷 )
8 1 csbeq2i 𝑅 / 𝑠 𝐷 = 𝑅 / 𝑠 ( ( 𝑠 𝑈 ) ( 𝑄 ( ( 𝑃 𝑠 ) 𝑊 ) ) )
9 7 8 eqtrdi ( ¬ 𝑅 ( 𝑃 𝑄 ) → if ( 𝑅 ( 𝑃 𝑄 ) , 𝑅 / 𝑠 𝐼 , 𝑅 / 𝑠 𝐷 ) = 𝑅 / 𝑠 ( ( 𝑠 𝑈 ) ( 𝑄 ( ( 𝑃 𝑠 ) 𝑊 ) ) ) )
10 nfcvd ( 𝑅𝐴 𝑠 ( ( 𝑅 𝑈 ) ( 𝑄 ( ( 𝑃 𝑅 ) 𝑊 ) ) ) )
11 oveq1 ( 𝑠 = 𝑅 → ( 𝑠 𝑈 ) = ( 𝑅 𝑈 ) )
12 oveq2 ( 𝑠 = 𝑅 → ( 𝑃 𝑠 ) = ( 𝑃 𝑅 ) )
13 12 oveq1d ( 𝑠 = 𝑅 → ( ( 𝑃 𝑠 ) 𝑊 ) = ( ( 𝑃 𝑅 ) 𝑊 ) )
14 13 oveq2d ( 𝑠 = 𝑅 → ( 𝑄 ( ( 𝑃 𝑠 ) 𝑊 ) ) = ( 𝑄 ( ( 𝑃 𝑅 ) 𝑊 ) ) )
15 11 14 oveq12d ( 𝑠 = 𝑅 → ( ( 𝑠 𝑈 ) ( 𝑄 ( ( 𝑃 𝑠 ) 𝑊 ) ) ) = ( ( 𝑅 𝑈 ) ( 𝑄 ( ( 𝑃 𝑅 ) 𝑊 ) ) ) )
16 10 15 csbiegf ( 𝑅𝐴 𝑅 / 𝑠 ( ( 𝑠 𝑈 ) ( 𝑄 ( ( 𝑃 𝑠 ) 𝑊 ) ) ) = ( ( 𝑅 𝑈 ) ( 𝑄 ( ( 𝑃 𝑅 ) 𝑊 ) ) ) )
17 9 16 sylan9eqr ( ( 𝑅𝐴 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) → if ( 𝑅 ( 𝑃 𝑄 ) , 𝑅 / 𝑠 𝐼 , 𝑅 / 𝑠 𝐷 ) = ( ( 𝑅 𝑈 ) ( 𝑄 ( ( 𝑃 𝑅 ) 𝑊 ) ) ) )
18 6 17 eqtrd ( ( 𝑅𝐴 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) → 𝑅 / 𝑠 𝑁 = ( ( 𝑅 𝑈 ) ( 𝑄 ( ( 𝑃 𝑅 ) 𝑊 ) ) ) )
19 18 3 eqtr4di ( ( 𝑅𝐴 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) → 𝑅 / 𝑠 𝑁 = 𝐶 )