Description: Part of proof of Lemma E in Crawley p. 114, first part of 4th paragraph. We show, in their notation, f_s(p)=q. TODO FIX COMMENT. (Contributed by NM, 11-Apr-2013)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | cdlemef46.b | |- B = ( Base ` K ) |
|
| cdlemef46.l | |- .<_ = ( le ` K ) |
||
| cdlemef46.j | |- .\/ = ( join ` K ) |
||
| cdlemef46.m | |- ./\ = ( meet ` K ) |
||
| cdlemef46.a | |- A = ( Atoms ` K ) |
||
| cdlemef46.h | |- H = ( LHyp ` K ) |
||
| cdlemef46.u | |- U = ( ( P .\/ Q ) ./\ W ) |
||
| cdlemef46.d | |- D = ( ( t .\/ U ) ./\ ( Q .\/ ( ( P .\/ t ) ./\ W ) ) ) |
||
| cdlemefs46.e | |- E = ( ( P .\/ Q ) ./\ ( D .\/ ( ( s .\/ t ) ./\ W ) ) ) |
||
| cdlemef46.f | |- F = ( x e. B |-> if ( ( P =/= Q /\ -. x .<_ W ) , ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( x ./\ W ) ) = x ) -> z = ( if ( s .<_ ( P .\/ Q ) , ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = E ) ) , [_ s / t ]_ D ) .\/ ( x ./\ W ) ) ) ) , x ) ) |
||
| Assertion | cdleme17d | |- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( F ` P ) = Q ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cdlemef46.b | |- B = ( Base ` K ) |
|
| 2 | cdlemef46.l | |- .<_ = ( le ` K ) |
|
| 3 | cdlemef46.j | |- .\/ = ( join ` K ) |
|
| 4 | cdlemef46.m | |- ./\ = ( meet ` K ) |
|
| 5 | cdlemef46.a | |- A = ( Atoms ` K ) |
|
| 6 | cdlemef46.h | |- H = ( LHyp ` K ) |
|
| 7 | cdlemef46.u | |- U = ( ( P .\/ Q ) ./\ W ) |
|
| 8 | cdlemef46.d | |- D = ( ( t .\/ U ) ./\ ( Q .\/ ( ( P .\/ t ) ./\ W ) ) ) |
|
| 9 | cdlemefs46.e | |- E = ( ( P .\/ Q ) ./\ ( D .\/ ( ( s .\/ t ) ./\ W ) ) ) |
|
| 10 | cdlemef46.f | |- F = ( x e. B |-> if ( ( P =/= Q /\ -. x .<_ W ) , ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( x ./\ W ) ) = x ) -> z = ( if ( s .<_ ( P .\/ Q ) , ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = E ) ) , [_ s / t ]_ D ) .\/ ( x ./\ W ) ) ) ) , x ) ) |
|
| 11 | 1 2 3 4 5 6 7 8 9 10 | cdleme17d4 | |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P = Q ) -> ( F ` P ) = Q ) |
| 12 | 1 2 3 4 5 6 7 8 9 10 | cdleme17d3 | |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P =/= Q ) -> ( F ` P ) = Q ) |
| 13 | 11 12 | pm2.61dane | |- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( F ` P ) = Q ) |