pjfo

Description: A projection is a surjection onto the subspace. (Contributed by Mario Carneiro, 16-Oct-2015)

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

Proof

Step	Hyp	Ref	Expression
1		pjf.k	$⊢ K = proj (W)$
2		pjf.v	$⊢ V = {Base}_{W}$
3	1 2	pjf2	$⊢ (W \in PreHil \land T \in dom K) \to K (T) : V ⟶ T$
4	3	frnd	$⊢ (W \in PreHil \land T \in dom K) \to ran K (T) \subseteq T$
5		eqid	$⊢ ocv (W) = ocv (W)$
6		eqid	$⊢ {proj}_{1} (W) = {proj}_{1} (W)$
7	5 6 1	pjval	$⊢ T \in dom K \to K (T) = T {proj}_{1} (W) ocv (W) (T)$
8	7	ad2antlr	$⊢ ((W \in PreHil \land T \in dom K) \land x \in T) \to K (T) = T {proj}_{1} (W) ocv (W) (T)$
9	8	fveq1d	$⊢ ((W \in PreHil \land T \in dom K) \land x \in T) \to K (T) (x) = (T {proj}_{1} (W) ocv (W) (T)) (x)$
10		eqid	$⊢ +_{W} = +_{W}$
11		eqid	$⊢ LSSum (W) = LSSum (W)$
12		eqid	$⊢ 0_{W} = 0_{W}$
13		eqid	$⊢ Cntz (W) = Cntz (W)$
14		phllmod	$⊢ W \in PreHil \to W \in LMod$
15	14	adantr	$⊢ (W \in PreHil \land T \in dom K) \to W \in LMod$
16		eqid	$⊢ LSubSp (W) = LSubSp (W)$
17	16	lsssssubg	$⊢ W \in LMod \to LSubSp (W) \subseteq SubGrp (W)$
18	15 17	syl	$⊢ (W \in PreHil \land T \in dom K) \to LSubSp (W) \subseteq SubGrp (W)$
19	2 16 5 11 1	pjdm2	$⊢ W \in PreHil \to (T \in dom K \leftrightarrow (T \in LSubSp (W) \land T LSSum (W) ocv (W) (T) = V))$
20	19	simprbda	$⊢ (W \in PreHil \land T \in dom K) \to T \in LSubSp (W)$
21	18 20	sseldd	$⊢ (W \in PreHil \land T \in dom K) \to T \in SubGrp (W)$
22	2 16	lssss	$⊢ T \in LSubSp (W) \to T \subseteq V$
23	20 22	syl	$⊢ (W \in PreHil \land T \in dom K) \to T \subseteq V$
24	2 5 16	ocvlss	$⊢ (W \in PreHil \land T \subseteq V) \to ocv (W) (T) \in LSubSp (W)$
25	23 24	syldan	$⊢ (W \in PreHil \land T \in dom K) \to ocv (W) (T) \in LSubSp (W)$
26	18 25	sseldd	$⊢ (W \in PreHil \land T \in dom K) \to ocv (W) (T) \in SubGrp (W)$
27	5 16 12	ocvin	$⊢ (W \in PreHil \land T \in LSubSp (W)) \to T \cap ocv (W) (T) = \{0_{W}\}$
28	20 27	syldan	$⊢ (W \in PreHil \land T \in dom K) \to T \cap ocv (W) (T) = \{0_{W}\}$
29		lmodabl	$⊢ W \in LMod \to W \in Abel$
30	15 29	syl	$⊢ (W \in PreHil \land T \in dom K) \to W \in Abel$
31	13 30 21 26	ablcntzd	$⊢ (W \in PreHil \land T \in dom K) \to T \subseteq Cntz (W) (ocv (W) (T))$
32	10 11 12 13 21 26 28 31 6	pj1lid	$⊢ ((W \in PreHil \land T \in dom K) \land x \in T) \to (T {proj}_{1} (W) ocv (W) (T)) (x) = x$
33	9 32	eqtrd	$⊢ ((W \in PreHil \land T \in dom K) \land x \in T) \to K (T) (x) = x$
34	3	ffnd	$⊢ (W \in PreHil \land T \in dom K) \to K (T) Fn V$
35	23	sselda	$⊢ ((W \in PreHil \land T \in dom K) \land x \in T) \to x \in V$
36		fnfvelrn	$⊢ (K (T) Fn V \land x \in V) \to K (T) (x) \in ran K (T)$
37	34 35 36	syl2an2r	$⊢ ((W \in PreHil \land T \in dom K) \land x \in T) \to K (T) (x) \in ran K (T)$
38	33 37	eqeltrrd	$⊢ ((W \in PreHil \land T \in dom K) \land x \in T) \to x \in ran K (T)$
39	4 38	eqelssd	$⊢ (W \in PreHil \land T \in dom K) \to ran K (T) = T$
40		dffo2	$⊢ K (T) : V \underset{onto}{⟶} T \leftrightarrow (K (T) : V ⟶ T \land ran K (T) = T)$
41	3 39 40	sylanbrc	$⊢ (W \in PreHil \land T \in dom K) \to K (T) : V \underset{onto}{⟶} T$

Metamath Proof Explorer

Theorem pjfo

Proof