dihlspsnssN

Description: A subspace included in a 1-dim subspace belongs to the range of isomorphism H. (Contributed by NM, 26-Apr-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dih1dor0.h	$⊢ H = LHyp (K)$
	dih1dor0.u	$⊢ U = DVecH (K) (W)$
	dihldor0.v	$⊢ V = {Base}_{U}$
	dih1dor0.s	$⊢ S = LSubSp (U)$
	dih1dor0.n	$⊢ N = LSpan (U)$
	dih1dor0.i	$⊢ I = DIsoH (K) (W)$
Assertion	dihlspsnssN	$⊢ ((K \in HL \land W \in H) \land X \in V \land T \subseteq N (\{X\})) \to (T \in S \leftrightarrow T \in ran I)$

Proof

Step	Hyp	Ref	Expression
1		dih1dor0.h	$⊢ H = LHyp (K)$
2		dih1dor0.u	$⊢ U = DVecH (K) (W)$
3		dihldor0.v	$⊢ V = {Base}_{U}$
4		dih1dor0.s	$⊢ S = LSubSp (U)$
5		dih1dor0.n	$⊢ N = LSpan (U)$
6		dih1dor0.i	$⊢ I = DIsoH (K) (W)$
7		simpr	$⊢ ((((K \in HL \land W \in H) \land X \in V \land T \subseteq N (\{X\})) \land T \in S) \land T = N (\{X\})) \to T = N (\{X\})$
8	1 2 3 5 6	dihlsprn	$⊢ ((K \in HL \land W \in H) \land X \in V) \to N (\{X\}) \in ran I$
9	8	3adant3	$⊢ ((K \in HL \land W \in H) \land X \in V \land T \subseteq N (\{X\})) \to N (\{X\}) \in ran I$
10	9	ad2antrr	$⊢ ((((K \in HL \land W \in H) \land X \in V \land T \subseteq N (\{X\})) \land T \in S) \land T = N (\{X\})) \to N (\{X\}) \in ran I$
11	7 10	eqeltrd	$⊢ ((((K \in HL \land W \in H) \land X \in V \land T \subseteq N (\{X\})) \land T \in S) \land T = N (\{X\})) \to T \in ran I$
12		simpr	$⊢ ((((K \in HL \land W \in H) \land X \in V \land T \subseteq N (\{X\})) \land T \in S) \land T = \{0_{U}\}) \to T = \{0_{U}\}$
13		simpll1	$⊢ ((((K \in HL \land W \in H) \land X \in V \land T \subseteq N (\{X\})) \land T \in S) \land T = \{0_{U}\}) \to (K \in HL \land W \in H)$
14		eqid	$⊢ 0. (K) = 0. (K)$
15		eqid	$⊢ 0_{U} = 0_{U}$
16	14 1 6 2 15	dih0	$⊢ (K \in HL \land W \in H) \to I (0. (K)) = \{0_{U}\}$
17	13 16	syl	$⊢ ((((K \in HL \land W \in H) \land X \in V \land T \subseteq N (\{X\})) \land T \in S) \land T = \{0_{U}\}) \to I (0. (K)) = \{0_{U}\}$
18	12 17	eqtr4d	$⊢ ((((K \in HL \land W \in H) \land X \in V \land T \subseteq N (\{X\})) \land T \in S) \land T = \{0_{U}\}) \to T = I (0. (K))$
19		eqid	$⊢ {Base}_{K} = {Base}_{K}$
20	19 1 6	dihfn	$⊢ (K \in HL \land W \in H) \to I Fn {Base}_{K}$
21	13 20	syl	$⊢ ((((K \in HL \land W \in H) \land X \in V \land T \subseteq N (\{X\})) \land T \in S) \land T = \{0_{U}\}) \to I Fn {Base}_{K}$
22		simp1l	$⊢ ((K \in HL \land W \in H) \land X \in V \land T \subseteq N (\{X\})) \to K \in HL$
23	22	ad2antrr	$⊢ ((((K \in HL \land W \in H) \land X \in V \land T \subseteq N (\{X\})) \land T \in S) \land T = \{0_{U}\}) \to K \in HL$
24		hlop	$⊢ K \in HL \to K \in OP$
25	19 14	op0cl	$⊢ K \in OP \to 0. (K) \in {Base}_{K}$
26	23 24 25	3syl	$⊢ ((((K \in HL \land W \in H) \land X \in V \land T \subseteq N (\{X\})) \land T \in S) \land T = \{0_{U}\}) \to 0. (K) \in {Base}_{K}$
27		fnfvelrn	$⊢ (I Fn {Base}_{K} \land 0. (K) \in {Base}_{K}) \to I (0. (K)) \in ran I$
28	21 26 27	syl2anc	$⊢ ((((K \in HL \land W \in H) \land X \in V \land T \subseteq N (\{X\})) \land T \in S) \land T = \{0_{U}\}) \to I (0. (K)) \in ran I$
29	18 28	eqeltrd	$⊢ ((((K \in HL \land W \in H) \land X \in V \land T \subseteq N (\{X\})) \land T \in S) \land T = \{0_{U}\}) \to T \in ran I$
30		simpl1	$⊢ (((K \in HL \land W \in H) \land X \in V \land T \subseteq N (\{X\})) \land T \in S) \to (K \in HL \land W \in H)$
31	1 2 30	dvhlvec	$⊢ (((K \in HL \land W \in H) \land X \in V \land T \subseteq N (\{X\})) \land T \in S) \to U \in LVec$
32		simpr	$⊢ (((K \in HL \land W \in H) \land X \in V \land T \subseteq N (\{X\})) \land T \in S) \to T \in S$
33		simpl2	$⊢ (((K \in HL \land W \in H) \land X \in V \land T \subseteq N (\{X\})) \land T \in S) \to X \in V$
34		simpl3	$⊢ (((K \in HL \land W \in H) \land X \in V \land T \subseteq N (\{X\})) \land T \in S) \to T \subseteq N (\{X\})$
35	3 15 4 5	lspsnat	$⊢ ((U \in LVec \land T \in S \land X \in V) \land T \subseteq N (\{X\})) \to (T = N (\{X\}) \lor T = \{0_{U}\})$
36	31 32 33 34 35	syl31anc	$⊢ (((K \in HL \land W \in H) \land X \in V \land T \subseteq N (\{X\})) \land T \in S) \to (T = N (\{X\}) \lor T = \{0_{U}\})$
37	11 29 36	mpjaodan	$⊢ (((K \in HL \land W \in H) \land X \in V \land T \subseteq N (\{X\})) \land T \in S) \to T \in ran I$
38	37	ex	$⊢ ((K \in HL \land W \in H) \land X \in V \land T \subseteq N (\{X\})) \to (T \in S \to T \in ran I)$
39	1 2 6 4	dihsslss	$⊢ (K \in HL \land W \in H) \to ran I \subseteq S$
40	39	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land X \in V \land T \subseteq N (\{X\})) \to ran I \subseteq S$
41	40	sseld	$⊢ ((K \in HL \land W \in H) \land X \in V \land T \subseteq N (\{X\})) \to (T \in ran I \to T \in S)$
42	38 41	impbid	$⊢ ((K \in HL \land W \in H) \land X \in V \land T \subseteq N (\{X\})) \to (T \in S \leftrightarrow T \in ran I)$

Metamath Proof Explorer

Theorem dihlspsnssN

Proof