Description: Part of proof of Lemma K of Crawley p. 118. Value of the sigma_2 (p) function, given V . (Contributed by NM, 2-Jul-2013) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | 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 | cdlemkuv-2N | |- ( G e. T -> ( V ` G ) = ( iota_ k e. T ( k ` P ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( Q ` P ) .\/ ( R ` ( G o. `' C ) ) ) ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdlemk2.b | |- B = ( Base ` K ) |
|
2 | cdlemk2.l | |- .<_ = ( le ` K ) |
|
3 | cdlemk2.j | |- .\/ = ( join ` K ) |
|
4 | cdlemk2.m | |- ./\ = ( meet ` K ) |
|
5 | cdlemk2.a | |- A = ( Atoms ` K ) |
|
6 | cdlemk2.h | |- H = ( LHyp ` K ) |
|
7 | cdlemk2.t | |- T = ( ( LTrn ` K ) ` W ) |
|
8 | cdlemk2.r | |- R = ( ( trL ` K ) ` W ) |
|
9 | cdlemk2.s | |- S = ( f e. T |-> ( iota_ i e. T ( i ` P ) = ( ( P .\/ ( R ` f ) ) ./\ ( ( N ` P ) .\/ ( R ` ( f o. `' F ) ) ) ) ) ) |
|
10 | cdlemk2.q | |- Q = ( S ` C ) |
|
11 | cdlemk2.v | |- V = ( d e. T |-> ( iota_ k e. T ( k ` P ) = ( ( P .\/ ( R ` d ) ) ./\ ( ( Q ` P ) .\/ ( R ` ( d o. `' C ) ) ) ) ) ) |
|
12 | 1 2 3 5 6 7 8 4 11 | cdlemksv | |- ( G e. T -> ( V ` G ) = ( iota_ k e. T ( k ` P ) = ( ( P .\/ ( R ` G ) ) ./\ ( ( Q ` P ) .\/ ( R ` ( G o. `' C ) ) ) ) ) ) |