Description: A two-dimensional subspace of partial vector space A is closed, or equivalently, the isomorphism of a join of two atoms is a subset of the subspace sum of the isomorphisms of each atom (and thus they are equal, as shown later for the full vector space H). (Contributed by NM, 9-Sep-2014)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | dia2dim.l | |- .<_ = ( le ` K ) |
|
| dia2dim.j | |- .\/ = ( join ` K ) |
||
| dia2dim.a | |- A = ( Atoms ` K ) |
||
| dia2dim.h | |- H = ( LHyp ` K ) |
||
| dia2dim.y | |- Y = ( ( DVecA ` K ) ` W ) |
||
| dia2dim.pl | |- .(+) = ( LSSum ` Y ) |
||
| dia2dim.i | |- I = ( ( DIsoA ` K ) ` W ) |
||
| dia2dim.k | |- ( ph -> ( K e. HL /\ W e. H ) ) |
||
| dia2dim.u | |- ( ph -> ( U e. A /\ U .<_ W ) ) |
||
| dia2dim.v | |- ( ph -> ( V e. A /\ V .<_ W ) ) |
||
| Assertion | dia2dim | |- ( ph -> ( I ` ( U .\/ V ) ) C_ ( ( I ` U ) .(+) ( I ` V ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dia2dim.l | |- .<_ = ( le ` K ) |
|
| 2 | dia2dim.j | |- .\/ = ( join ` K ) |
|
| 3 | dia2dim.a | |- A = ( Atoms ` K ) |
|
| 4 | dia2dim.h | |- H = ( LHyp ` K ) |
|
| 5 | dia2dim.y | |- Y = ( ( DVecA ` K ) ` W ) |
|
| 6 | dia2dim.pl | |- .(+) = ( LSSum ` Y ) |
|
| 7 | dia2dim.i | |- I = ( ( DIsoA ` K ) ` W ) |
|
| 8 | dia2dim.k | |- ( ph -> ( K e. HL /\ W e. H ) ) |
|
| 9 | dia2dim.u | |- ( ph -> ( U e. A /\ U .<_ W ) ) |
|
| 10 | dia2dim.v | |- ( ph -> ( V e. A /\ V .<_ W ) ) |
|
| 11 | eqid | |- ( meet ` K ) = ( meet ` K ) |
|
| 12 | eqid | |- ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W ) |
|
| 13 | eqid | |- ( ( trL ` K ) ` W ) = ( ( trL ` K ) ` W ) |
|
| 14 | eqid | |- ( LSubSp ` Y ) = ( LSubSp ` Y ) |
|
| 15 | eqid | |- ( LSpan ` Y ) = ( LSpan ` Y ) |
|
| 16 | 1 2 11 3 4 12 13 5 14 6 15 7 8 9 10 | dia2dimlem13 | |- ( ph -> ( I ` ( U .\/ V ) ) C_ ( ( I ` U ) .(+) ( I ` V ) ) ) |