Metamath Proof Explorer


Theorem lshpkrlem4

Description: Lemma for lshpkrex . Part of showing linearity of G . (Contributed by NM, 16-Jul-2014)

Ref Expression
Hypotheses lshpkrlem.v 𝑉 = ( Base ‘ 𝑊 )
lshpkrlem.a + = ( +g𝑊 )
lshpkrlem.n 𝑁 = ( LSpan ‘ 𝑊 )
lshpkrlem.p = ( LSSum ‘ 𝑊 )
lshpkrlem.h 𝐻 = ( LSHyp ‘ 𝑊 )
lshpkrlem.w ( 𝜑𝑊 ∈ LVec )
lshpkrlem.u ( 𝜑𝑈𝐻 )
lshpkrlem.z ( 𝜑𝑍𝑉 )
lshpkrlem.x ( 𝜑𝑋𝑉 )
lshpkrlem.e ( 𝜑 → ( 𝑈 ( 𝑁 ‘ { 𝑍 } ) ) = 𝑉 )
lshpkrlem.d 𝐷 = ( Scalar ‘ 𝑊 )
lshpkrlem.k 𝐾 = ( Base ‘ 𝐷 )
lshpkrlem.t · = ( ·𝑠𝑊 )
lshpkrlem.o 0 = ( 0g𝐷 )
lshpkrlem.g 𝐺 = ( 𝑥𝑉 ↦ ( 𝑘𝐾𝑦𝑈 𝑥 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ) )
Assertion lshpkrlem4 ( ( ( 𝜑𝑙𝐾𝑢𝑉 ) ∧ ( 𝑣𝑉𝑟𝑉𝑠𝑉 ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺𝑣 ) · 𝑍 ) ) ) ) → ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( ( ( 𝑙 · 𝑟 ) + 𝑠 ) + ( ( ( 𝑙 ( .r𝐷 ) ( 𝐺𝑢 ) ) ( +g𝐷 ) ( 𝐺𝑣 ) ) · 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 lshpkrlem.v 𝑉 = ( Base ‘ 𝑊 )
2 lshpkrlem.a + = ( +g𝑊 )
3 lshpkrlem.n 𝑁 = ( LSpan ‘ 𝑊 )
4 lshpkrlem.p = ( LSSum ‘ 𝑊 )
5 lshpkrlem.h 𝐻 = ( LSHyp ‘ 𝑊 )
6 lshpkrlem.w ( 𝜑𝑊 ∈ LVec )
7 lshpkrlem.u ( 𝜑𝑈𝐻 )
8 lshpkrlem.z ( 𝜑𝑍𝑉 )
9 lshpkrlem.x ( 𝜑𝑋𝑉 )
10 lshpkrlem.e ( 𝜑 → ( 𝑈 ( 𝑁 ‘ { 𝑍 } ) ) = 𝑉 )
11 lshpkrlem.d 𝐷 = ( Scalar ‘ 𝑊 )
12 lshpkrlem.k 𝐾 = ( Base ‘ 𝐷 )
13 lshpkrlem.t · = ( ·𝑠𝑊 )
14 lshpkrlem.o 0 = ( 0g𝐷 )
15 lshpkrlem.g 𝐺 = ( 𝑥𝑉 ↦ ( 𝑘𝐾𝑦𝑈 𝑥 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ) )
16 simp3l ( ( ( 𝜑𝑙𝐾𝑢𝑉 ) ∧ ( 𝑣𝑉𝑟𝑉𝑠𝑉 ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺𝑣 ) · 𝑍 ) ) ) ) → 𝑢 = ( 𝑟 + ( ( 𝐺𝑢 ) · 𝑍 ) ) )
17 16 oveq2d ( ( ( 𝜑𝑙𝐾𝑢𝑉 ) ∧ ( 𝑣𝑉𝑟𝑉𝑠𝑉 ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺𝑣 ) · 𝑍 ) ) ) ) → ( 𝑙 · 𝑢 ) = ( 𝑙 · ( 𝑟 + ( ( 𝐺𝑢 ) · 𝑍 ) ) ) )
18 simp3r ( ( ( 𝜑𝑙𝐾𝑢𝑉 ) ∧ ( 𝑣𝑉𝑟𝑉𝑠𝑉 ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺𝑣 ) · 𝑍 ) ) ) ) → 𝑣 = ( 𝑠 + ( ( 𝐺𝑣 ) · 𝑍 ) ) )
19 17 18 oveq12d ( ( ( 𝜑𝑙𝐾𝑢𝑉 ) ∧ ( 𝑣𝑉𝑟𝑉𝑠𝑉 ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺𝑣 ) · 𝑍 ) ) ) ) → ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( ( 𝑙 · ( 𝑟 + ( ( 𝐺𝑢 ) · 𝑍 ) ) ) + ( 𝑠 + ( ( 𝐺𝑣 ) · 𝑍 ) ) ) )
20 simpl1 ( ( ( 𝜑𝑙𝐾𝑢𝑉 ) ∧ ( 𝑣𝑉𝑟𝑉𝑠𝑉 ) ) → 𝜑 )
21 lveclmod ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
22 20 6 21 3syl ( ( ( 𝜑𝑙𝐾𝑢𝑉 ) ∧ ( 𝑣𝑉𝑟𝑉𝑠𝑉 ) ) → 𝑊 ∈ LMod )
23 simpl2 ( ( ( 𝜑𝑙𝐾𝑢𝑉 ) ∧ ( 𝑣𝑉𝑟𝑉𝑠𝑉 ) ) → 𝑙𝐾 )
24 simpr2 ( ( ( 𝜑𝑙𝐾𝑢𝑉 ) ∧ ( 𝑣𝑉𝑟𝑉𝑠𝑉 ) ) → 𝑟𝑉 )
25 simpl3 ( ( ( 𝜑𝑙𝐾𝑢𝑉 ) ∧ ( 𝑣𝑉𝑟𝑉𝑠𝑉 ) ) → 𝑢𝑉 )
26 6 adantr ( ( 𝜑𝑢𝑉 ) → 𝑊 ∈ LVec )
27 7 adantr ( ( 𝜑𝑢𝑉 ) → 𝑈𝐻 )
28 8 adantr ( ( 𝜑𝑢𝑉 ) → 𝑍𝑉 )
29 simpr ( ( 𝜑𝑢𝑉 ) → 𝑢𝑉 )
30 10 adantr ( ( 𝜑𝑢𝑉 ) → ( 𝑈 ( 𝑁 ‘ { 𝑍 } ) ) = 𝑉 )
31 1 2 3 4 5 26 27 28 29 30 11 12 13 14 15 lshpkrlem2 ( ( 𝜑𝑢𝑉 ) → ( 𝐺𝑢 ) ∈ 𝐾 )
32 20 25 31 syl2anc ( ( ( 𝜑𝑙𝐾𝑢𝑉 ) ∧ ( 𝑣𝑉𝑟𝑉𝑠𝑉 ) ) → ( 𝐺𝑢 ) ∈ 𝐾 )
33 20 8 syl ( ( ( 𝜑𝑙𝐾𝑢𝑉 ) ∧ ( 𝑣𝑉𝑟𝑉𝑠𝑉 ) ) → 𝑍𝑉 )
34 1 11 13 12 lmodvscl ( ( 𝑊 ∈ LMod ∧ ( 𝐺𝑢 ) ∈ 𝐾𝑍𝑉 ) → ( ( 𝐺𝑢 ) · 𝑍 ) ∈ 𝑉 )
35 22 32 33 34 syl3anc ( ( ( 𝜑𝑙𝐾𝑢𝑉 ) ∧ ( 𝑣𝑉𝑟𝑉𝑠𝑉 ) ) → ( ( 𝐺𝑢 ) · 𝑍 ) ∈ 𝑉 )
36 1 2 11 13 12 lmodvsdi ( ( 𝑊 ∈ LMod ∧ ( 𝑙𝐾𝑟𝑉 ∧ ( ( 𝐺𝑢 ) · 𝑍 ) ∈ 𝑉 ) ) → ( 𝑙 · ( 𝑟 + ( ( 𝐺𝑢 ) · 𝑍 ) ) ) = ( ( 𝑙 · 𝑟 ) + ( 𝑙 · ( ( 𝐺𝑢 ) · 𝑍 ) ) ) )
37 22 23 24 35 36 syl13anc ( ( ( 𝜑𝑙𝐾𝑢𝑉 ) ∧ ( 𝑣𝑉𝑟𝑉𝑠𝑉 ) ) → ( 𝑙 · ( 𝑟 + ( ( 𝐺𝑢 ) · 𝑍 ) ) ) = ( ( 𝑙 · 𝑟 ) + ( 𝑙 · ( ( 𝐺𝑢 ) · 𝑍 ) ) ) )
38 eqid ( .r𝐷 ) = ( .r𝐷 )
39 1 11 13 12 38 lmodvsass ( ( 𝑊 ∈ LMod ∧ ( 𝑙𝐾 ∧ ( 𝐺𝑢 ) ∈ 𝐾𝑍𝑉 ) ) → ( ( 𝑙 ( .r𝐷 ) ( 𝐺𝑢 ) ) · 𝑍 ) = ( 𝑙 · ( ( 𝐺𝑢 ) · 𝑍 ) ) )
40 22 23 32 33 39 syl13anc ( ( ( 𝜑𝑙𝐾𝑢𝑉 ) ∧ ( 𝑣𝑉𝑟𝑉𝑠𝑉 ) ) → ( ( 𝑙 ( .r𝐷 ) ( 𝐺𝑢 ) ) · 𝑍 ) = ( 𝑙 · ( ( 𝐺𝑢 ) · 𝑍 ) ) )
41 40 oveq2d ( ( ( 𝜑𝑙𝐾𝑢𝑉 ) ∧ ( 𝑣𝑉𝑟𝑉𝑠𝑉 ) ) → ( ( 𝑙 · 𝑟 ) + ( ( 𝑙 ( .r𝐷 ) ( 𝐺𝑢 ) ) · 𝑍 ) ) = ( ( 𝑙 · 𝑟 ) + ( 𝑙 · ( ( 𝐺𝑢 ) · 𝑍 ) ) ) )
42 37 41 eqtr4d ( ( ( 𝜑𝑙𝐾𝑢𝑉 ) ∧ ( 𝑣𝑉𝑟𝑉𝑠𝑉 ) ) → ( 𝑙 · ( 𝑟 + ( ( 𝐺𝑢 ) · 𝑍 ) ) ) = ( ( 𝑙 · 𝑟 ) + ( ( 𝑙 ( .r𝐷 ) ( 𝐺𝑢 ) ) · 𝑍 ) ) )
43 42 oveq1d ( ( ( 𝜑𝑙𝐾𝑢𝑉 ) ∧ ( 𝑣𝑉𝑟𝑉𝑠𝑉 ) ) → ( ( 𝑙 · ( 𝑟 + ( ( 𝐺𝑢 ) · 𝑍 ) ) ) + ( 𝑠 + ( ( 𝐺𝑣 ) · 𝑍 ) ) ) = ( ( ( 𝑙 · 𝑟 ) + ( ( 𝑙 ( .r𝐷 ) ( 𝐺𝑢 ) ) · 𝑍 ) ) + ( 𝑠 + ( ( 𝐺𝑣 ) · 𝑍 ) ) ) )
44 1 11 13 12 lmodvscl ( ( 𝑊 ∈ LMod ∧ 𝑙𝐾𝑟𝑉 ) → ( 𝑙 · 𝑟 ) ∈ 𝑉 )
45 22 23 24 44 syl3anc ( ( ( 𝜑𝑙𝐾𝑢𝑉 ) ∧ ( 𝑣𝑉𝑟𝑉𝑠𝑉 ) ) → ( 𝑙 · 𝑟 ) ∈ 𝑉 )
46 11 12 38 lmodmcl ( ( 𝑊 ∈ LMod ∧ 𝑙𝐾 ∧ ( 𝐺𝑢 ) ∈ 𝐾 ) → ( 𝑙 ( .r𝐷 ) ( 𝐺𝑢 ) ) ∈ 𝐾 )
47 22 23 32 46 syl3anc ( ( ( 𝜑𝑙𝐾𝑢𝑉 ) ∧ ( 𝑣𝑉𝑟𝑉𝑠𝑉 ) ) → ( 𝑙 ( .r𝐷 ) ( 𝐺𝑢 ) ) ∈ 𝐾 )
48 1 11 13 12 lmodvscl ( ( 𝑊 ∈ LMod ∧ ( 𝑙 ( .r𝐷 ) ( 𝐺𝑢 ) ) ∈ 𝐾𝑍𝑉 ) → ( ( 𝑙 ( .r𝐷 ) ( 𝐺𝑢 ) ) · 𝑍 ) ∈ 𝑉 )
49 22 47 33 48 syl3anc ( ( ( 𝜑𝑙𝐾𝑢𝑉 ) ∧ ( 𝑣𝑉𝑟𝑉𝑠𝑉 ) ) → ( ( 𝑙 ( .r𝐷 ) ( 𝐺𝑢 ) ) · 𝑍 ) ∈ 𝑉 )
50 simpr3 ( ( ( 𝜑𝑙𝐾𝑢𝑉 ) ∧ ( 𝑣𝑉𝑟𝑉𝑠𝑉 ) ) → 𝑠𝑉 )
51 simpr1 ( ( ( 𝜑𝑙𝐾𝑢𝑉 ) ∧ ( 𝑣𝑉𝑟𝑉𝑠𝑉 ) ) → 𝑣𝑉 )
52 6 adantr ( ( 𝜑𝑣𝑉 ) → 𝑊 ∈ LVec )
53 7 adantr ( ( 𝜑𝑣𝑉 ) → 𝑈𝐻 )
54 8 adantr ( ( 𝜑𝑣𝑉 ) → 𝑍𝑉 )
55 simpr ( ( 𝜑𝑣𝑉 ) → 𝑣𝑉 )
56 10 adantr ( ( 𝜑𝑣𝑉 ) → ( 𝑈 ( 𝑁 ‘ { 𝑍 } ) ) = 𝑉 )
57 1 2 3 4 5 52 53 54 55 56 11 12 13 14 15 lshpkrlem2 ( ( 𝜑𝑣𝑉 ) → ( 𝐺𝑣 ) ∈ 𝐾 )
58 20 51 57 syl2anc ( ( ( 𝜑𝑙𝐾𝑢𝑉 ) ∧ ( 𝑣𝑉𝑟𝑉𝑠𝑉 ) ) → ( 𝐺𝑣 ) ∈ 𝐾 )
59 1 11 13 12 lmodvscl ( ( 𝑊 ∈ LMod ∧ ( 𝐺𝑣 ) ∈ 𝐾𝑍𝑉 ) → ( ( 𝐺𝑣 ) · 𝑍 ) ∈ 𝑉 )
60 22 58 33 59 syl3anc ( ( ( 𝜑𝑙𝐾𝑢𝑉 ) ∧ ( 𝑣𝑉𝑟𝑉𝑠𝑉 ) ) → ( ( 𝐺𝑣 ) · 𝑍 ) ∈ 𝑉 )
61 1 2 lmod4 ( ( 𝑊 ∈ LMod ∧ ( ( 𝑙 · 𝑟 ) ∈ 𝑉 ∧ ( ( 𝑙 ( .r𝐷 ) ( 𝐺𝑢 ) ) · 𝑍 ) ∈ 𝑉 ) ∧ ( 𝑠𝑉 ∧ ( ( 𝐺𝑣 ) · 𝑍 ) ∈ 𝑉 ) ) → ( ( ( 𝑙 · 𝑟 ) + ( ( 𝑙 ( .r𝐷 ) ( 𝐺𝑢 ) ) · 𝑍 ) ) + ( 𝑠 + ( ( 𝐺𝑣 ) · 𝑍 ) ) ) = ( ( ( 𝑙 · 𝑟 ) + 𝑠 ) + ( ( ( 𝑙 ( .r𝐷 ) ( 𝐺𝑢 ) ) · 𝑍 ) + ( ( 𝐺𝑣 ) · 𝑍 ) ) ) )
62 22 45 49 50 60 61 syl122anc ( ( ( 𝜑𝑙𝐾𝑢𝑉 ) ∧ ( 𝑣𝑉𝑟𝑉𝑠𝑉 ) ) → ( ( ( 𝑙 · 𝑟 ) + ( ( 𝑙 ( .r𝐷 ) ( 𝐺𝑢 ) ) · 𝑍 ) ) + ( 𝑠 + ( ( 𝐺𝑣 ) · 𝑍 ) ) ) = ( ( ( 𝑙 · 𝑟 ) + 𝑠 ) + ( ( ( 𝑙 ( .r𝐷 ) ( 𝐺𝑢 ) ) · 𝑍 ) + ( ( 𝐺𝑣 ) · 𝑍 ) ) ) )
63 eqid ( +g𝐷 ) = ( +g𝐷 )
64 1 2 11 13 12 63 lmodvsdir ( ( 𝑊 ∈ LMod ∧ ( ( 𝑙 ( .r𝐷 ) ( 𝐺𝑢 ) ) ∈ 𝐾 ∧ ( 𝐺𝑣 ) ∈ 𝐾𝑍𝑉 ) ) → ( ( ( 𝑙 ( .r𝐷 ) ( 𝐺𝑢 ) ) ( +g𝐷 ) ( 𝐺𝑣 ) ) · 𝑍 ) = ( ( ( 𝑙 ( .r𝐷 ) ( 𝐺𝑢 ) ) · 𝑍 ) + ( ( 𝐺𝑣 ) · 𝑍 ) ) )
65 22 47 58 33 64 syl13anc ( ( ( 𝜑𝑙𝐾𝑢𝑉 ) ∧ ( 𝑣𝑉𝑟𝑉𝑠𝑉 ) ) → ( ( ( 𝑙 ( .r𝐷 ) ( 𝐺𝑢 ) ) ( +g𝐷 ) ( 𝐺𝑣 ) ) · 𝑍 ) = ( ( ( 𝑙 ( .r𝐷 ) ( 𝐺𝑢 ) ) · 𝑍 ) + ( ( 𝐺𝑣 ) · 𝑍 ) ) )
66 65 oveq2d ( ( ( 𝜑𝑙𝐾𝑢𝑉 ) ∧ ( 𝑣𝑉𝑟𝑉𝑠𝑉 ) ) → ( ( ( 𝑙 · 𝑟 ) + 𝑠 ) + ( ( ( 𝑙 ( .r𝐷 ) ( 𝐺𝑢 ) ) ( +g𝐷 ) ( 𝐺𝑣 ) ) · 𝑍 ) ) = ( ( ( 𝑙 · 𝑟 ) + 𝑠 ) + ( ( ( 𝑙 ( .r𝐷 ) ( 𝐺𝑢 ) ) · 𝑍 ) + ( ( 𝐺𝑣 ) · 𝑍 ) ) ) )
67 62 66 eqtr4d ( ( ( 𝜑𝑙𝐾𝑢𝑉 ) ∧ ( 𝑣𝑉𝑟𝑉𝑠𝑉 ) ) → ( ( ( 𝑙 · 𝑟 ) + ( ( 𝑙 ( .r𝐷 ) ( 𝐺𝑢 ) ) · 𝑍 ) ) + ( 𝑠 + ( ( 𝐺𝑣 ) · 𝑍 ) ) ) = ( ( ( 𝑙 · 𝑟 ) + 𝑠 ) + ( ( ( 𝑙 ( .r𝐷 ) ( 𝐺𝑢 ) ) ( +g𝐷 ) ( 𝐺𝑣 ) ) · 𝑍 ) ) )
68 43 67 eqtrd ( ( ( 𝜑𝑙𝐾𝑢𝑉 ) ∧ ( 𝑣𝑉𝑟𝑉𝑠𝑉 ) ) → ( ( 𝑙 · ( 𝑟 + ( ( 𝐺𝑢 ) · 𝑍 ) ) ) + ( 𝑠 + ( ( 𝐺𝑣 ) · 𝑍 ) ) ) = ( ( ( 𝑙 · 𝑟 ) + 𝑠 ) + ( ( ( 𝑙 ( .r𝐷 ) ( 𝐺𝑢 ) ) ( +g𝐷 ) ( 𝐺𝑣 ) ) · 𝑍 ) ) )
69 68 3adant3 ( ( ( 𝜑𝑙𝐾𝑢𝑉 ) ∧ ( 𝑣𝑉𝑟𝑉𝑠𝑉 ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺𝑣 ) · 𝑍 ) ) ) ) → ( ( 𝑙 · ( 𝑟 + ( ( 𝐺𝑢 ) · 𝑍 ) ) ) + ( 𝑠 + ( ( 𝐺𝑣 ) · 𝑍 ) ) ) = ( ( ( 𝑙 · 𝑟 ) + 𝑠 ) + ( ( ( 𝑙 ( .r𝐷 ) ( 𝐺𝑢 ) ) ( +g𝐷 ) ( 𝐺𝑣 ) ) · 𝑍 ) ) )
70 19 69 eqtrd ( ( ( 𝜑𝑙𝐾𝑢𝑉 ) ∧ ( 𝑣𝑉𝑟𝑉𝑠𝑉 ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺𝑣 ) · 𝑍 ) ) ) ) → ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( ( ( 𝑙 · 𝑟 ) + 𝑠 ) + ( ( ( 𝑙 ( .r𝐷 ) ( 𝐺𝑢 ) ) ( +g𝐷 ) ( 𝐺𝑣 ) ) · 𝑍 ) ) )