Theorem dihsumssj

Description: The subspace sum of two isomorphisms of lattice elements is less than the isomorphism of their lattice join. (Contributed by NM, 23-Sep-2014)

	Ref	Expression
Hypotheses	dihsumssj.b	$$⊢B={\mathrm{Base}}_K$$
	dihsumssj.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dihsumssj.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	dihsumssj.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dihsumssj.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
	dihsumssj.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
	dihsumssj.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	dihsumssj.x	$$⊢\phi \to X\in B$$
	dihsumssj.y	$$⊢\phi \to Y\in B$$
Assertion	dihsumssj	$$⊢\phi \to I\left(X\right)\underset{\dot{}}{\oplus }I\left(Y\right)\subseteq I\left(X\underset{\dot{}}{\vee }Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		dihsumssj.b	$$⊢B={\mathrm{Base}}_K$$
2		dihsumssj.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
3		dihsumssj.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		dihsumssj.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
5		dihsumssj.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
6		dihsumssj.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
7		dihsumssj.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
8		dihsumssj.x	$$⊢\phi \to X\in B$$
9		dihsumssj.y	$$⊢\phi \to Y\in B$$
10		eqid	$$⊢{\mathrm{Base}}_U={\mathrm{Base}}_U$$
11		eqid	$$⊢\mathrm{joinH}\left(K\right)\left(W\right)=\mathrm{joinH}\left(K\right)\left(W\right)$$
12	1 2 6 4 10	dihss	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge X\in B\right)\to I\left(X\right)\subseteq {\mathrm{Base}}_U$$
13	7 8 12	syl2anc	$$⊢\phi \to I\left(X\right)\subseteq {\mathrm{Base}}_U$$
14	1 2 6 4 10	dihss	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge Y\in B\right)\to I\left(Y\right)\subseteq {\mathrm{Base}}_U$$
15	7 9 14	syl2anc	$$⊢\phi \to I\left(Y\right)\subseteq {\mathrm{Base}}_U$$
16	2 4 10 5 11 7 13 15	djhsumss	$$⊢\phi \to I\left(X\right)\underset{\dot{}}{\oplus }I\left(Y\right)\subseteq I\left(X\right)\mathrm{joinH}\left(K\right)\left(W\right)I\left(Y\right)$$
17	1 3 2 6 11	djhlj	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left(X\in B\wedge Y\in B\right)\right)\to I\left(X\underset{\dot{}}{\vee }Y\right)=I\left(X\right)\mathrm{joinH}\left(K\right)\left(W\right)I\left(Y\right)$$
18	7 8 9 17	syl12anc	$$⊢\phi \to I\left(X\underset{\dot{}}{\vee }Y\right)=I\left(X\right)\mathrm{joinH}\left(K\right)\left(W\right)I\left(Y\right)$$
19	16 18	sseqtrrd	$$⊢\phi \to I\left(X\right)\underset{\dot{}}{\oplus }I\left(Y\right)\subseteq I\left(X\underset{\dot{}}{\vee }Y\right)$$