pj1lmhm2

Description: The left projection function is a linear operator. (Contributed by Mario Carneiro, 15-Oct-2015) (Revised by Mario Carneiro, 21-Apr-2016)

	Ref	Expression
Hypotheses	pj1lmhm.l	$⊢ L = LSubSp (W)$
	pj1lmhm.s	$⊢ \underset{˙}{\oplus} = LSSum (W)$
	pj1lmhm.z	$⊢ \underset{˙}{0} = 0_{W}$
	pj1lmhm.p	$⊢ P = {proj}_{1} (W)$
	pj1lmhm.1	$⊢ φ \to W \in LMod$
	pj1lmhm.2	$⊢ φ \to T \in L$
	pj1lmhm.3	$⊢ φ \to U \in L$
	pj1lmhm.4	$⊢ φ \to T \cap U = \{\underset{˙}{0}\}$
Assertion	pj1lmhm2	$⊢ φ \to T P U \in ((W ↾_{𝑠} (T \underset{˙}{\oplus} U)) LMHom (W ↾_{𝑠} T))$

Proof

Step	Hyp	Ref	Expression
1		pj1lmhm.l	$⊢ L = LSubSp (W)$
2		pj1lmhm.s	$⊢ \underset{˙}{\oplus} = LSSum (W)$
3		pj1lmhm.z	$⊢ \underset{˙}{0} = 0_{W}$
4		pj1lmhm.p	$⊢ P = {proj}_{1} (W)$
5		pj1lmhm.1	$⊢ φ \to W \in LMod$
6		pj1lmhm.2	$⊢ φ \to T \in L$
7		pj1lmhm.3	$⊢ φ \to U \in L$
8		pj1lmhm.4	$⊢ φ \to T \cap U = \{\underset{˙}{0}\}$
9	1 2 3 4 5 6 7 8	pj1lmhm	$⊢ φ \to T P U \in ((W ↾_{𝑠} (T \underset{˙}{\oplus} U)) LMHom W)$
10		eqid	$⊢ +_{W} = +_{W}$
11		eqid	$⊢ Cntz (W) = Cntz (W)$
12	1	lsssssubg	$⊢ W \in LMod \to L \subseteq SubGrp (W)$
13	5 12	syl	$⊢ φ \to L \subseteq SubGrp (W)$
14	13 6	sseldd	$⊢ φ \to T \in SubGrp (W)$
15	13 7	sseldd	$⊢ φ \to U \in SubGrp (W)$
16		lmodabl	$⊢ W \in LMod \to W \in Abel$
17	5 16	syl	$⊢ φ \to W \in Abel$
18	11 17 14 15	ablcntzd	$⊢ φ \to T \subseteq Cntz (W) (U)$
19	10 2 3 11 14 15 8 18 4	pj1f	$⊢ φ \to (T P U) : T \underset{˙}{\oplus} U ⟶ T$
20	19	frnd	$⊢ φ \to ran (T P U) \subseteq T$
21		eqid	$⊢ W ↾_{𝑠} T = W ↾_{𝑠} T$
22	21 1	reslmhm2b	$⊢ (W \in LMod \land T \in L \land ran (T P U) \subseteq T) \to (T P U \in ((W ↾_{𝑠} (T \underset{˙}{\oplus} U)) LMHom W) \leftrightarrow T P U \in ((W ↾_{𝑠} (T \underset{˙}{\oplus} U)) LMHom (W ↾_{𝑠} T)))$
23	5 6 20 22	syl3anc	$⊢ φ \to (T P U \in ((W ↾_{𝑠} (T \underset{˙}{\oplus} U)) LMHom W) \leftrightarrow T P U \in ((W ↾_{𝑠} (T \underset{˙}{\oplus} U)) LMHom (W ↾_{𝑠} T)))$
24	9 23	mpbid	$⊢ φ \to T P U \in ((W ↾_{𝑠} (T \underset{˙}{\oplus} U)) LMHom (W ↾_{𝑠} T))$

Metamath Proof Explorer

Theorem pj1lmhm2

Proof