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