Metamath Proof Explorer

Theorem lshpkrlem5

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 lshpkrlem5 ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) = ( ( 𝑙 ( .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 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
17 eqid ⊢ ( Cntz ‘ 𝑊 ) = ( Cntz ‘ 𝑊 )
18 simp11 ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → 𝜑 )
19 18 6 syl ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → 𝑊 ∈ LVec )
20 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
21 19 20 syl ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → 𝑊 ∈ LMod )
22 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
23 22 lsssssubg ⊢ ( 𝑊 ∈ LMod → ( LSubSp ‘ 𝑊 ) ⊆ ( SubGrp ‘ 𝑊 ) )
24 21 23 syl ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → ( LSubSp ‘ 𝑊 ) ⊆ ( SubGrp ‘ 𝑊 ) )
25 6 20 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
26 22 5 25 7 lshplss ⊢ ( 𝜑 → 𝑈 ∈ ( LSubSp ‘ 𝑊 ) )
27 18 26 syl ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → 𝑈 ∈ ( LSubSp ‘ 𝑊 ) )
28 24 27 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
29 18 8 syl ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → 𝑍 ∈ 𝑉 )
30 1 22 3 lspsncl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑍 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑍 } ) ∈ ( LSubSp ‘ 𝑊 ) )
31 21 29 30 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → ( 𝑁 ‘ { 𝑍 } ) ∈ ( LSubSp ‘ 𝑊 ) )
32 24 31 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → ( 𝑁 ‘ { 𝑍 } ) ∈ ( SubGrp ‘ 𝑊 ) )
33 1 16 3 4 5 6 7 8 10 lshpdisj ⊢ ( 𝜑 → ( 𝑈 ∩ ( 𝑁 ‘ { 𝑍 } ) ) = { ( 0g ‘ 𝑊 ) } )
34 18 33 syl ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → ( 𝑈 ∩ ( 𝑁 ‘ { 𝑍 } ) ) = { ( 0g ‘ 𝑊 ) } )
35 lmodabl ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
36 21 35 syl ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → 𝑊 ∈ Abel )
37 17 36 28 32 ablcntzd ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → 𝑈 ⊆ ( ( Cntz ‘ 𝑊 ) ‘ ( 𝑁 ‘ { 𝑍 } ) ) )
38 simp23r ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → 𝑧 ∈ 𝑈 )
39 simp12 ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → 𝑙 ∈ 𝐾 )
40 simp22 ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → 𝑟 ∈ 𝑈 )
41 11 13 12 22 lssvscl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) ∧ ( 𝑙 ∈ 𝐾 ∧ 𝑟 ∈ 𝑈 ) ) → ( 𝑙 · 𝑟 ) ∈ 𝑈 )
42 21 27 39 40 41 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → ( 𝑙 · 𝑟 ) ∈ 𝑈 )
43 simp23l ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → 𝑠 ∈ 𝑈 )
44 2 22 lssvacl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ) ∧ ( ( 𝑙 · 𝑟 ) ∈ 𝑈 ∧ 𝑠 ∈ 𝑈 ) ) → ( ( 𝑙 · 𝑟 ) + 𝑠 ) ∈ 𝑈 )
45 21 27 42 43 44 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → ( ( 𝑙 · 𝑟 ) + 𝑠 ) ∈ 𝑈 )
46 simp13 ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → 𝑢 ∈ 𝑉 )
47 1 11 13 12 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) → ( 𝑙 · 𝑢 ) ∈ 𝑉 )
48 21 39 46 47 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → ( 𝑙 · 𝑢 ) ∈ 𝑉 )
49 simp21 ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → 𝑣 ∈ 𝑉 )
50 1 2 lmodvacl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑙 · 𝑢 ) ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝑙 · 𝑢 ) + 𝑣 ) ∈ 𝑉 )
51 21 48 49 50 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → ( ( 𝑙 · 𝑢 ) + 𝑣 ) ∈ 𝑉 )
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 18 51 57 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) ∈ 𝐾 )
59 1 13 11 12 3 21 58 29 ellspsni ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ∈ ( 𝑁 ‘ { 𝑍 } ) )
60 6 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑉 ) → 𝑊 ∈ LVec )
61 7 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑉 ) → 𝑈 ∈ 𝐻 )
62 8 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑉 ) → 𝑍 ∈ 𝑉 )
63 simpr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑉 ) → 𝑢 ∈ 𝑉 )
64 10 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑉 ) → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑍 } ) ) = 𝑉 )
65 1 2 3 4 5 60 61 62 63 64 11 12 13 14 15 lshpkrlem2 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑢 ) ∈ 𝐾 )
66 18 46 65 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → ( 𝐺 ‘ 𝑢 ) ∈ 𝐾 )
67 eqid ⊢ ( .r ‘ 𝐷 ) = ( .r ‘ 𝐷 )
68 11 12 67 lmodmcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑙 ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑢 ) ∈ 𝐾 ) → ( 𝑙 ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑢 ) ) ∈ 𝐾 )
69 21 39 66 68 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → ( 𝑙 ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑢 ) ) ∈ 𝐾 )
70 6 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → 𝑊 ∈ LVec )
71 7 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → 𝑈 ∈ 𝐻 )
72 8 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → 𝑍 ∈ 𝑉 )
73 simpr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ 𝑉 )
74 10 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑍 } ) ) = 𝑉 )
75 1 2 3 4 5 70 71 72 73 74 11 12 13 14 15 lshpkrlem2 ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑣 ) ∈ 𝐾 )
76 18 49 75 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → ( 𝐺 ‘ 𝑣 ) ∈ 𝐾 )
77 eqid ⊢ ( +g ‘ 𝐷 ) = ( +g ‘ 𝐷 )
78 11 12 77 lmodacl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑙 ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑢 ) ) ∈ 𝐾 ∧ ( 𝐺 ‘ 𝑣 ) ∈ 𝐾 ) → ( ( 𝑙 ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑢 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑣 ) ) ∈ 𝐾 )
79 21 69 76 78 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → ( ( 𝑙 ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑢 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑣 ) ) ∈ 𝐾 )
80 1 13 11 12 3 21 79 29 ellspsni ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → ( ( ( 𝑙 ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑢 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑣 ) ) · 𝑍 ) ∈ ( 𝑁 ‘ { 𝑍 } ) )
81 simp33 ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) )
82 simp1 ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) )
83 1 22 lssel ⊢ ( ( 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑟 ∈ 𝑈 ) → 𝑟 ∈ 𝑉 )
84 27 40 83 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → 𝑟 ∈ 𝑉 )
85 1 22 lssel ⊢ ( ( 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑠 ∈ 𝑈 ) → 𝑠 ∈ 𝑉 )
86 27 43 85 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → 𝑠 ∈ 𝑉 )
87 simp31 ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) )
88 simp32 ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) )
89 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 lshpkrlem4 ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑉 ∧ 𝑠 ∈ 𝑉 ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ) ) → ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( ( ( 𝑙 · 𝑟 ) + 𝑠 ) + ( ( ( 𝑙 ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑢 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑣 ) ) · 𝑍 ) ) )
90 82 49 84 86 87 88 89 syl132anc ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( ( ( 𝑙 · 𝑟 ) + 𝑠 ) + ( ( ( 𝑙 ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑢 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑣 ) ) · 𝑍 ) ) )
91 81 90 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) = ( ( ( 𝑙 · 𝑟 ) + 𝑠 ) + ( ( ( 𝑙 ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑢 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑣 ) ) · 𝑍 ) ) )
92 2 16 17 28 32 34 37 38 45 59 80 91 subgdisj2 ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) = ( ( ( 𝑙 ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑢 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑣 ) ) · 𝑍 ) )
93 1 3 4 5 16 25 7 8 10 lshpne0 ⊢ ( 𝜑 → 𝑍 ≠ ( 0g ‘ 𝑊 ) )
94 18 93 syl ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → 𝑍 ≠ ( 0g ‘ 𝑊 ) )
95 1 13 11 12 16 19 58 79 29 94 lvecvscan2 ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → ( ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) = ( ( ( 𝑙 ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑢 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑣 ) ) · 𝑍 ) ↔ ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) = ( ( 𝑙 ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑢 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑣 ) ) ) )
96 92 95 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) = ( ( 𝑙 ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑢 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑣 ) ) )