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 D = s ˙ U ˙ Q ˙ P ˙ s ˙ W
cdleme31sn2.n N = if s ˙ P ˙ Q I D
cdleme31sn2.c C = R ˙ U ˙ Q ˙ P ˙ R ˙ W
Assertion cdleme31sn2 R A ¬ R ˙ P ˙ Q R / s N = C

Proof

Step Hyp Ref Expression
1 cdleme32sn2.d D = s ˙ U ˙ Q ˙ P ˙ s ˙ W
2 cdleme31sn2.n N = if s ˙ P ˙ Q I D
3 cdleme31sn2.c C = R ˙ U ˙ Q ˙ P ˙ R ˙ W
4 eqid if R ˙ P ˙ Q R / s I R / s D = if R ˙ P ˙ Q R / s I R / s D
5 2 4 cdleme31sn R A R / s N = if R ˙ P ˙ Q R / s I R / s D
6 5 adantr R A ¬ R ˙ P ˙ Q R / s N = if R ˙ P ˙ Q R / s I R / s D
7 iffalse ¬ R ˙ P ˙ Q if R ˙ P ˙ Q R / s I R / s D = R / s D
8 1 csbeq2i R / s D = R / s s ˙ U ˙ Q ˙ P ˙ s ˙ W
9 7 8 eqtrdi ¬ R ˙ P ˙ Q if R ˙ P ˙ Q R / s I R / s D = R / s s ˙ U ˙ Q ˙ P ˙ s ˙ W
10 nfcvd R A _ s R ˙ U ˙ Q ˙ P ˙ R ˙ W
11 oveq1 s = R s ˙ U = R ˙ U
12 oveq2 s = R P ˙ s = P ˙ R
13 12 oveq1d s = R P ˙ s ˙ W = P ˙ R ˙ W
14 13 oveq2d s = R Q ˙ P ˙ s ˙ W = Q ˙ P ˙ R ˙ W
15 11 14 oveq12d s = R s ˙ U ˙ Q ˙ P ˙ s ˙ W = R ˙ U ˙ Q ˙ P ˙ R ˙ W
16 10 15 csbiegf R A R / s s ˙ U ˙ Q ˙ P ˙ s ˙ W = R ˙ U ˙ Q ˙ P ˙ R ˙ W
17 9 16 sylan9eqr R A ¬ R ˙ P ˙ Q if R ˙ P ˙ Q R / s I R / s D = R ˙ U ˙ Q ˙ P ˙ R ˙ W
18 6 17 eqtrd R A ¬ R ˙ P ˙ Q R / s N = R ˙ U ˙ Q ˙ P ˙ R ˙ W
19 18 3 eqtr4di R A ¬ R ˙ P ˙ Q R / s N = C