Theorem dia2dim

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	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	dia2dim.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	dia2dim.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	dia2dim.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dia2dim.y	$$⊢Y=\mathrm{DVecA}\left(K\right)\left(W\right)$$
	dia2dim.pl	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(Y\right)$$
	dia2dim.i	$$⊢I=\mathrm{DIsoA}\left(K\right)\left(W\right)$$
	dia2dim.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	dia2dim.u	$$⊢\phi \to \left(U\in A\wedge U\underset{\dot{}}{\le }W\right)$$
	dia2dim.v	$$⊢\phi \to \left(V\in A\wedge V\underset{\dot{}}{\le }W\right)$$
Assertion	dia2dim	$$⊢\phi \to I\left(U\underset{\dot{}}{\vee }V\right)\subseteq I\left(U\right)\underset{\dot{}}{\oplus }I\left(V\right)$$

Proof

Step	Hyp	Ref	Expression
1		dia2dim.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		dia2dim.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		dia2dim.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		dia2dim.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
5		dia2dim.y	$$⊢Y=\mathrm{DVecA}\left(K\right)\left(W\right)$$
6		dia2dim.pl	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(Y\right)$$
7		dia2dim.i	$$⊢I=\mathrm{DIsoA}\left(K\right)\left(W\right)$$
8		dia2dim.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
9		dia2dim.u	$$⊢\phi \to \left(U\in A\wedge U\underset{\dot{}}{\le }W\right)$$
10		dia2dim.v	$$⊢\phi \to \left(V\in A\wedge V\underset{\dot{}}{\le }W\right)$$
11		eqid	$$⊢\mathrm{meet}\left(K\right)=\mathrm{meet}\left(K\right)$$
12		eqid	$$⊢\mathrm{LTrn}\left(K\right)\left(W\right)=\mathrm{LTrn}\left(K\right)\left(W\right)$$
13		eqid	$$⊢\mathrm{trL}\left(K\right)\left(W\right)=\mathrm{trL}\left(K\right)\left(W\right)$$
14		eqid	$$⊢\mathrm{LSubSp}\left(Y\right)=\mathrm{LSubSp}\left(Y\right)$$
15		eqid	$$⊢\mathrm{LSpan}\left(Y\right)=\mathrm{LSpan}\left(Y\right)$$
16	1 2 11 3 4 12 13 5 14 6 15 7 8 9 10	dia2dimlem13	$$⊢\phi \to I\left(U\underset{\dot{}}{\vee }V\right)\subseteq I\left(U\right)\underset{\dot{}}{\oplus }I\left(V\right)$$