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

Theorem cdleme31sc 30573
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 2420 . . 3  |-  ( R  e.  A  ->  F/_ s
( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
) ) )
2 oveq1 5865 . . . 4  |-  ( s  =  R  ->  (
s  .\/  U )  =  ( R  .\/  U ) )
3 oveq2 5866 . . . . . 6  |-  ( s  =  R  ->  ( P  .\/  s )  =  ( P  .\/  R
) )
43oveq1d 5873 . . . . 5  |-  ( s  =  R  ->  (
( P  .\/  s
)  ./\  W )  =  ( ( P 
.\/  R )  ./\  W ) )
54oveq2d 5874 . . . 4  |-  ( s  =  R  ->  ( Q  .\/  ( ( P 
.\/  s )  ./\  W ) )  =  ( Q  .\/  ( ( P  .\/  R ) 
./\  W ) ) )
62, 5oveq12d 5876 . . 3  |-  ( s  =  R  ->  (
( s  .\/  U
)  ./\  ( Q  .\/  ( ( P  .\/  s )  ./\  W
) ) )  =  ( ( R  .\/  U )  ./\  ( Q  .\/  ( ( P  .\/  R )  ./\  W )
) ) )
71, 6csbiegf 3121 . 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 3107 . 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 2340 1  |-  ( R  e.  A  ->  [_ R  /  s ]_ C  =  X )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684   [_csb 3081  (class class class)co 5858
This theorem is referenced by:  cdleme31snd  30575  cdleme31sdnN  30576  cdlemefr44  30614  cdlemefr45e  30617  cdleme48fv  30688  cdleme46fvaw  30690  cdleme48bw  30691  cdleme46fsvlpq  30694  cdlemeg46fvcl  30695  cdlemeg49le  30700  cdlemeg46fjgN  30710  cdlemeg46rjgN  30711  cdlemeg46fjv  30712  cdleme48d  30724  cdlemeg49lebilem  30728  cdleme50eq  30730  cdleme50f  30731  cdlemg2jlemOLDN  30782  cdlemg2klem  30784
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861
  Copyright terms: Public domain W3C validator