Description: Lemma for dia2dim . Convert ordering hypothesis on RF to subspace membership F e. ( I( U .\/ V ) ) . (Contributed by NM, 8-Sep-2014)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | dia2dimlem11.l | |- .<_ = ( le ` K ) |
|
| dia2dimlem11.j | |- .\/ = ( join ` K ) |
||
| dia2dimlem11.m | |- ./\ = ( meet ` K ) |
||
| dia2dimlem11.a | |- A = ( Atoms ` K ) |
||
| dia2dimlem11.h | |- H = ( LHyp ` K ) |
||
| dia2dimlem11.t | |- T = ( ( LTrn ` K ) ` W ) |
||
| dia2dimlem11.r | |- R = ( ( trL ` K ) ` W ) |
||
| dia2dimlem11.y | |- Y = ( ( DVecA ` K ) ` W ) |
||
| dia2dimlem11.s | |- S = ( LSubSp ` Y ) |
||
| dia2dimlem11.pl | |- .(+) = ( LSSum ` Y ) |
||
| dia2dimlem11.n | |- N = ( LSpan ` Y ) |
||
| dia2dimlem11.i | |- I = ( ( DIsoA ` K ) ` W ) |
||
| dia2dimlem11.k | |- ( ph -> ( K e. HL /\ W e. H ) ) |
||
| dia2dimlem11.u | |- ( ph -> ( U e. A /\ U .<_ W ) ) |
||
| dia2dimlem11.v | |- ( ph -> ( V e. A /\ V .<_ W ) ) |
||
| dia2dimlem11.f | |- ( ph -> F e. T ) |
||
| dia2dimlem11.uv | |- ( ph -> U =/= V ) |
||
| dia2dimlem11.fe | |- ( ph -> F e. ( I ` ( U .\/ V ) ) ) |
||
| Assertion | dia2dimlem11 | |- ( ph -> F e. ( ( I ` U ) .(+) ( I ` V ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dia2dimlem11.l | |- .<_ = ( le ` K ) |
|
| 2 | dia2dimlem11.j | |- .\/ = ( join ` K ) |
|
| 3 | dia2dimlem11.m | |- ./\ = ( meet ` K ) |
|
| 4 | dia2dimlem11.a | |- A = ( Atoms ` K ) |
|
| 5 | dia2dimlem11.h | |- H = ( LHyp ` K ) |
|
| 6 | dia2dimlem11.t | |- T = ( ( LTrn ` K ) ` W ) |
|
| 7 | dia2dimlem11.r | |- R = ( ( trL ` K ) ` W ) |
|
| 8 | dia2dimlem11.y | |- Y = ( ( DVecA ` K ) ` W ) |
|
| 9 | dia2dimlem11.s | |- S = ( LSubSp ` Y ) |
|
| 10 | dia2dimlem11.pl | |- .(+) = ( LSSum ` Y ) |
|
| 11 | dia2dimlem11.n | |- N = ( LSpan ` Y ) |
|
| 12 | dia2dimlem11.i | |- I = ( ( DIsoA ` K ) ` W ) |
|
| 13 | dia2dimlem11.k | |- ( ph -> ( K e. HL /\ W e. H ) ) |
|
| 14 | dia2dimlem11.u | |- ( ph -> ( U e. A /\ U .<_ W ) ) |
|
| 15 | dia2dimlem11.v | |- ( ph -> ( V e. A /\ V .<_ W ) ) |
|
| 16 | dia2dimlem11.f | |- ( ph -> F e. T ) |
|
| 17 | dia2dimlem11.uv | |- ( ph -> U =/= V ) |
|
| 18 | dia2dimlem11.fe | |- ( ph -> F e. ( I ` ( U .\/ V ) ) ) |
|
| 19 | 1 2 4 5 6 7 8 9 11 12 13 14 15 16 18 | dia2dimlem10 | |- ( ph -> ( R ` F ) .<_ ( U .\/ V ) ) |
| 20 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 19 17 | dia2dimlem9 | |- ( ph -> F e. ( ( I ` U ) .(+) ( I ` V ) ) ) |