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 ‘ 𝐾 ) | |
| dia2dim.j | ⊢ ∨ = ( join ‘ 𝐾 ) | ||
| dia2dim.a | ⊢ 𝐴 = ( Atoms ‘ 𝐾 ) | ||
| dia2dim.h | ⊢ 𝐻 = ( LHyp ‘ 𝐾 ) | ||
| dia2dim.y | ⊢ 𝑌 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 ) | ||
| dia2dim.pl | ⊢ ⊕ = ( LSSum ‘ 𝑌 ) | ||
| dia2dim.i | ⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) | ||
| dia2dim.k | ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) | ||
| dia2dim.u | ⊢ ( 𝜑 → ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) | ||
| dia2dim.v | ⊢ ( 𝜑 → ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) | ||
| Assertion | dia2dim | ⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑈 ∨ 𝑉 ) ) ⊆ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dia2dim.l | ⊢ ≤ = ( le ‘ 𝐾 ) | |
| 2 | dia2dim.j | ⊢ ∨ = ( join ‘ 𝐾 ) | |
| 3 | dia2dim.a | ⊢ 𝐴 = ( Atoms ‘ 𝐾 ) | |
| 4 | dia2dim.h | ⊢ 𝐻 = ( LHyp ‘ 𝐾 ) | |
| 5 | dia2dim.y | ⊢ 𝑌 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 ) | |
| 6 | dia2dim.pl | ⊢ ⊕ = ( LSSum ‘ 𝑌 ) | |
| 7 | dia2dim.i | ⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) | |
| 8 | dia2dim.k | ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) | |
| 9 | dia2dim.u | ⊢ ( 𝜑 → ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) | |
| 10 | dia2dim.v | ⊢ ( 𝜑 → ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) | |
| 11 | eqid | ⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 ) | |
| 12 | eqid | ⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) | |
| 13 | eqid | ⊢ ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) = ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) | |
| 14 | eqid | ⊢ ( LSubSp ‘ 𝑌 ) = ( LSubSp ‘ 𝑌 ) | |
| 15 | eqid | ⊢ ( LSpan ‘ 𝑌 ) = ( LSpan ‘ 𝑌 ) | |
| 16 | 1 2 11 3 4 12 13 5 14 6 15 7 8 9 10 | dia2dimlem13 | ⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑈 ∨ 𝑉 ) ) ⊆ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) ) |