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

Metamath Proof Explorer

Theorem lshpkrlem6

Description: Lemma for lshpkrex . Show linearlity of G . (Contributed by NM, 17-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 lshpkrlem6 ( ( 𝜑 ∧ ( 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) = ( ( 𝑙 ( .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 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) → 𝑊 ∈ LVec )
17 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) → 𝑈 ∈ 𝐻 )
18 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) → 𝑍 ∈ 𝑉 )
19 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) → 𝑢 ∈ 𝑉 )
20 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑍 } ) ) = 𝑉 )
21 1 2 3 4 5 16 17 18 19 20 11 12 13 14 15 lshpkrlem3 ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) → ∃ 𝑟 ∈ 𝑈 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) )
22 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) → 𝑣 ∈ 𝑉 )
23 1 2 3 4 5 16 17 18 22 20 11 12 13 14 15 lshpkrlem3 ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) → ∃ 𝑠 ∈ 𝑈 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) )
24 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
25 16 24 syl ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) → 𝑊 ∈ LMod )
26 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) → 𝑙 ∈ 𝐾 )
27 1 11 13 12 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) → ( 𝑙 · 𝑢 ) ∈ 𝑉 )
28 25 26 19 27 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) → ( 𝑙 · 𝑢 ) ∈ 𝑉 )
29 1 2 lmodvacl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑙 · 𝑢 ) ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝑙 · 𝑢 ) + 𝑣 ) ∈ 𝑉 )
30 25 28 22 29 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) → ( ( 𝑙 · 𝑢 ) + 𝑣 ) ∈ 𝑉 )
31 1 2 3 4 5 16 17 18 30 20 11 12 13 14 15 lshpkrlem3 ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) → ∃ 𝑧 ∈ 𝑈 ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) )
32 3reeanv ⊢ ( ∃ 𝑟 ∈ 𝑈 ∃ 𝑠 ∈ 𝑈 ∃ 𝑧 ∈ 𝑈 ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ↔ ( ∃ 𝑟 ∈ 𝑈 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ ∃ 𝑠 ∈ 𝑈 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ∃ 𝑧 ∈ 𝑈 ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) )
33 simp1l ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) ∧ ( ( 𝑟 ∈ 𝑈 ∧ 𝑠 ∈ 𝑈 ) ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → 𝜑 )
34 simp1r1 ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) ∧ ( ( 𝑟 ∈ 𝑈 ∧ 𝑠 ∈ 𝑈 ) ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → 𝑙 ∈ 𝐾 )
35 simp1r2 ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) ∧ ( ( 𝑟 ∈ 𝑈 ∧ 𝑠 ∈ 𝑈 ) ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → 𝑢 ∈ 𝑉 )
36 simp1r3 ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) ∧ ( ( 𝑟 ∈ 𝑈 ∧ 𝑠 ∈ 𝑈 ) ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → 𝑣 ∈ 𝑉 )
37 simp2ll ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) ∧ ( ( 𝑟 ∈ 𝑈 ∧ 𝑠 ∈ 𝑈 ) ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → 𝑟 ∈ 𝑈 )
38 simp2lr ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) ∧ ( ( 𝑟 ∈ 𝑈 ∧ 𝑠 ∈ 𝑈 ) ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → 𝑠 ∈ 𝑈 )
39 simp2r ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) ∧ ( ( 𝑟 ∈ 𝑈 ∧ 𝑠 ∈ 𝑈 ) ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → 𝑧 ∈ 𝑈 )
40 38 39 jca ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) ∧ ( ( 𝑟 ∈ 𝑈 ∧ 𝑠 ∈ 𝑈 ) ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) )
41 simp31 ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) ∧ ( ( 𝑟 ∈ 𝑈 ∧ 𝑠 ∈ 𝑈 ) ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) )
42 simp32 ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) ∧ ( ( 𝑟 ∈ 𝑈 ∧ 𝑠 ∈ 𝑈 ) ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) )
43 simp33 ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) ∧ ( ( 𝑟 ∈ 𝑈 ∧ 𝑠 ∈ 𝑈 ) ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) )
44 1 2 3 4 5 6 7 8 8 10 11 12 13 14 15 lshpkrlem5 ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) = ( ( 𝑙 ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑢 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑣 ) ) )
45 33 34 35 36 37 40 41 42 43 44 syl333anc ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) ∧ ( ( 𝑟 ∈ 𝑈 ∧ 𝑠 ∈ 𝑈 ) ∧ 𝑧 ∈ 𝑈 ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) = ( ( 𝑙 ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑢 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑣 ) ) )
46 45 3exp ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) → ( ( ( 𝑟 ∈ 𝑈 ∧ 𝑠 ∈ 𝑈 ) ∧ 𝑧 ∈ 𝑈 ) → ( ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) → ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) = ( ( 𝑙 ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑢 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑣 ) ) ) ) )
47 46 expdimp ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) ∧ ( 𝑟 ∈ 𝑈 ∧ 𝑠 ∈ 𝑈 ) ) → ( 𝑧 ∈ 𝑈 → ( ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) → ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) = ( ( 𝑙 ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑢 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑣 ) ) ) ) )
48 47 rexlimdv ⊢ ( ( ( 𝜑 ∧ ( 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) ∧ ( 𝑟 ∈ 𝑈 ∧ 𝑠 ∈ 𝑈 ) ) → ( ∃ 𝑧 ∈ 𝑈 ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) → ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) = ( ( 𝑙 ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑢 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑣 ) ) ) )
49 48 rexlimdvva ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) → ( ∃ 𝑟 ∈ 𝑈 ∃ 𝑠 ∈ 𝑈 ∃ 𝑧 ∈ 𝑈 ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) → ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) = ( ( 𝑙 ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑢 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑣 ) ) ) )
50 32 49 biimtrrid ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) → ( ( ∃ 𝑟 ∈ 𝑈 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ ∃ 𝑠 ∈ 𝑈 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ∃ 𝑧 ∈ 𝑈 ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) → ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) = ( ( 𝑙 ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑢 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑣 ) ) ) )
51 21 23 31 50 mp3and ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) = ( ( 𝑙 ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑢 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑣 ) ) )