dvadiaN

Description: Any closed subspace is a member of the range of partial isomorphism A, showing the isomorphism maps onto the set of closed subspaces of partial vector space A. (Contributed by NM, 17-Jan-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dvadia.h	$⊢ H = LHyp (K)$
	dvadia.u	$⊢ U = DVecA (K) (W)$
	dvadia.i	$⊢ I = DIsoA (K) (W)$
	dvadia.n	$⊢ \underset{˙}{⊥} = ocA (K) (W)$
	dvadia.s	$⊢ S = LSubSp (U)$
Assertion	dvadiaN	$⊢ ((K \in HL \land W \in H) \land (X \in S \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X)) \to X \in ran I$

Proof

Step	Hyp	Ref	Expression
1		dvadia.h	$⊢ H = LHyp (K)$
2		dvadia.u	$⊢ U = DVecA (K) (W)$
3		dvadia.i	$⊢ I = DIsoA (K) (W)$
4		dvadia.n	$⊢ \underset{˙}{⊥} = ocA (K) (W)$
5		dvadia.s	$⊢ S = LSubSp (U)$
6		simprr	$⊢ ((K \in HL \land W \in H) \land (X \in S \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X$
7		eqid	$⊢ {Base}_{U} = {Base}_{U}$
8	7 5	lssss	$⊢ X \in S \to X \subseteq {Base}_{U}$
9	8	ad2antrl	$⊢ ((K \in HL \land W \in H) \land (X \in S \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X)) \to X \subseteq {Base}_{U}$
10		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
11	1 10 2 7	dvavbase	$⊢ (K \in HL \land W \in H) \to {Base}_{U} = LTrn (K) (W)$
12	11	adantr	$⊢ ((K \in HL \land W \in H) \land (X \in S \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X)) \to {Base}_{U} = LTrn (K) (W)$
13	9 12	sseqtrd	$⊢ ((K \in HL \land W \in H) \land (X \in S \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X)) \to X \subseteq LTrn (K) (W)$
14	1 10 3 4	docaclN	$⊢ ((K \in HL \land W \in H) \land X \subseteq LTrn (K) (W)) \to \underset{˙}{⊥} (X) \in ran I$
15	13 14	syldan	$⊢ ((K \in HL \land W \in H) \land (X \in S \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X)) \to \underset{˙}{⊥} (X) \in ran I$
16	1 10 3	diaelrnN	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (X) \in ran I) \to \underset{˙}{⊥} (X) \subseteq LTrn (K) (W)$
17	15 16	syldan	$⊢ ((K \in HL \land W \in H) \land (X \in S \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X)) \to \underset{˙}{⊥} (X) \subseteq LTrn (K) (W)$
18	1 10 3 4	docaclN	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (X) \subseteq LTrn (K) (W)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \in ran I$
19	17 18	syldan	$⊢ ((K \in HL \land W \in H) \land (X \in S \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \in ran I$
20	6 19	eqeltrrd	$⊢ ((K \in HL \land W \in H) \land (X \in S \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X)) \to X \in ran I$

Metamath Proof Explorer

Theorem dvadiaN

Proof