lshpkrlem5 - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > lshpkrlem5		Structured version Visualization version GIF version

Theorem lshpkrlem5 36865

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

**Hypotheses**
Ref	Expression
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**
Ref	Expression
lshpkrlem5	⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → (𝐺‘((𝑙 · 𝑢) + 𝑣)) = ((𝑙(._r‘𝐷)(𝐺‘𝑢))(+_g‘𝐷)(𝐺‘𝑣)))

Distinct variable groups: 𝑥,𝑘,𝑦, + 𝑘,𝐾,𝑥 0 ,𝑘 · ,𝑘,𝑥,𝑦 𝑈,𝑘,𝑥,𝑦 𝑥,𝑉 𝑘,𝑋,𝑥,𝑦 𝑘,𝑍,𝑥,𝑦 𝑧,𝑙, + 𝐺,𝑙,𝑧 𝐾,𝑙 𝑈,𝑙,𝑧 𝑋,𝑙,𝑧 𝑍,𝑙,𝑧,𝑘,𝑥,𝑦 · ,𝑙,𝑧 𝑢,𝑘,𝑣,𝑥,𝑦 Allowed substitution hints: 𝜑(𝑥,𝑦,𝑧,𝑣,𝑢,𝑘,𝑠,𝑟,𝑙) 𝐷(𝑥,𝑦,𝑧,𝑣,𝑢,𝑘,𝑠,𝑟,𝑙) + (𝑣,𝑢,𝑠,𝑟) ⊕ (𝑥,𝑦,𝑧,𝑣,𝑢,𝑘,𝑠,𝑟,𝑙) · (𝑣,𝑢,𝑠,𝑟) 𝑈(𝑣,𝑢,𝑠,𝑟) 𝐺(𝑥,𝑦,𝑣,𝑢,𝑘,𝑠,𝑟) 𝐻(𝑥,𝑦,𝑧,𝑣,𝑢,𝑘,𝑠,𝑟,𝑙) 𝐾(𝑦,𝑧,𝑣,𝑢,𝑠,𝑟) 𝑁(𝑥,𝑦,𝑧,𝑣,𝑢,𝑘,𝑠,𝑟,𝑙) 𝑉(𝑦,𝑧,𝑣,𝑢,𝑘,𝑠,𝑟,𝑙) 𝑊(𝑥,𝑦,𝑧,𝑣,𝑢,𝑘,𝑠,𝑟,𝑙) 𝑋(𝑣,𝑢,𝑠,𝑟) 0 (𝑥,𝑦,𝑧,𝑣,𝑢,𝑠,𝑟,𝑙) 𝑍(𝑣,𝑢,𝑠,𝑟)

**Proof of Theorem lshpkrlem5**
Step	Hyp	Ref	Expression
1		lshpkrlem.a	. . 3 ⊢ + = (+_g‘𝑊)
2		eqid 2737	. . 3 ⊢ (0_g‘𝑊) = (0_g‘𝑊)
3		eqid 2737	. . 3 ⊢ (Cntz‘𝑊) = (Cntz‘𝑊)
4		simp11 1205	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → 𝜑)
5		lshpkrlem.w	. . . . . . 7 ⊢ (𝜑 → 𝑊 ∈ LVec)
6	4, 5	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → 𝑊 ∈ LVec)
7		lveclmod 20143	. . . . . 6 ⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod)
8	6, 7	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → 𝑊 ∈ LMod)
9		eqid 2737	. . . . . 6 ⊢ (LSubSp‘𝑊) = (LSubSp‘𝑊)
10	9	lsssssubg 19995	. . . . 5 ⊢ (𝑊 ∈ LMod → (LSubSp‘𝑊) ⊆ (SubGrp‘𝑊))
11	8, 10	syl 17	. . . 4 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → (LSubSp‘𝑊) ⊆ (SubGrp‘𝑊))
12		lshpkrlem.h	. . . . . 6 ⊢ 𝐻 = (LSHyp‘𝑊)
13	5, 7	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑊 ∈ LMod)
14		lshpkrlem.u	. . . . . 6 ⊢ (𝜑 → 𝑈 ∈ 𝐻)
15	9, 12, 13, 14	lshplss 36732	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ (LSubSp‘𝑊))
16	4, 15	syl 17	. . . 4 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → 𝑈 ∈ (LSubSp‘𝑊))
17	11, 16	sseldd 3902	. . 3 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → 𝑈 ∈ (SubGrp‘𝑊))
18		lshpkrlem.z	. . . . . 6 ⊢ (𝜑 → 𝑍 ∈ 𝑉)
19	4, 18	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → 𝑍 ∈ 𝑉)
20		lshpkrlem.v	. . . . . 6 ⊢ 𝑉 = (Base‘𝑊)
21		lshpkrlem.n	. . . . . 6 ⊢ 𝑁 = (LSpan‘𝑊)
22	20, 9, 21	lspsncl 20014	. . . . 5 ⊢ ((𝑊 ∈ LMod ∧ 𝑍 ∈ 𝑉) → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑊))
23	8, 19, 22	syl2anc 587	. . . 4 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑊))
24	11, 23	sseldd 3902	. . 3 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → (𝑁‘{𝑍}) ∈ (SubGrp‘𝑊))
25		lshpkrlem.p	. . . . 5 ⊢ ⊕ = (LSSum‘𝑊)
26		lshpkrlem.e	. . . . 5 ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉)
27	20, 2, 21, 25, 12, 5, 14, 18, 26	lshpdisj 36738	. . . 4 ⊢ (𝜑 → (𝑈 ∩ (𝑁‘{𝑍})) = {(0_g‘𝑊)})
28	4, 27	syl 17	. . 3 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → (𝑈 ∩ (𝑁‘{𝑍})) = {(0_g‘𝑊)})
29		lmodabl 19946	. . . . 5 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Abel)
30	8, 29	syl 17	. . . 4 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → 𝑊 ∈ Abel)
31	3, 30, 17, 24	ablcntzd 19242	. . 3 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → 𝑈 ⊆ ((Cntz‘𝑊)‘(𝑁‘{𝑍})))
32		simp23r 1297	. . 3 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → 𝑧 ∈ 𝑈)
33		simp12 1206	. . . . 5 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → 𝑙 ∈ 𝐾)
34		simp22 1209	. . . . 5 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → 𝑟 ∈ 𝑈)
35		lshpkrlem.d	. . . . . 6 ⊢ 𝐷 = (Scalar‘𝑊)
36		lshpkrlem.t	. . . . . 6 ⊢ · = ( ·_𝑠 ‘𝑊)
37		lshpkrlem.k	. . . . . 6 ⊢ 𝐾 = (Base‘𝐷)
38	35, 36, 37, 9	lssvscl 19992	. . . . 5 ⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ (LSubSp‘𝑊)) ∧ (𝑙 ∈ 𝐾 ∧ 𝑟 ∈ 𝑈)) → (𝑙 · 𝑟) ∈ 𝑈)
39	8, 16, 33, 34, 38	syl22anc 839	. . . 4 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → (𝑙 · 𝑟) ∈ 𝑈)
40		simp23l 1296	. . . 4 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → 𝑠 ∈ 𝑈)
41	1, 9	lssvacl 19991	. . . 4 ⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ (LSubSp‘𝑊)) ∧ ((𝑙 · 𝑟) ∈ 𝑈 ∧ 𝑠 ∈ 𝑈)) → ((𝑙 · 𝑟) + 𝑠) ∈ 𝑈)
42	8, 16, 39, 40, 41	syl22anc 839	. . 3 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → ((𝑙 · 𝑟) + 𝑠) ∈ 𝑈)
43		simp13 1207	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → 𝑢 ∈ 𝑉)
44	20, 35, 36, 37	lmodvscl 19916	. . . . . . 7 ⊢ ((𝑊 ∈ LMod ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) → (𝑙 · 𝑢) ∈ 𝑉)
45	8, 33, 43, 44	syl3anc 1373	. . . . . 6 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → (𝑙 · 𝑢) ∈ 𝑉)
46		simp21 1208	. . . . . 6 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → 𝑣 ∈ 𝑉)
47	20, 1	lmodvacl 19913	. . . . . 6 ⊢ ((𝑊 ∈ LMod ∧ (𝑙 · 𝑢) ∈ 𝑉 ∧ 𝑣 ∈ 𝑉) → ((𝑙 · 𝑢) + 𝑣) ∈ 𝑉)
48	8, 45, 46, 47	syl3anc 1373	. . . . 5 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → ((𝑙 · 𝑢) + 𝑣) ∈ 𝑉)
49	5	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑙 · 𝑢) + 𝑣) ∈ 𝑉) → 𝑊 ∈ LVec)
50	14	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑙 · 𝑢) + 𝑣) ∈ 𝑉) → 𝑈 ∈ 𝐻)
51	18	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑙 · 𝑢) + 𝑣) ∈ 𝑉) → 𝑍 ∈ 𝑉)
52		simpr 488	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑙 · 𝑢) + 𝑣) ∈ 𝑉) → ((𝑙 · 𝑢) + 𝑣) ∈ 𝑉)
53	26	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑙 · 𝑢) + 𝑣) ∈ 𝑉) → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉)
54		lshpkrlem.o	. . . . . 6 ⊢ 0 = (0_g‘𝐷)
55		lshpkrlem.g	. . . . . 6 ⊢ 𝐺 = (𝑥 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑥 = (𝑦 + (𝑘 · 𝑍))))
56	20, 1, 21, 25, 12, 49, 50, 51, 52, 53, 35, 37, 36, 54, 55	lshpkrlem2 36862	. . . . 5 ⊢ ((𝜑 ∧ ((𝑙 · 𝑢) + 𝑣) ∈ 𝑉) → (𝐺‘((𝑙 · 𝑢) + 𝑣)) ∈ 𝐾)
57	4, 48, 56	syl2anc 587	. . . 4 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → (𝐺‘((𝑙 · 𝑢) + 𝑣)) ∈ 𝐾)
58	20, 36, 35, 37, 21, 8, 57, 19	lspsneli 20038	. . 3 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍) ∈ (𝑁‘{𝑍}))
59	5	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑉) → 𝑊 ∈ LVec)
60	14	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑉) → 𝑈 ∈ 𝐻)
61	18	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑉) → 𝑍 ∈ 𝑉)
62		simpr 488	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑉) → 𝑢 ∈ 𝑉)
63	26	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑉) → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉)
64	20, 1, 21, 25, 12, 59, 60, 61, 62, 63, 35, 37, 36, 54, 55	lshpkrlem2 36862	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑉) → (𝐺‘𝑢) ∈ 𝐾)
65	4, 43, 64	syl2anc 587	. . . . . 6 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → (𝐺‘𝑢) ∈ 𝐾)
66		eqid 2737	. . . . . . 7 ⊢ (._r‘𝐷) = (._r‘𝐷)
67	35, 37, 66	lmodmcl 19911	. . . . . 6 ⊢ ((𝑊 ∈ LMod ∧ 𝑙 ∈ 𝐾 ∧ (𝐺‘𝑢) ∈ 𝐾) → (𝑙(._r‘𝐷)(𝐺‘𝑢)) ∈ 𝐾)
68	8, 33, 65, 67	syl3anc 1373	. . . . 5 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → (𝑙(._r‘𝐷)(𝐺‘𝑢)) ∈ 𝐾)
69	5	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝑊 ∈ LVec)
70	14	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝑈 ∈ 𝐻)
71	18	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝑍 ∈ 𝑉)
72		simpr 488	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ 𝑉)
73	26	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉)
74	20, 1, 21, 25, 12, 69, 70, 71, 72, 73, 35, 37, 36, 54, 55	lshpkrlem2 36862	. . . . . 6 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → (𝐺‘𝑣) ∈ 𝐾)
75	4, 46, 74	syl2anc 587	. . . . 5 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → (𝐺‘𝑣) ∈ 𝐾)
76		eqid 2737	. . . . . 6 ⊢ (+_g‘𝐷) = (+_g‘𝐷)
77	35, 37, 76	lmodacl 19910	. . . . 5 ⊢ ((𝑊 ∈ LMod ∧ (𝑙(._r‘𝐷)(𝐺‘𝑢)) ∈ 𝐾 ∧ (𝐺‘𝑣) ∈ 𝐾) → ((𝑙(._r‘𝐷)(𝐺‘𝑢))(+_g‘𝐷)(𝐺‘𝑣)) ∈ 𝐾)
78	8, 68, 75, 77	syl3anc 1373	. . . 4 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → ((𝑙(._r‘𝐷)(𝐺‘𝑢))(+_g‘𝐷)(𝐺‘𝑣)) ∈ 𝐾)
79	20, 36, 35, 37, 21, 8, 78, 19	lspsneli 20038	. . 3 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → (((𝑙(._r‘𝐷)(𝐺‘𝑢))(+_g‘𝐷)(𝐺‘𝑣)) · 𝑍) ∈ (𝑁‘{𝑍}))
80		simp33 1213	. . . 4 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))
81		simp1 1138	. . . . 5 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → (𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉))
82	20, 9	lssel 19974	. . . . . 6 ⊢ ((𝑈 ∈ (LSubSp‘𝑊) ∧ 𝑟 ∈ 𝑈) → 𝑟 ∈ 𝑉)
83	16, 34, 82	syl2anc 587	. . . . 5 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → 𝑟 ∈ 𝑉)
84	20, 9	lssel 19974	. . . . . 6 ⊢ ((𝑈 ∈ (LSubSp‘𝑊) ∧ 𝑠 ∈ 𝑈) → 𝑠 ∈ 𝑉)
85	16, 40, 84	syl2anc 587	. . . . 5 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → 𝑠 ∈ 𝑉)
86		simp31 1211	. . . . 5 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → 𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)))
87		simp32 1212	. . . . 5 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)))
88		lshpkrlem.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
89	20, 1, 21, 25, 12, 5, 14, 18, 88, 26, 35, 37, 36, 54, 55	lshpkrlem4 36864	. . . . 5 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑉 ∧ 𝑠 ∈ 𝑉) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)))) → ((𝑙 · 𝑢) + 𝑣) = (((𝑙 · 𝑟) + 𝑠) + (((𝑙(._r‘𝐷)(𝐺‘𝑢))(+_g‘𝐷)(𝐺‘𝑣)) · 𝑍)))
90	81, 46, 83, 85, 86, 87, 89	syl132anc 1390	. . . 4 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → ((𝑙 · 𝑢) + 𝑣) = (((𝑙 · 𝑟) + 𝑠) + (((𝑙(._r‘𝐷)(𝐺‘𝑢))(+_g‘𝐷)(𝐺‘𝑣)) · 𝑍)))
91	80, 90	eqtr3d 2779	. . 3 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)) = (((𝑙 · 𝑟) + 𝑠) + (((𝑙(._r‘𝐷)(𝐺‘𝑢))(+_g‘𝐷)(𝐺‘𝑣)) · 𝑍)))
92	1, 2, 3, 17, 24, 28, 31, 32, 42, 58, 79, 91	subgdisj2 19082	. 2 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍) = (((𝑙(._r‘𝐷)(𝐺‘𝑢))(+_g‘𝐷)(𝐺‘𝑣)) · 𝑍))
93	20, 21, 25, 12, 2, 13, 14, 18, 26	lshpne0 36737	. . . 4 ⊢ (𝜑 → 𝑍 ≠ (0_g‘𝑊))
94	4, 93	syl 17	. . 3 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → 𝑍 ≠ (0_g‘𝑊))
95	20, 36, 35, 37, 2, 6, 57, 78, 19, 94	lvecvscan2 20149	. 2 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → (((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍) = (((𝑙(._r‘𝐷)(𝐺‘𝑢))(+_g‘𝐷)(𝐺‘𝑣)) · 𝑍) ↔ (𝐺‘((𝑙 · 𝑢) + 𝑣)) = ((𝑙(._r‘𝐷)(𝐺‘𝑢))(+_g‘𝐷)(𝐺‘𝑣))))
96	92, 95	mpbid 235	1 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → (𝐺‘((𝑙 · 𝑢) + 𝑣)) = ((𝑙(._r‘𝐷)(𝐺‘𝑢))(+_g‘𝐷)(𝐺‘𝑣)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1089 = wceq 1543 ∈ wcel 2110 ≠ wne 2940 ∃wrex 3062 ∩ cin 3865 ⊆ wss 3866 {csn 4541 ↦ cmpt 5135 ‘cfv 6380 ℩crio 7169 (class class class)co 7213 Basecbs 16760 +_gcplusg 16802 ._rcmulr 16803 Scalarcsca 16805 ·_𝑠 cvsca 16806 0_gc0g 16944 SubGrpcsubg 18537 Cntzccntz 18709 LSSumclsm 19023 Abelcabl 19171 LModclmod 19899 LSubSpclss 19968 LSpanclspn 20008 LVecclvec 20139 LSHypclsh 36726

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2708 ax-rep 5179 ax-sep 5192 ax-nul 5199 ax-pow 5258 ax-pr 5322 ax-un 7523 ax-cnex 10785 ax-resscn 10786 ax-1cn 10787 ax-icn 10788 ax-addcl 10789 ax-addrcl 10790 ax-mulcl 10791 ax-mulrcl 10792 ax-mulcom 10793 ax-addass 10794 ax-mulass 10795 ax-distr 10796 ax-i2m1 10797 ax-1ne0 10798 ax-1rid 10799 ax-rnegex 10800 ax-rrecex 10801 ax-cnre 10802 ax-pre-lttri 10803 ax-pre-lttrn 10804 ax-pre-ltadd 10805 ax-pre-mulgt0 10806

This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2886 df-ne 2941 df-nel 3047 df-ral 3066 df-rex 3067 df-reu 3068 df-rmo 3069 df-rab 3070 df-v 3410 df-sbc 3695 df-csb 3812 df-dif 3869 df-un 3871 df-in 3873 df-ss 3883 df-pss 3885 df-nul 4238 df-if 4440 df-pw 4515 df-sn 4542 df-pr 4544 df-tp 4546 df-op 4548 df-uni 4820 df-int 4860 df-iun 4906 df-br 5054 df-opab 5116 df-mpt 5136 df-tr 5162 df-id 5455 df-eprel 5460 df-po 5468 df-so 5469 df-fr 5509 df-we 5511 df-xp 5557 df-rel 5558 df-cnv 5559 df-co 5560 df-dm 5561 df-rn 5562 df-res 5563 df-ima 5564 df-pred 6160 df-ord 6216 df-on 6217 df-lim 6218 df-suc 6219 df-iota 6338 df-fun 6382 df-fn 6383 df-f 6384 df-f1 6385 df-fo 6386 df-f1o 6387 df-fv 6388 df-riota 7170 df-ov 7216 df-oprab 7217 df-mpo 7218 df-om 7645 df-1st 7761 df-2nd 7762 df-tpos 7968 df-wrecs 8047 df-recs 8108 df-rdg 8146 df-er 8391 df-en 8627 df-dom 8628 df-sdom 8629 df-pnf 10869 df-mnf 10870 df-xr 10871 df-ltxr 10872 df-le 10873 df-sub 11064 df-neg 11065 df-nn 11831 df-2 11893 df-3 11894 df-sets 16717 df-slot 16735 df-ndx 16745 df-base 16761 df-ress 16785 df-plusg 16815 df-mulr 16816 df-0g 16946 df-mgm 18114 df-sgrp 18163 df-mnd 18174 df-submnd 18219 df-grp 18368 df-minusg 18369 df-sbg 18370 df-subg 18540 df-cntz 18711 df-lsm 19025 df-cmn 19172 df-abl 19173 df-mgp 19505 df-ur 19517 df-ring 19564 df-oppr 19641 df-dvdsr 19659 df-unit 19660 df-invr 19690 df-drng 19769 df-lmod 19901 df-lss 19969 df-lsp 20009 df-lvec 20140 df-lshyp 36728

This theorem is referenced by: lshpkrlem6 36866

W3C validator