pjff

Description: A projection is a linear operator. (Contributed by Mario Carneiro, 16-Oct-2015)

		Ref	Expression
	Hypothesis	pjf.k	$⊢ K = proj (W)$
	Assertion	pjff	$⊢ W \in PreHil \to K : dom K ⟶ W LMHom W$

Proof

Step	Hyp	Ref	Expression
1		pjf.k	$⊢ K = proj (W)$
2		eqid	$⊢ LSubSp (W) = LSubSp (W)$
3		eqid	$⊢ LSSum (W) = LSSum (W)$
4		eqid	$⊢ 0_{W} = 0_{W}$
5		eqid	$⊢ {proj}_{1} (W) = {proj}_{1} (W)$
6		phllmod	$⊢ W \in PreHil \to W \in LMod$
7	6	adantr	$⊢ (W \in PreHil \land x \in dom K) \to W \in LMod$
8		eqid	$⊢ {Base}_{W} = {Base}_{W}$
9		eqid	$⊢ ocv (W) = ocv (W)$
10	8 2 9 3 1	pjdm2	$⊢ W \in PreHil \to (x \in dom K \leftrightarrow (x \in LSubSp (W) \land x LSSum (W) ocv (W) (x) = {Base}_{W}))$
11	10	simprbda	$⊢ (W \in PreHil \land x \in dom K) \to x \in LSubSp (W)$
12	8 2	lssss	$⊢ x \in LSubSp (W) \to x \subseteq {Base}_{W}$
13	11 12	syl	$⊢ (W \in PreHil \land x \in dom K) \to x \subseteq {Base}_{W}$
14	8 9 2	ocvlss	$⊢ (W \in PreHil \land x \subseteq {Base}_{W}) \to ocv (W) (x) \in LSubSp (W)$
15	13 14	syldan	$⊢ (W \in PreHil \land x \in dom K) \to ocv (W) (x) \in LSubSp (W)$
16	9 2 4	ocvin	$⊢ (W \in PreHil \land x \in LSubSp (W)) \to x \cap ocv (W) (x) = \{0_{W}\}$
17	11 16	syldan	$⊢ (W \in PreHil \land x \in dom K) \to x \cap ocv (W) (x) = \{0_{W}\}$
18	2 3 4 5 7 11 15 17	pj1lmhm	$⊢ (W \in PreHil \land x \in dom K) \to x {proj}_{1} (W) ocv (W) (x) \in ((W ↾_{𝑠} (x LSSum (W) ocv (W) (x))) LMHom W)$
19	10	simplbda	$⊢ (W \in PreHil \land x \in dom K) \to x LSSum (W) ocv (W) (x) = {Base}_{W}$
20	19	oveq2d	$⊢ (W \in PreHil \land x \in dom K) \to W ↾_{𝑠} (x LSSum (W) ocv (W) (x)) = W ↾_{𝑠} {Base}_{W}$
21	8	ressid	$⊢ W \in PreHil \to W ↾_{𝑠} {Base}_{W} = W$
22	21	adantr	$⊢ (W \in PreHil \land x \in dom K) \to W ↾_{𝑠} {Base}_{W} = W$
23	20 22	eqtrd	$⊢ (W \in PreHil \land x \in dom K) \to W ↾_{𝑠} (x LSSum (W) ocv (W) (x)) = W$
24	23	oveq1d	$⊢ (W \in PreHil \land x \in dom K) \to (W ↾_{𝑠} (x LSSum (W) ocv (W) (x))) LMHom W = W LMHom W$
25	18 24	eleqtrd	$⊢ (W \in PreHil \land x \in dom K) \to x {proj}_{1} (W) ocv (W) (x) \in (W LMHom W)$
26	9 5 1	pjfval2	$⊢ K = (x \in dom K ⟼ x {proj}_{1} (W) ocv (W) (x))$
27	25 26	fmptd	$⊢ W \in PreHil \to K : dom K ⟶ W LMHom W$

Metamath Proof Explorer

Theorem pjff

Proof