pjdm

Description: A subspace is in the domain of the projection function iff the subspace admits a projection decomposition of the whole space. (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypotheses	pjfval.v	$⊢ V = {Base}_{W}$
	pjfval.l	$⊢ L = LSubSp (W)$
	pjfval.o	$⊢ \underset{˙}{⊥} = ocv (W)$
	pjfval.p	$⊢ P = {proj}_{1} (W)$
	pjfval.k	$⊢ K = proj (W)$
Assertion	pjdm	$⊢ T \in dom K \leftrightarrow (T \in L \land (T P \underset{˙}{⊥} (T)) : V ⟶ V)$

Proof

Step	Hyp	Ref	Expression
1		pjfval.v	$⊢ V = {Base}_{W}$
2		pjfval.l	$⊢ L = LSubSp (W)$
3		pjfval.o	$⊢ \underset{˙}{⊥} = ocv (W)$
4		pjfval.p	$⊢ P = {proj}_{1} (W)$
5		pjfval.k	$⊢ K = proj (W)$
6		id	$⊢ x = T \to x = T$
7		fveq2	$⊢ x = T \to \underset{˙}{⊥} (x) = \underset{˙}{⊥} (T)$
8	6 7	oveq12d	$⊢ x = T \to x P \underset{˙}{⊥} (x) = T P \underset{˙}{⊥} (T)$
9	8	eleq1d	$⊢ x = T \to (x P \underset{˙}{⊥} (x) \in (V^{V}) \leftrightarrow T P \underset{˙}{⊥} (T) \in (V^{V}))$
10	1	fvexi	$⊢ V \in V$
11	10 10	elmap	$⊢ T P \underset{˙}{⊥} (T) \in (V^{V}) \leftrightarrow (T P \underset{˙}{⊥} (T)) : V ⟶ V$
12	9 11	bitrdi	$⊢ x = T \to (x P \underset{˙}{⊥} (x) \in (V^{V}) \leftrightarrow (T P \underset{˙}{⊥} (T)) : V ⟶ V)$
13		cnvin	$⊢ {((x \in L ⟼ x P \underset{˙}{⊥} (x)) \cap (V \times (V^{V})))}^{-1} = {(x \in L ⟼ x P \underset{˙}{⊥} (x))}^{-1} \cap {(V \times (V^{V}))}^{-1}$
14		cnvxp	$⊢ {(V \times (V^{V}))}^{-1} = (V^{V}) \times V$
15	14	ineq2i	$⊢ {(x \in L ⟼ x P \underset{˙}{⊥} (x))}^{-1} \cap {(V \times (V^{V}))}^{-1} = {(x \in L ⟼ x P \underset{˙}{⊥} (x))}^{-1} \cap ((V^{V}) \times V)$
16	13 15	eqtri	$⊢ {((x \in L ⟼ x P \underset{˙}{⊥} (x)) \cap (V \times (V^{V})))}^{-1} = {(x \in L ⟼ x P \underset{˙}{⊥} (x))}^{-1} \cap ((V^{V}) \times V)$
17	1 2 3 4 5	pjfval	$⊢ K = (x \in L ⟼ x P \underset{˙}{⊥} (x)) \cap (V \times (V^{V}))$
18	17	cnveqi	$⊢ K^{-1} = {((x \in L ⟼ x P \underset{˙}{⊥} (x)) \cap (V \times (V^{V})))}^{-1}$
19		df-res	$⊢ {{(x \in L ⟼ x P \underset{˙}{⊥} (x))}^{-1} ↾}_{(V^{V})} = {(x \in L ⟼ x P \underset{˙}{⊥} (x))}^{-1} \cap ((V^{V}) \times V)$
20	16 18 19	3eqtr4i	$⊢ K^{-1} = {{(x \in L ⟼ x P \underset{˙}{⊥} (x))}^{-1} ↾}_{(V^{V})}$
21	20	rneqi	$⊢ ran K^{-1} = ran ({{(x \in L ⟼ x P \underset{˙}{⊥} (x))}^{-1} ↾}_{(V^{V})})$
22		dfdm4	$⊢ dom K = ran K^{-1}$
23		df-ima	$⊢ {(x \in L ⟼ x P \underset{˙}{⊥} (x))}^{-1} [V^{V}] = ran ({{(x \in L ⟼ x P \underset{˙}{⊥} (x))}^{-1} ↾}_{(V^{V})})$
24	21 22 23	3eqtr4i	$⊢ dom K = {(x \in L ⟼ x P \underset{˙}{⊥} (x))}^{-1} [V^{V}]$
25		eqid	$⊢ (x \in L ⟼ x P \underset{˙}{⊥} (x)) = (x \in L ⟼ x P \underset{˙}{⊥} (x))$
26	25	mptpreima	$⊢ {(x \in L ⟼ x P \underset{˙}{⊥} (x))}^{-1} [V^{V}] = \{x \in L \| x P \underset{˙}{⊥} (x) \in (V^{V})\}$
27	24 26	eqtri	$⊢ dom K = \{x \in L \| x P \underset{˙}{⊥} (x) \in (V^{V})\}$
28	12 27	elrab2	$⊢ T \in dom K \leftrightarrow (T \in L \land (T P \underset{˙}{⊥} (T)) : V ⟶ V)$

Metamath Proof Explorer

Theorem pjdm

Proof