This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
pj1lmhm.s ⊢ ⊕ = ( LSSum ‘ 𝑊 )
pj1lmhm.z ⊢ 0 = ( 0g ‘ 𝑊 )
pj1lmhm.p ⊢ 𝑃 = ( proj1 ‘ 𝑊 )
pj1lmhm.1 ⊢ ( 𝜑 → 𝑊 ∈ LMod )
pj1lmhm.2 ⊢ ( 𝜑 → 𝑇 ∈ 𝐿 )
pj1lmhm.3 ⊢ ( 𝜑 → 𝑈 ∈ 𝐿 )
pj1lmhm.4 ⊢ ( 𝜑 → ( 𝑇 ∩ 𝑈 ) = { 0 } )
Assertion pj1lmhm ( 𝜑 → ( 𝑇 𝑃 𝑈 ) ∈ ( ( 𝑊 ↾s ( 𝑇 ⊕ 𝑈 ) ) LMHom 𝑊 ) )

Proof

Step Hyp Ref Expression
1 pj1lmhm.l ⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
2 pj1lmhm.s ⊢ ⊕ = ( LSSum ‘ 𝑊 )
3 pj1lmhm.z ⊢ 0 = ( 0g ‘ 𝑊 )
4 pj1lmhm.p ⊢ 𝑃 = ( proj1 ‘ 𝑊 )
5 pj1lmhm.1 ⊢ ( 𝜑 → 𝑊 ∈ LMod )
6 pj1lmhm.2 ⊢ ( 𝜑 → 𝑇 ∈ 𝐿 )
7 pj1lmhm.3 ⊢ ( 𝜑 → 𝑈 ∈ 𝐿 )
8 pj1lmhm.4 ⊢ ( 𝜑 → ( 𝑇 ∩ 𝑈 ) = { 0 } )
9 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
10 eqid ⊢ ( Cntz ‘ 𝑊 ) = ( Cntz ‘ 𝑊 )
11 1 lsssssubg ⊢ ( 𝑊 ∈ LMod → 𝐿 ⊆ ( SubGrp ‘ 𝑊 ) )
12 5 11 syl ⊢ ( 𝜑 → 𝐿 ⊆ ( SubGrp ‘ 𝑊 ) )
13 12 6 sseldd ⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝑊 ) )
14 12 7 sseldd ⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
15 lmodabl ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
16 5 15 syl ⊢ ( 𝜑 → 𝑊 ∈ Abel )
17 10 16 13 14 ablcntzd ⊢ ( 𝜑 → 𝑇 ⊆ ( ( Cntz ‘ 𝑊 ) ‘ 𝑈 ) )
18 9 2 3 10 13 14 8 17 4 pj1ghm ⊢ ( 𝜑 → ( 𝑇 𝑃 𝑈 ) ∈ ( ( 𝑊 ↾s ( 𝑇 ⊕ 𝑈 ) ) GrpHom 𝑊 ) )
19 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
20 19 a1i ⊢ ( 𝜑 → ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 ) )
21 9 2 3 10 13 14 8 17 4 pj1id ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ) → 𝑦 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑦 ) ( +g ‘ 𝑊 ) ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑦 ) ) )
22 21 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ) ) → 𝑦 = ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑦 ) ( +g ‘ 𝑊 ) ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑦 ) ) )
23 22 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑦 ) ( +g ‘ 𝑊 ) ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑦 ) ) ) )
24 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ) ) → 𝑊 ∈ LMod )
25 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ) ) → 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
26 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ) ) → 𝑇 ∈ 𝐿 )
27 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
28 27 1 lssss ⊢ ( 𝑇 ∈ 𝐿 → 𝑇 ⊆ ( Base ‘ 𝑊 ) )
29 26 28 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ) ) → 𝑇 ⊆ ( Base ‘ 𝑊 ) )
30 13 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ) ) → 𝑇 ∈ ( SubGrp ‘ 𝑊 ) )
31 14 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ) ) → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
32 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ) ) → ( 𝑇 ∩ 𝑈 ) = { 0 } )
33 17 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ) ) → 𝑇 ⊆ ( ( Cntz ‘ 𝑊 ) ‘ 𝑈 ) )
34 9 2 3 10 30 31 32 33 4 pj1f ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ) ) → ( 𝑇 𝑃 𝑈 ) : ( 𝑇 ⊕ 𝑈 ) ⟶ 𝑇 )
35 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ) ) → 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) )
36 34 35 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ) ) → ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑦 ) ∈ 𝑇 )
37 29 36 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ) ) → ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝑊 ) )
38 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ) ) → 𝑈 ∈ 𝐿 )
39 27 1 lssss ⊢ ( 𝑈 ∈ 𝐿 → 𝑈 ⊆ ( Base ‘ 𝑊 ) )
40 38 39 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ) ) → 𝑈 ⊆ ( Base ‘ 𝑊 ) )
41 9 2 3 10 30 31 32 33 4 pj2f ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ) ) → ( 𝑈 𝑃 𝑇 ) : ( 𝑇 ⊕ 𝑈 ) ⟶ 𝑈 )
42 41 35 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ) ) → ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑦 ) ∈ 𝑈 )
43 40 42 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ) ) → ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝑊 ) )
44 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
45 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
46 27 9 19 44 45 lmodvsdi ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝑊 ) ∧ ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑦 ) ( +g ‘ 𝑊 ) ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑦 ) ) ) = ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑦 ) ) ( +g ‘ 𝑊 ) ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑦 ) ) ) )
47 24 25 37 43 46 syl13anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑦 ) ( +g ‘ 𝑊 ) ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑦 ) ) ) = ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑦 ) ) ( +g ‘ 𝑊 ) ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑦 ) ) ) )
48 23 47 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) = ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑦 ) ) ( +g ‘ 𝑊 ) ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑦 ) ) ) )
49 1 2 lsmcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝐿 ∧ 𝑈 ∈ 𝐿 ) → ( 𝑇 ⊕ 𝑈 ) ∈ 𝐿 )
50 5 6 7 49 syl3anc ⊢ ( 𝜑 → ( 𝑇 ⊕ 𝑈 ) ∈ 𝐿 )
51 50 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ) ) → ( 𝑇 ⊕ 𝑈 ) ∈ 𝐿 )
52 19 44 45 1 lssvscl ⊢ ( ( ( 𝑊 ∈ LMod ∧ ( 𝑇 ⊕ 𝑈 ) ∈ 𝐿 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ ( 𝑇 ⊕ 𝑈 ) )
53 24 51 25 35 52 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ ( 𝑇 ⊕ 𝑈 ) )
54 19 44 45 1 lssvscl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝐿 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑦 ) ∈ 𝑇 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑦 ) ) ∈ 𝑇 )
55 24 26 25 36 54 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑦 ) ) ∈ 𝑇 )
56 19 44 45 1 lssvscl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑦 ) ∈ 𝑈 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑦 ) ) ∈ 𝑈 )
57 24 38 25 42 56 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑦 ) ) ∈ 𝑈 )
58 9 2 3 10 30 31 32 33 4 53 55 57 pj1eq ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) = ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑦 ) ) ( +g ‘ 𝑊 ) ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑦 ) ) ) ↔ ( ( ( 𝑇 𝑃 𝑈 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑦 ) ) ∧ ( ( 𝑈 𝑃 𝑇 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑦 ) ) ) ) )
59 48 58 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ) ) → ( ( ( 𝑇 𝑃 𝑈 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑦 ) ) ∧ ( ( 𝑈 𝑃 𝑇 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( ( 𝑈 𝑃 𝑇 ) ‘ 𝑦 ) ) ) )
60 59 simpld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ) ) → ( ( 𝑇 𝑃 𝑈 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑦 ) ) )
61 60 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ( ( 𝑇 𝑃 𝑈 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑦 ) ) )
62 12 50 sseldd ⊢ ( 𝜑 → ( 𝑇 ⊕ 𝑈 ) ∈ ( SubGrp ‘ 𝑊 ) )
63 eqid ⊢ ( 𝑊 ↾s ( 𝑇 ⊕ 𝑈 ) ) = ( 𝑊 ↾s ( 𝑇 ⊕ 𝑈 ) )
64 63 subgbas ⊢ ( ( 𝑇 ⊕ 𝑈 ) ∈ ( SubGrp ‘ 𝑊 ) → ( 𝑇 ⊕ 𝑈 ) = ( Base ‘ ( 𝑊 ↾s ( 𝑇 ⊕ 𝑈 ) ) ) )
65 62 64 syl ⊢ ( 𝜑 → ( 𝑇 ⊕ 𝑈 ) = ( Base ‘ ( 𝑊 ↾s ( 𝑇 ⊕ 𝑈 ) ) ) )
66 65 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ( ( 𝑇 𝑃 𝑈 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s ( 𝑇 ⊕ 𝑈 ) ) ) ( ( 𝑇 𝑃 𝑈 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑦 ) ) ) )
67 66 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ( ( 𝑇 𝑃 𝑈 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s ( 𝑇 ⊕ 𝑈 ) ) ) ( ( 𝑇 𝑃 𝑈 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑦 ) ) ) )
68 61 67 mpbid ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s ( 𝑇 ⊕ 𝑈 ) ) ) ( ( 𝑇 𝑃 𝑈 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑦 ) ) )
69 63 1 lsslmod ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑇 ⊕ 𝑈 ) ∈ 𝐿 ) → ( 𝑊 ↾s ( 𝑇 ⊕ 𝑈 ) ) ∈ LMod )
70 5 50 69 syl2anc ⊢ ( 𝜑 → ( 𝑊 ↾s ( 𝑇 ⊕ 𝑈 ) ) ∈ LMod )
71 ovex ⊢ ( 𝑇 ⊕ 𝑈 ) ∈ V
72 63 19 resssca ⊢ ( ( 𝑇 ⊕ 𝑈 ) ∈ V → ( Scalar ‘ 𝑊 ) = ( Scalar ‘ ( 𝑊 ↾s ( 𝑇 ⊕ 𝑈 ) ) ) )
73 71 72 ax-mp ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ ( 𝑊 ↾s ( 𝑇 ⊕ 𝑈 ) ) )
74 eqid ⊢ ( Base ‘ ( 𝑊 ↾s ( 𝑇 ⊕ 𝑈 ) ) ) = ( Base ‘ ( 𝑊 ↾s ( 𝑇 ⊕ 𝑈 ) ) )
75 63 44 ressvsca ⊢ ( ( 𝑇 ⊕ 𝑈 ) ∈ V → ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ ( 𝑊 ↾s ( 𝑇 ⊕ 𝑈 ) ) ) )
76 71 75 ax-mp ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ ( 𝑊 ↾s ( 𝑇 ⊕ 𝑈 ) ) )
77 73 19 45 74 76 44 islmhm3 ⊢ ( ( ( 𝑊 ↾s ( 𝑇 ⊕ 𝑈 ) ) ∈ LMod ∧ 𝑊 ∈ LMod ) → ( ( 𝑇 𝑃 𝑈 ) ∈ ( ( 𝑊 ↾s ( 𝑇 ⊕ 𝑈 ) ) LMHom 𝑊 ) ↔ ( ( 𝑇 𝑃 𝑈 ) ∈ ( ( 𝑊 ↾s ( 𝑇 ⊕ 𝑈 ) ) GrpHom 𝑊 ) ∧ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s ( 𝑇 ⊕ 𝑈 ) ) ) ( ( 𝑇 𝑃 𝑈 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑦 ) ) ) ) )
78 70 5 77 syl2anc ⊢ ( 𝜑 → ( ( 𝑇 𝑃 𝑈 ) ∈ ( ( 𝑊 ↾s ( 𝑇 ⊕ 𝑈 ) ) LMHom 𝑊 ) ↔ ( ( 𝑇 𝑃 𝑈 ) ∈ ( ( 𝑊 ↾s ( 𝑇 ⊕ 𝑈 ) ) GrpHom 𝑊 ) ∧ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝑊 ↾s ( 𝑇 ⊕ 𝑈 ) ) ) ( ( 𝑇 𝑃 𝑈 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( ( 𝑇 𝑃 𝑈 ) ‘ 𝑦 ) ) ) ) )
79 18 20 68 78 mpbir3and ⊢ ( 𝜑 → ( 𝑇 𝑃 𝑈 ) ∈ ( ( 𝑊 ↾s ( 𝑇 ⊕ 𝑈 ) ) LMHom 𝑊 ) )