dibss

Description: The partial isomorphism B maps to a set of vectors in full vector space H. (Contributed by NM, 1-Jan-2014)

	Ref	Expression
Hypotheses	dibss.b	$⊢ B = {Base}_{K}$
	dibss.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dibss.h	$⊢ H = LHyp (K)$
	dibss.i	$⊢ I = DIsoB (K) (W)$
	dibss.u	$⊢ U = DVecH (K) (W)$
	dibss.v	$⊢ V = {Base}_{U}$
Assertion	dibss	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to I (X) \subseteq V$

Proof

Step	Hyp	Ref	Expression
1		dibss.b	$⊢ B = {Base}_{K}$
2		dibss.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dibss.h	$⊢ H = LHyp (K)$
4		dibss.i	$⊢ I = DIsoB (K) (W)$
5		dibss.u	$⊢ U = DVecH (K) (W)$
6		dibss.v	$⊢ V = {Base}_{U}$
7		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
8		eqid	$⊢ DIsoA (K) (W) = DIsoA (K) (W)$
9	1 2 3 7 8	diass	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to DIsoA (K) (W) (X) \subseteq LTrn (K) (W)$
10		eqid	$⊢ TEndo (K) (W) = TEndo (K) (W)$
11		eqid	$⊢ (f \in LTrn (K) (W) ⟼ {I ↾}_{B}) = (f \in LTrn (K) (W) ⟼ {I ↾}_{B})$
12	1 3 7 10 11	tendo0cl	$⊢ (K \in HL \land W \in H) \to (f \in LTrn (K) (W) ⟼ {I ↾}_{B}) \in TEndo (K) (W)$
13	12	snssd	$⊢ (K \in HL \land W \in H) \to \{(f \in LTrn (K) (W) ⟼ {I ↾}_{B})\} \subseteq TEndo (K) (W)$
14	13	adantr	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to \{(f \in LTrn (K) (W) ⟼ {I ↾}_{B})\} \subseteq TEndo (K) (W)$
15		xpss12	$⊢ (DIsoA (K) (W) (X) \subseteq LTrn (K) (W) \land \{(f \in LTrn (K) (W) ⟼ {I ↾}_{B})\} \subseteq TEndo (K) (W)) \to DIsoA (K) (W) (X) \times \{(f \in LTrn (K) (W) ⟼ {I ↾}_{B})\} \subseteq LTrn (K) (W) \times TEndo (K) (W)$
16	9 14 15	syl2anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to DIsoA (K) (W) (X) \times \{(f \in LTrn (K) (W) ⟼ {I ↾}_{B})\} \subseteq LTrn (K) (W) \times TEndo (K) (W)$
17	1 2 3 7 11 8 4	dibval2	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to I (X) = DIsoA (K) (W) (X) \times \{(f \in LTrn (K) (W) ⟼ {I ↾}_{B})\}$
18	3 7 10 5 6	dvhvbase	$⊢ (K \in HL \land W \in H) \to V = LTrn (K) (W) \times TEndo (K) (W)$
19	18	adantr	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to V = LTrn (K) (W) \times TEndo (K) (W)$
20	16 17 19	3sstr4d	$⊢ ((K \in HL \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to I (X) \subseteq V$

Metamath Proof Explorer

Theorem dibss

Proof