Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cdleme31sc Unicode version

Theorem cdleme31sc 29262
Description: Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 31-Mar-2013.)
Hypotheses
Ref Expression
cdleme31sc.c  |-  C  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W
) ) )
cdleme31sc.x  |-  X  =  ( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
) )
Assertion
Ref Expression
cdleme31sc  |-  ( R  e.  A  ->  [_ R  /  s ]_ C  =  X )
Distinct variable groups:    A, s    .\/ , s    ./\ , s    P, s    Q, s    R, s    U, s    W, s
Allowed substitution hints:    C( s)    X( s)

Proof of Theorem cdleme31sc
StepHypRef Expression
1 nfcvd 2386 . . 3  |-  ( R  e.  A  ->  F/_ s
( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
) ) )
2 oveq1 5717 . . . 4  |-  ( s  =  R  ->  (
s  .\/  U )  =  ( R  .\/  U ) )
3 oveq2 5718 . . . . . 6  |-  ( s  =  R  ->  ( P  .\/  s )  =  ( P  .\/  R
) )
43oveq1d 5725 . . . . 5  |-  ( s  =  R  ->  (
( P  .\/  s
)  ./\  W )  =  ( ( P 
.\/  R )  ./\  W ) )
54oveq2d 5726 . . . 4  |-  ( s  =  R  ->  ( Q  .\/  ( ( P 
.\/  s )  ./\  W ) )  =  ( Q  .\/  ( ( P  .\/  R ) 
./\  W ) ) )
62, 5oveq12d 5728 . . 3  |-  ( s  =  R  ->  (
( s  .\/  U
)  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W
) ) )  =  ( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
) ) )
71, 6csbiegf 3049 . 2  |-  ( R  e.  A  ->  [_ R  /  s ]_ (
( s  .\/  U
)  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W
) ) )  =  ( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
) ) )
8 cdleme31sc.c . . 3  |-  C  =  ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W
) ) )
98csbeq2i 3035 . 2  |-  [_ R  /  s ]_ C  =  [_ R  /  s ]_ ( ( s  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W
) ) )
10 cdleme31sc.x . 2  |-  X  =  ( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
) )
117, 9, 103eqtr4g 2310 1  |-  ( R  e.  A  ->  [_ R  /  s ]_ C  =  X )
Colors of variables: wff set class
Syntax hints:    -> wi 6    = wceq 1619    e. wcel 1621   [_csb 3009  (class class class)co 5710
This theorem is referenced by:  cdleme31snd  29264  cdleme31sdnN  29265  cdlemefr44  29303  cdlemefr45e  29306  cdleme48fv  29377  cdleme46fvaw  29379  cdleme48bw  29380  cdleme46fsvlpq  29383  cdlemeg46fvcl  29384  cdlemeg49le  29389  cdlemeg46fjgN  29399  cdlemeg46rjgN  29400  cdlemeg46fjv  29401  cdleme48d  29413  cdlemeg49lebilem  29417  cdleme50eq  29419  cdleme50f  29420  cdlemg2jlemOLDN  29471  cdlemg2klem  29473
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-rex 2514  df-rab 2516  df-v 2729  df-sbc 2922  df-csb 3010  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-nul 3363  df-if 3471  df-sn 3550  df-pr 3551  df-op 3553  df-uni 3728  df-br 3921  df-opab 3975  df-xp 4594  df-cnv 4596  df-dm 4598  df-rn 4599  df-res 4600  df-ima 4601  df-fv 4608  df-ov 5713
  Copyright terms: Public domain W3C validator