pj1lmhm

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	pj1lmhm	$⊢ φ \to T P U \in ((W ↾_{𝑠} (T \underset{˙}{\oplus} U)) LMHom W)$

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		eqid	$⊢ +_{W} = +_{W}$
10		eqid	$⊢ Cntz (W) = Cntz (W)$
11	1	lsssssubg	$⊢ W \in LMod \to L \subseteq SubGrp (W)$
12	5 11	syl	$⊢ φ \to L \subseteq SubGrp (W)$
13	12 6	sseldd	$⊢ φ \to T \in SubGrp (W)$
14	12 7	sseldd	$⊢ φ \to U \in SubGrp (W)$
15		lmodabl	$⊢ W \in LMod \to W \in Abel$
16	5 15	syl	$⊢ φ \to W \in Abel$
17	10 16 13 14	ablcntzd	$⊢ φ \to T \subseteq Cntz (W) (U)$
18	9 2 3 10 13 14 8 17 4	pj1ghm	$⊢ φ \to T P U \in ((W ↾_{𝑠} (T \underset{˙}{\oplus} U)) GrpHom W)$
19		eqid	$⊢ Scalar (W) = Scalar (W)$
20	19	a1i	$⊢ φ \to Scalar (W) = Scalar (W)$
21	9 2 3 10 13 14 8 17 4	pj1id	$⊢ (φ \land y \in (T \underset{˙}{\oplus} U)) \to y = (T P U) (y) +_{W} (U P T) (y)$
22	21	adantrl	$⊢ (φ \land (x \in {Base}_{Scalar (W)} \land y \in (T \underset{˙}{\oplus} U))) \to y = (T P U) (y) +_{W} (U P T) (y)$
23	22	oveq2d	$⊢ (φ \land (x \in {Base}_{Scalar (W)} \land y \in (T \underset{˙}{\oplus} U))) \to x \cdot_{W} y = x \cdot_{W} ((T P U) (y) +_{W} (U P T) (y))$
24	5	adantr	$⊢ (φ \land (x \in {Base}_{Scalar (W)} \land y \in (T \underset{˙}{\oplus} U))) \to W \in LMod$
25		simprl	$⊢ (φ \land (x \in {Base}_{Scalar (W)} \land y \in (T \underset{˙}{\oplus} U))) \to x \in {Base}_{Scalar (W)}$
26	6	adantr	$⊢ (φ \land (x \in {Base}_{Scalar (W)} \land y \in (T \underset{˙}{\oplus} U))) \to T \in L$
27		eqid	$⊢ {Base}_{W} = {Base}_{W}$
28	27 1	lssss	$⊢ T \in L \to T \subseteq {Base}_{W}$
29	26 28	syl	$⊢ (φ \land (x \in {Base}_{Scalar (W)} \land y \in (T \underset{˙}{\oplus} U))) \to T \subseteq {Base}_{W}$
30	13	adantr	$⊢ (φ \land (x \in {Base}_{Scalar (W)} \land y \in (T \underset{˙}{\oplus} U))) \to T \in SubGrp (W)$
31	14	adantr	$⊢ (φ \land (x \in {Base}_{Scalar (W)} \land y \in (T \underset{˙}{\oplus} U))) \to U \in SubGrp (W)$
32	8	adantr	$⊢ (φ \land (x \in {Base}_{Scalar (W)} \land y \in (T \underset{˙}{\oplus} U))) \to T \cap U = \{\underset{˙}{0}\}$
33	17	adantr	$⊢ (φ \land (x \in {Base}_{Scalar (W)} \land y \in (T \underset{˙}{\oplus} U))) \to T \subseteq Cntz (W) (U)$
34	9 2 3 10 30 31 32 33 4	pj1f	$⊢ (φ \land (x \in {Base}_{Scalar (W)} \land y \in (T \underset{˙}{\oplus} U))) \to (T P U) : T \underset{˙}{\oplus} U ⟶ T$
35		simprr	$⊢ (φ \land (x \in {Base}_{Scalar (W)} \land y \in (T \underset{˙}{\oplus} U))) \to y \in (T \underset{˙}{\oplus} U)$
36	34 35	ffvelcdmd	$⊢ (φ \land (x \in {Base}_{Scalar (W)} \land y \in (T \underset{˙}{\oplus} U))) \to (T P U) (y) \in T$
37	29 36	sseldd	$⊢ (φ \land (x \in {Base}_{Scalar (W)} \land y \in (T \underset{˙}{\oplus} U))) \to (T P U) (y) \in {Base}_{W}$
38	7	adantr	$⊢ (φ \land (x \in {Base}_{Scalar (W)} \land y \in (T \underset{˙}{\oplus} U))) \to U \in L$
39	27 1	lssss	$⊢ U \in L \to U \subseteq {Base}_{W}$
40	38 39	syl	$⊢ (φ \land (x \in {Base}_{Scalar (W)} \land y \in (T \underset{˙}{\oplus} U))) \to U \subseteq {Base}_{W}$
41	9 2 3 10 30 31 32 33 4	pj2f	$⊢ (φ \land (x \in {Base}_{Scalar (W)} \land y \in (T \underset{˙}{\oplus} U))) \to (U P T) : T \underset{˙}{\oplus} U ⟶ U$
42	41 35	ffvelcdmd	$⊢ (φ \land (x \in {Base}_{Scalar (W)} \land y \in (T \underset{˙}{\oplus} U))) \to (U P T) (y) \in U$
43	40 42	sseldd	$⊢ (φ \land (x \in {Base}_{Scalar (W)} \land y \in (T \underset{˙}{\oplus} U))) \to (U P T) (y) \in {Base}_{W}$
44		eqid	$⊢ \cdot_{W} = \cdot_{W}$
45		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
46	27 9 19 44 45	lmodvsdi	$⊢ (W \in LMod \land (x \in {Base}_{Scalar (W)} \land (T P U) (y) \in {Base}_{W} \land (U P T) (y) \in {Base}_{W})) \to x \cdot_{W} ((T P U) (y) +_{W} (U P T) (y)) = (x \cdot_{W} (T P U) (y)) +_{W} (x \cdot_{W} (U P T) (y))$
47	24 25 37 43 46	syl13anc	$⊢ (φ \land (x \in {Base}_{Scalar (W)} \land y \in (T \underset{˙}{\oplus} U))) \to x \cdot_{W} ((T P U) (y) +_{W} (U P T) (y)) = (x \cdot_{W} (T P U) (y)) +_{W} (x \cdot_{W} (U P T) (y))$
48	23 47	eqtrd	$⊢ (φ \land (x \in {Base}_{Scalar (W)} \land y \in (T \underset{˙}{\oplus} U))) \to x \cdot_{W} y = (x \cdot_{W} (T P U) (y)) +_{W} (x \cdot_{W} (U P T) (y))$
49	1 2	lsmcl	$⊢ (W \in LMod \land T \in L \land U \in L) \to T \underset{˙}{\oplus} U \in L$
50	5 6 7 49	syl3anc	$⊢ φ \to T \underset{˙}{\oplus} U \in L$
51	50	adantr	$⊢ (φ \land (x \in {Base}_{Scalar (W)} \land y \in (T \underset{˙}{\oplus} U))) \to T \underset{˙}{\oplus} U \in L$
52	19 44 45 1	lssvscl	$⊢ ((W \in LMod \land T \underset{˙}{\oplus} U \in L) \land (x \in {Base}_{Scalar (W)} \land y \in (T \underset{˙}{\oplus} U))) \to x \cdot_{W} y \in (T \underset{˙}{\oplus} U)$
53	24 51 25 35 52	syl22anc	$⊢ (φ \land (x \in {Base}_{Scalar (W)} \land y \in (T \underset{˙}{\oplus} U))) \to x \cdot_{W} y \in (T \underset{˙}{\oplus} U)$
54	19 44 45 1	lssvscl	$⊢ ((W \in LMod \land T \in L) \land (x \in {Base}_{Scalar (W)} \land (T P U) (y) \in T)) \to x \cdot_{W} (T P U) (y) \in T$
55	24 26 25 36 54	syl22anc	$⊢ (φ \land (x \in {Base}_{Scalar (W)} \land y \in (T \underset{˙}{\oplus} U))) \to x \cdot_{W} (T P U) (y) \in T$
56	19 44 45 1	lssvscl	$⊢ ((W \in LMod \land U \in L) \land (x \in {Base}_{Scalar (W)} \land (U P T) (y) \in U)) \to x \cdot_{W} (U P T) (y) \in U$
57	24 38 25 42 56	syl22anc	$⊢ (φ \land (x \in {Base}_{Scalar (W)} \land y \in (T \underset{˙}{\oplus} U))) \to x \cdot_{W} (U P T) (y) \in U$
58	9 2 3 10 30 31 32 33 4 53 55 57	pj1eq	$⊢ (φ \land (x \in {Base}_{Scalar (W)} \land y \in (T \underset{˙}{\oplus} U))) \to (x \cdot_{W} y = (x \cdot_{W} (T P U) (y)) +_{W} (x \cdot_{W} (U P T) (y)) \leftrightarrow ((T P U) (x \cdot_{W} y) = x \cdot_{W} (T P U) (y) \land (U P T) (x \cdot_{W} y) = x \cdot_{W} (U P T) (y)))$
59	48 58	mpbid	$⊢ (φ \land (x \in {Base}_{Scalar (W)} \land y \in (T \underset{˙}{\oplus} U))) \to ((T P U) (x \cdot_{W} y) = x \cdot_{W} (T P U) (y) \land (U P T) (x \cdot_{W} y) = x \cdot_{W} (U P T) (y))$
60	59	simpld	$⊢ (φ \land (x \in {Base}_{Scalar (W)} \land y \in (T \underset{˙}{\oplus} U))) \to (T P U) (x \cdot_{W} y) = x \cdot_{W} (T P U) (y)$
61	60	ralrimivva	$⊢ φ \to \forall x \in {Base}_{Scalar (W)} \forall y \in (T \underset{˙}{\oplus} U) (T P U) (x \cdot_{W} y) = x \cdot_{W} (T P U) (y)$
62	12 50	sseldd	$⊢ φ \to T \underset{˙}{\oplus} U \in SubGrp (W)$
63		eqid	$⊢ W ↾_{𝑠} (T \underset{˙}{\oplus} U) = W ↾_{𝑠} (T \underset{˙}{\oplus} U)$
64	63	subgbas	$⊢ T \underset{˙}{\oplus} U \in SubGrp (W) \to T \underset{˙}{\oplus} U = {Base}_{(W ↾_{𝑠} (T \underset{˙}{\oplus} U))}$
65	62 64	syl	$⊢ φ \to T \underset{˙}{\oplus} U = {Base}_{(W ↾_{𝑠} (T \underset{˙}{\oplus} U))}$
66	65	raleqdv	$⊢ φ \to (\forall y \in (T \underset{˙}{\oplus} U) (T P U) (x \cdot_{W} y) = x \cdot_{W} (T P U) (y) \leftrightarrow \forall y \in {Base}_{(W ↾_{𝑠} (T \underset{˙}{\oplus} U))} (T P U) (x \cdot_{W} y) = x \cdot_{W} (T P U) (y))$
67	66	ralbidv	$⊢ φ \to (\forall x \in {Base}_{Scalar (W)} \forall y \in (T \underset{˙}{\oplus} U) (T P U) (x \cdot_{W} y) = x \cdot_{W} (T P U) (y) \leftrightarrow \forall x \in {Base}_{Scalar (W)} \forall y \in {Base}_{(W ↾_{𝑠} (T \underset{˙}{\oplus} U))} (T P U) (x \cdot_{W} y) = x \cdot_{W} (T P U) (y))$
68	61 67	mpbid	$⊢ φ \to \forall x \in {Base}_{Scalar (W)} \forall y \in {Base}_{(W ↾_{𝑠} (T \underset{˙}{\oplus} U))} (T P U) (x \cdot_{W} y) = x \cdot_{W} (T P U) (y)$
69	63 1	lsslmod	$⊢ (W \in LMod \land T \underset{˙}{\oplus} U \in L) \to W ↾_{𝑠} (T \underset{˙}{\oplus} U) \in LMod$
70	5 50 69	syl2anc	$⊢ φ \to W ↾_{𝑠} (T \underset{˙}{\oplus} U) \in LMod$
71		ovex	$⊢ T \underset{˙}{\oplus} U \in V$
72	63 19	resssca	$⊢ T \underset{˙}{\oplus} U \in V \to Scalar (W) = Scalar (W ↾_{𝑠} (T \underset{˙}{\oplus} U))$
73	71 72	ax-mp	$⊢ Scalar (W) = Scalar (W ↾_{𝑠} (T \underset{˙}{\oplus} U))$
74		eqid	$⊢ {Base}_{(W ↾_{𝑠} (T \underset{˙}{\oplus} U))} = {Base}_{(W ↾_{𝑠} (T \underset{˙}{\oplus} U))}$
75	63 44	ressvsca	$⊢ T \underset{˙}{\oplus} U \in V \to \cdot_{W} = \cdot_{(W ↾_{𝑠} (T \underset{˙}{\oplus} U))}$
76	71 75	ax-mp	$⊢ \cdot_{W} = \cdot_{(W ↾_{𝑠} (T \underset{˙}{\oplus} U))}$
77	73 19 45 74 76 44	islmhm3	$⊢ (W ↾_{𝑠} (T \underset{˙}{\oplus} U) \in LMod \land W \in LMod) \to (T P U \in ((W ↾_{𝑠} (T \underset{˙}{\oplus} U)) LMHom W) \leftrightarrow (T P U \in ((W ↾_{𝑠} (T \underset{˙}{\oplus} U)) GrpHom W) \land Scalar (W) = Scalar (W) \land \forall x \in {Base}_{Scalar (W)} \forall y \in {Base}_{(W ↾_{𝑠} (T \underset{˙}{\oplus} U))} (T P U) (x \cdot_{W} y) = x \cdot_{W} (T P U) (y)))$
78	70 5 77	syl2anc	$⊢ φ \to (T P U \in ((W ↾_{𝑠} (T \underset{˙}{\oplus} U)) LMHom W) \leftrightarrow (T P U \in ((W ↾_{𝑠} (T \underset{˙}{\oplus} U)) GrpHom W) \land Scalar (W) = Scalar (W) \land \forall x \in {Base}_{Scalar (W)} \forall y \in {Base}_{(W ↾_{𝑠} (T \underset{˙}{\oplus} U))} (T P U) (x \cdot_{W} y) = x \cdot_{W} (T P U) (y)))$
79	18 20 68 78	mpbir3and	$⊢ φ \to T P U \in ((W ↾_{𝑠} (T \underset{˙}{\oplus} U)) LMHom W)$

Metamath Proof Explorer

Theorem pj1lmhm

Proof