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

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 ‘ 𝐷 ) ( 𝐺 ‘ 𝑣 ) ) · 𝑍 ) ) )