diarnN

Description: Partial isomorphism A maps onto the set of all closed subspaces of partial vector space A. Part of Lemma M of Crawley p. 121 line 12, with closed subspaces rather than subspaces. (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	diarnN	$⊢ (K \in HL \land W \in H) \to ran I = \{x \in S \| \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x\}$

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	1 2 3 5	diasslssN	$⊢ (K \in HL \land W \in H) \to ran I \subseteq S$
7		sseqin2	$⊢ ran I \subseteq S \leftrightarrow S \cap ran I = ran I$
8	6 7	sylib	$⊢ (K \in HL \land W \in H) \to S \cap ran I = ran I$
9	1 3 4	doca3N	$⊢ ((K \in HL \land W \in H) \land x \in ran I) \to \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x$
10	9	ex	$⊢ (K \in HL \land W \in H) \to (x \in ran I \to \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x)$
11	10	adantr	$⊢ ((K \in HL \land W \in H) \land x \in S) \to (x \in ran I \to \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x)$
12	1 2 3 4 5	dvadiaN	$⊢ ((K \in HL \land W \in H) \land (x \in S \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x)) \to x \in ran I$
13	12	expr	$⊢ ((K \in HL \land W \in H) \land x \in S) \to (\underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x \to x \in ran I)$
14	11 13	impbid	$⊢ ((K \in HL \land W \in H) \land x \in S) \to (x \in ran I \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x)$
15	14	rabbi2dva	$⊢ (K \in HL \land W \in H) \to S \cap ran I = \{x \in S \| \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x\}$
16	8 15	eqtr3d	$⊢ (K \in HL \land W \in H) \to ran I = \{x \in S \| \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x\}$

Metamath Proof Explorer

Theorem diarnN

Proof