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

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

Proof of Theorem cdlemkuv-2N
StepHypRef Expression
1 cdlemk2.b . 2  |-  B  =  ( Base `  K
)
2 cdlemk2.l . 2  |-  .<_  =  ( le `  K )
3 cdlemk2.j . 2  |-  .\/  =  ( join `  K )
4 cdlemk2.a . 2  |-  A  =  ( Atoms `  K )
5 cdlemk2.h . 2  |-  H  =  ( LHyp `  K
)
6 cdlemk2.t . 2  |-  T  =  ( ( LTrn `  K
) `  W )
7 cdlemk2.r . 2  |-  R  =  ( ( trL `  K
) `  W )
8 cdlemk2.m . 2  |-  ./\  =  ( meet `  K )
9 cdlemk2.v . 2  |-  V  =  ( d  e.  T  |->  ( iota_ k  e.  T  ( k `  P
)  =  ( ( P  .\/  ( R `
 d ) ) 
./\  ( ( Q `
 P )  .\/  ( R `  ( d  o.  `' C ) ) ) ) ) )
101, 2, 3, 4, 5, 6, 7, 8, 9cdlemksv 34456 1  |-  ( G  e.  T  ->  ( V `  G )  =  ( iota_ k  e.  T  ( k `  P )  =  ( ( P  .\/  ( R `  G )
)  ./\  ( ( Q `  P )  .\/  ( R `  ( G  o.  `' C
) ) ) ) ) )
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