pjf2

Description: A projection is a function from the base set to the subspace. (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypotheses	pjf.k	$⊢ K = proj (W)$
	pjf.v	$⊢ V = {Base}_{W}$
Assertion	pjf2	$⊢ (W \in PreHil \land T \in dom K) \to K (T) : V ⟶ T$

Proof

Step	Hyp	Ref	Expression
1		pjf.k	$⊢ K = proj (W)$
2		pjf.v	$⊢ V = {Base}_{W}$
3		eqid	$⊢ +_{W} = +_{W}$
4		eqid	$⊢ LSSum (W) = LSSum (W)$
5		eqid	$⊢ 0_{W} = 0_{W}$
6		eqid	$⊢ Cntz (W) = Cntz (W)$
7		phllmod	$⊢ W \in PreHil \to W \in LMod$
8	7	adantr	$⊢ (W \in PreHil \land T \in dom K) \to W \in LMod$
9		eqid	$⊢ LSubSp (W) = LSubSp (W)$
10	9	lsssssubg	$⊢ W \in LMod \to LSubSp (W) \subseteq SubGrp (W)$
11	8 10	syl	$⊢ (W \in PreHil \land T \in dom K) \to LSubSp (W) \subseteq SubGrp (W)$
12		eqid	$⊢ ocv (W) = ocv (W)$
13	2 9 12 4 1	pjdm2	$⊢ W \in PreHil \to (T \in dom K \leftrightarrow (T \in LSubSp (W) \land T LSSum (W) ocv (W) (T) = V))$
14	13	simprbda	$⊢ (W \in PreHil \land T \in dom K) \to T \in LSubSp (W)$
15	11 14	sseldd	$⊢ (W \in PreHil \land T \in dom K) \to T \in SubGrp (W)$
16	2 9	lssss	$⊢ T \in LSubSp (W) \to T \subseteq V$
17	14 16	syl	$⊢ (W \in PreHil \land T \in dom K) \to T \subseteq V$
18	2 12 9	ocvlss	$⊢ (W \in PreHil \land T \subseteq V) \to ocv (W) (T) \in LSubSp (W)$
19	17 18	syldan	$⊢ (W \in PreHil \land T \in dom K) \to ocv (W) (T) \in LSubSp (W)$
20	11 19	sseldd	$⊢ (W \in PreHil \land T \in dom K) \to ocv (W) (T) \in SubGrp (W)$
21	12 9 5	ocvin	$⊢ (W \in PreHil \land T \in LSubSp (W)) \to T \cap ocv (W) (T) = \{0_{W}\}$
22	14 21	syldan	$⊢ (W \in PreHil \land T \in dom K) \to T \cap ocv (W) (T) = \{0_{W}\}$
23		lmodabl	$⊢ W \in LMod \to W \in Abel$
24	8 23	syl	$⊢ (W \in PreHil \land T \in dom K) \to W \in Abel$
25	6 24 15 20	ablcntzd	$⊢ (W \in PreHil \land T \in dom K) \to T \subseteq Cntz (W) (ocv (W) (T))$
26		eqid	$⊢ {proj}_{1} (W) = {proj}_{1} (W)$
27	3 4 5 6 15 20 22 25 26	pj1f	$⊢ (W \in PreHil \land T \in dom K) \to (T {proj}_{1} (W) ocv (W) (T)) : T LSSum (W) ocv (W) (T) ⟶ T$
28	12 26 1	pjval	$⊢ T \in dom K \to K (T) = T {proj}_{1} (W) ocv (W) (T)$
29	28	adantl	$⊢ (W \in PreHil \land T \in dom K) \to K (T) = T {proj}_{1} (W) ocv (W) (T)$
30	29	eqcomd	$⊢ (W \in PreHil \land T \in dom K) \to T {proj}_{1} (W) ocv (W) (T) = K (T)$
31	13	simplbda	$⊢ (W \in PreHil \land T \in dom K) \to T LSSum (W) ocv (W) (T) = V$
32	30 31	feq12d	$⊢ (W \in PreHil \land T \in dom K) \to ((T {proj}_{1} (W) ocv (W) (T)) : T LSSum (W) ocv (W) (T) ⟶ T \leftrightarrow K (T) : V ⟶ T)$
33	27 32	mpbid	$⊢ (W \in PreHil \land T \in dom K) \to K (T) : V ⟶ T$

Metamath Proof Explorer

Theorem pjf2

Proof