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 = ( 0_g ‘ 𝐷 )
	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 = ( 0_g ‘ 𝐷 )
15		lshpkrlem.g	⊢ 𝐺 = ( 𝑥 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝐾 ∃ 𝑦 ∈ 𝑈 𝑥 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ) )
16		eqid	⊢ ( 0_g ‘ 𝑊 ) = ( 0_g ‘ 𝑊 )
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	⊢ ( 𝜑 → ( 𝑈 ∩ ( 𝑁 ‘ { 𝑍 } ) ) = { ( 0_g ‘ 𝑊 ) } )
34	18 33	syl	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → ( 𝑈 ∩ ( 𝑁 ‘ { 𝑍 } ) ) = { ( 0_g ‘ 𝑊 ) } )
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	⊢ ( 𝜑 → 𝑍 ≠ ( 0_g ‘ 𝑊 ) )
94	18 93	syl	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → 𝑍 ≠ ( 0_g ‘ 𝑊 ) )
95	1 13 11 12 16 19 58 79 29 94	lvecvscan2	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → ( ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) = ( ( ( 𝑙 ( ._r ‘ 𝐷 ) ( 𝐺 ‘ 𝑢 ) ) ( +_g ‘ 𝐷 ) ( 𝐺 ‘ 𝑣 ) ) · 𝑍 ) ↔ ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) = ( ( 𝑙 ( ._r ‘ 𝐷 ) ( 𝐺 ‘ 𝑢 ) ) ( +_g ‘ 𝐷 ) ( 𝐺 ‘ 𝑣 ) ) ) )
96	92 95	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ ( 𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈 ) ) ∧ ( 𝑢 = ( 𝑟 + ( ( 𝐺 ‘ 𝑢 ) · 𝑍 ) ) ∧ 𝑣 = ( 𝑠 + ( ( 𝐺 ‘ 𝑣 ) · 𝑍 ) ) ∧ ( ( 𝑙 · 𝑢 ) + 𝑣 ) = ( 𝑧 + ( ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) · 𝑍 ) ) ) ) → ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) = ( ( 𝑙 ( ._r ‘ 𝐷 ) ( 𝐺 ‘ 𝑢 ) ) ( +_g ‘ 𝐷 ) ( 𝐺 ‘ 𝑣 ) ) )

Metamath Proof Explorer

Theorem lshpkrlem5

Proof