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

Theorem cdlemkuvN 34476
Description: Part of proof of Lemma K of [Crawley] p. 118. Value of the sigma1 (p) function  U. (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.)
Hypotheses
Ref Expression
cdlemk1.b  |-  B  =  ( Base `  K
)
cdlemk1.l  |-  .<_  =  ( le `  K )
cdlemk1.j  |-  .\/  =  ( join `  K )
cdlemk1.m  |-  ./\  =  ( meet `  K )
cdlemk1.a  |-  A  =  ( Atoms `  K )
cdlemk1.h  |-  H  =  ( LHyp `  K
)
cdlemk1.t  |-  T  =  ( ( LTrn `  K
) `  W )
cdlemk1.r  |-  R  =  ( ( trL `  K
) `  W )
cdlemk1.s  |-  S  =  ( f  e.  T  |->  ( iota_ i  e.  T  ( i `  P
)  =  ( ( P  .\/  ( R `
 f ) ) 
./\  ( ( N `
 P )  .\/  ( R `  ( f  o.  `' F ) ) ) ) ) )
cdlemk1.o  |-  O  =  ( S `  D
)
cdlemk1.u  |-  U  =  ( e  e.  T  |->  ( iota_ j  e.  T  ( j `  P
)  =  ( ( P  .\/  ( R `
 e ) ) 
./\  ( ( O `
 P )  .\/  ( R `  ( e  o.  `' D ) ) ) ) ) )
Assertion
Ref Expression
cdlemkuvN  |-  ( G  e.  T  ->  ( U `  G )  =  ( iota_ j  e.  T  ( j `  P )  =  ( ( P  .\/  ( R `  G )
)  ./\  ( ( O `  P )  .\/  ( R `  ( G  o.  `' D
) ) ) ) ) )
Distinct variable groups:    f, i,  ./\    .<_ , i    .\/ , f, i    A, i    D, f, i    f, F, i    i, H    i, K    f, N, i    P, f, i    R, f, i    T, f, i    f, W, i    ./\ , e    .\/ , e    D, e    e, j, G    e, O    P, e    R, e    T, e    e, W
Allowed substitution hints:    A( e, f, j)    B( e, f, i, j)    D( j)    P( j)    R( j)    S( e, f, i, j)    T( j)    U( e, f, i, j)    F( e, j)    G( f, i)    H( e, f, j)    .\/ ( j)    K( e, f, j)    .<_ ( e, f, j)    ./\ ( j)    N( e, j)    O( f, i, j)    W( j)

Proof of Theorem cdlemkuvN
StepHypRef Expression
1 cdlemk1.b . 2  |-  B  =  ( Base `  K
)
2 cdlemk1.l . 2  |-  .<_  =  ( le `  K )
3 cdlemk1.j . 2  |-  .\/  =  ( join `  K )
4 cdlemk1.a . 2  |-  A  =  ( Atoms `  K )
5 cdlemk1.h . 2  |-  H  =  ( LHyp `  K
)
6 cdlemk1.t . 2  |-  T  =  ( ( LTrn `  K
) `  W )
7 cdlemk1.r . 2  |-  R  =  ( ( trL `  K
) `  W )
8 cdlemk1.m . 2  |-  ./\  =  ( meet `  K )
9 cdlemk1.u . 2  |-  U  =  ( e  e.  T  |->  ( iota_ j  e.  T  ( j `  P
)  =  ( ( P  .\/  ( R `
 e ) ) 
./\  ( ( O `
 P )  .\/  ( R `  ( e  o.  `' D ) ) ) ) ) )
101, 2, 3, 4, 5, 6, 7, 8, 9cdlemksv 34456 1  |-  ( G  e.  T  ->  ( U `  G )  =  ( iota_ j  e.  T  ( j `  P )  =  ( ( P  .\/  ( R `  G )
)  ./\  ( ( O `  P )  .\/  ( R `  ( G  o.  `' D
) ) ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1455    e. wcel 1898    |-> cmpt 4475   `'ccnv 4852    o. ccom 4857   ` cfv 5601   iota_crio 6276  (class class class)co 6315   Basecbs 15170   lecple 15246   joincjn 16238   meetcmee 16239   Atomscatm 32874   LHypclh 33594   LTrncltrn 33711   trLctrl 33769
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pr 4653
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-opab 4476  df-mpt 4477  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-iota 5565  df-fun 5603  df-fv 5609  df-riota 6277  df-ov 6318
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator