Theorem dihssxp

Description: An isomorphism H value is included in the vector space (expressed as T X. E ). (Contributed by NM, 26-Sep-2014)

	Ref	Expression
Hypotheses	dihssxp.b	$$⊢B={\mathrm{Base}}_K$$
	dihssxp.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dihssxp.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	dihssxp.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
	dihssxp.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
	dihssxp.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	dihssxp.x	$$⊢\phi \to X\in B$$
Assertion	dihssxp	$$⊢\phi \to I\left(X\right)\subseteq T\times E$$

Proof

Step	Hyp	Ref	Expression
1		dihssxp.b	$$⊢B={\mathrm{Base}}_K$$
2		dihssxp.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
3		dihssxp.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
4		dihssxp.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
5		dihssxp.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
6		dihssxp.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
7		dihssxp.x	$$⊢\phi \to X\in B$$
8		eqid	$$⊢\mathrm{DVecH}\left(K\right)\left(W\right)=\mathrm{DVecH}\left(K\right)\left(W\right)$$
9		eqid	$$⊢{\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)}={\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)}$$
10	1 2 5 8 9	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}}_{\mathrm{DVecH}\left(K\right)\left(W\right)}$$
11	6 7 10	syl2anc	$$⊢\phi \to I\left(X\right)\subseteq {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)}$$
12	2 3 4 8 9	dvhvbase	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)}=T\times E$$
13	6 12	syl	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)}=T\times E$$
14	11 13	sseqtrd	$$⊢\phi \to I\left(X\right)\subseteq T\times E$$