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 39100

Description: Lemma for lshpkrex 39104. 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 2729	. . 3 ⊢ (0_g‘𝑊) = (0_g‘𝑊)
3		eqid 2729	. . 3 ⊢ (Cntz‘𝑊) = (Cntz‘𝑊)
4		simp11 1204	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → 𝜑)
5		lshpkrlem.w	. . . . . . 7 ⊢ (𝜑 → 𝑊 ∈ LVec)
6	4, 5	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → 𝑊 ∈ LVec)
7		lveclmod 21045	. . . . . 6 ⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod)
8	6, 7	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → 𝑊 ∈ LMod)
9		eqid 2729	. . . . . 6 ⊢ (LSubSp‘𝑊) = (LSubSp‘𝑊)
10	9	lsssssubg 20896	. . . . 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 38967	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ (LSubSp‘𝑊))
16	4, 15	syl 17	. . . 4 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → 𝑈 ∈ (LSubSp‘𝑊))
17	11, 16	sseldd 3944	. . 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 20915	. . . . 5 ⊢ ((𝑊 ∈ LMod ∧ 𝑍 ∈ 𝑉) → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑊))
23	8, 19, 22	syl2anc 584	. . . 4 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑊))
24	11, 23	sseldd 3944	. . 3 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → (𝑁‘{𝑍}) ∈ (SubGrp‘𝑊))
25		lshpkrlem.p	. . . . 5 ⊢ ⊕ = (LSSum‘𝑊)
26		lshpkrlem.e	. . . . 5 ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉)
27	20, 2, 21, 25, 12, 5, 14, 18, 26	lshpdisj 38973	. . . 4 ⊢ (𝜑 → (𝑈 ∩ (𝑁‘{𝑍})) = {(0_g‘𝑊)})
28	4, 27	syl 17	. . 3 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → (𝑈 ∩ (𝑁‘{𝑍})) = {(0_g‘𝑊)})
29		lmodabl 20847	. . . . 5 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Abel)
30	8, 29	syl 17	. . . 4 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → 𝑊 ∈ Abel)
31	3, 30, 17, 24	ablcntzd 19771	. . 3 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → 𝑈 ⊆ ((Cntz‘𝑊)‘(𝑁‘{𝑍})))
32		simp23r 1296	. . 3 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → 𝑧 ∈ 𝑈)
33		simp12 1205	. . . . 5 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → 𝑙 ∈ 𝐾)
34		simp22 1208	. . . . 5 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → 𝑟 ∈ 𝑈)
35		lshpkrlem.d	. . . . . 6 ⊢ 𝐷 = (Scalar‘𝑊)
36		lshpkrlem.t	. . . . . 6 ⊢ · = ( ·_𝑠 ‘𝑊)
37		lshpkrlem.k	. . . . . 6 ⊢ 𝐾 = (Base‘𝐷)
38	35, 36, 37, 9	lssvscl 20893	. . . . 5 ⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ (LSubSp‘𝑊)) ∧ (𝑙 ∈ 𝐾 ∧ 𝑟 ∈ 𝑈)) → (𝑙 · 𝑟) ∈ 𝑈)
39	8, 16, 33, 34, 38	syl22anc 838	. . . 4 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → (𝑙 · 𝑟) ∈ 𝑈)
40		simp23l 1295	. . . 4 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → 𝑠 ∈ 𝑈)
41	1, 9	lssvacl 20881	. . . 4 ⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ (LSubSp‘𝑊)) ∧ ((𝑙 · 𝑟) ∈ 𝑈 ∧ 𝑠 ∈ 𝑈)) → ((𝑙 · 𝑟) + 𝑠) ∈ 𝑈)
42	8, 16, 39, 40, 41	syl22anc 838	. . 3 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → ((𝑙 · 𝑟) + 𝑠) ∈ 𝑈)
43		simp13 1206	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → 𝑢 ∈ 𝑉)
44	20, 35, 36, 37	lmodvscl 20816	. . . . . . 7 ⊢ ((𝑊 ∈ LMod ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) → (𝑙 · 𝑢) ∈ 𝑉)
45	8, 33, 43, 44	syl3anc 1373	. . . . . 6 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → (𝑙 · 𝑢) ∈ 𝑉)
46		simp21 1207	. . . . . 6 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → 𝑣 ∈ 𝑉)
47	20, 1	lmodvacl 20813	. . . . . 6 ⊢ ((𝑊 ∈ LMod ∧ (𝑙 · 𝑢) ∈ 𝑉 ∧ 𝑣 ∈ 𝑉) → ((𝑙 · 𝑢) + 𝑣) ∈ 𝑉)
48	8, 45, 46, 47	syl3anc 1373	. . . . 5 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → ((𝑙 · 𝑢) + 𝑣) ∈ 𝑉)
49	5	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑙 · 𝑢) + 𝑣) ∈ 𝑉) → 𝑊 ∈ LVec)
50	14	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑙 · 𝑢) + 𝑣) ∈ 𝑉) → 𝑈 ∈ 𝐻)
51	18	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑙 · 𝑢) + 𝑣) ∈ 𝑉) → 𝑍 ∈ 𝑉)
52		simpr 484	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑙 · 𝑢) + 𝑣) ∈ 𝑉) → ((𝑙 · 𝑢) + 𝑣) ∈ 𝑉)
53	26	adantr 480	. . . . . 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 39097	. . . . 5 ⊢ ((𝜑 ∧ ((𝑙 · 𝑢) + 𝑣) ∈ 𝑉) → (𝐺‘((𝑙 · 𝑢) + 𝑣)) ∈ 𝐾)
57	4, 48, 56	syl2anc 584	. . . 4 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → (𝐺‘((𝑙 · 𝑢) + 𝑣)) ∈ 𝐾)
58	20, 36, 35, 37, 21, 8, 57, 19	ellspsni 20939	. . 3 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍) ∈ (𝑁‘{𝑍}))
59	5	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑉) → 𝑊 ∈ LVec)
60	14	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑉) → 𝑈 ∈ 𝐻)
61	18	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑉) → 𝑍 ∈ 𝑉)
62		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑉) → 𝑢 ∈ 𝑉)
63	26	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑉) → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉)
64	20, 1, 21, 25, 12, 59, 60, 61, 62, 63, 35, 37, 36, 54, 55	lshpkrlem2 39097	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝑉) → (𝐺‘𝑢) ∈ 𝐾)
65	4, 43, 64	syl2anc 584	. . . . . 6 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → (𝐺‘𝑢) ∈ 𝐾)
66		eqid 2729	. . . . . . 7 ⊢ (._r‘𝐷) = (._r‘𝐷)
67	35, 37, 66	lmodmcl 20811	. . . . . 6 ⊢ ((𝑊 ∈ LMod ∧ 𝑙 ∈ 𝐾 ∧ (𝐺‘𝑢) ∈ 𝐾) → (𝑙(._r‘𝐷)(𝐺‘𝑢)) ∈ 𝐾)
68	8, 33, 65, 67	syl3anc 1373	. . . . 5 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → (𝑙(._r‘𝐷)(𝐺‘𝑢)) ∈ 𝐾)
69	5	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝑊 ∈ LVec)
70	14	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝑈 ∈ 𝐻)
71	18	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝑍 ∈ 𝑉)
72		simpr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ 𝑉)
73	26	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉)
74	20, 1, 21, 25, 12, 69, 70, 71, 72, 73, 35, 37, 36, 54, 55	lshpkrlem2 39097	. . . . . 6 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → (𝐺‘𝑣) ∈ 𝐾)
75	4, 46, 74	syl2anc 584	. . . . 5 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → (𝐺‘𝑣) ∈ 𝐾)
76		eqid 2729	. . . . . 6 ⊢ (+_g‘𝐷) = (+_g‘𝐷)
77	35, 37, 76	lmodacl 20810	. . . . 5 ⊢ ((𝑊 ∈ LMod ∧ (𝑙(._r‘𝐷)(𝐺‘𝑢)) ∈ 𝐾 ∧ (𝐺‘𝑣) ∈ 𝐾) → ((𝑙(._r‘𝐷)(𝐺‘𝑢))(+_g‘𝐷)(𝐺‘𝑣)) ∈ 𝐾)
78	8, 68, 75, 77	syl3anc 1373	. . . 4 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → ((𝑙(._r‘𝐷)(𝐺‘𝑢))(+_g‘𝐷)(𝐺‘𝑣)) ∈ 𝐾)
79	20, 36, 35, 37, 21, 8, 78, 19	ellspsni 20939	. . 3 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → (((𝑙(._r‘𝐷)(𝐺‘𝑢))(+_g‘𝐷)(𝐺‘𝑣)) · 𝑍) ∈ (𝑁‘{𝑍}))
80		simp33 1212	. . . 4 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))
81		simp1 1136	. . . . 5 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → (𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉))
82	20, 9	lssel 20875	. . . . . 6 ⊢ ((𝑈 ∈ (LSubSp‘𝑊) ∧ 𝑟 ∈ 𝑈) → 𝑟 ∈ 𝑉)
83	16, 34, 82	syl2anc 584	. . . . 5 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → 𝑟 ∈ 𝑉)
84	20, 9	lssel 20875	. . . . . 6 ⊢ ((𝑈 ∈ (LSubSp‘𝑊) ∧ 𝑠 ∈ 𝑈) → 𝑠 ∈ 𝑉)
85	16, 40, 84	syl2anc 584	. . . . 5 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → 𝑠 ∈ 𝑉)
86		simp31 1210	. . . . 5 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → 𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)))
87		simp32 1211	. . . . 5 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)))
88		lshpkrlem.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
89	20, 1, 21, 25, 12, 5, 14, 18, 88, 26, 35, 37, 36, 54, 55	lshpkrlem4 39099	. . . . 5 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑉 ∧ 𝑠 ∈ 𝑉) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)))) → ((𝑙 · 𝑢) + 𝑣) = (((𝑙 · 𝑟) + 𝑠) + (((𝑙(._r‘𝐷)(𝐺‘𝑢))(+_g‘𝐷)(𝐺‘𝑣)) · 𝑍)))
90	81, 46, 83, 85, 86, 87, 89	syl132anc 1390	. . . 4 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → ((𝑙 · 𝑢) + 𝑣) = (((𝑙 · 𝑟) + 𝑠) + (((𝑙(._r‘𝐷)(𝐺‘𝑢))(+_g‘𝐷)(𝐺‘𝑣)) · 𝑍)))
91	80, 90	eqtr3d 2766	. . 3 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)) = (((𝑙 · 𝑟) + 𝑠) + (((𝑙(._r‘𝐷)(𝐺‘𝑢))(+_g‘𝐷)(𝐺‘𝑣)) · 𝑍)))
92	1, 2, 3, 17, 24, 28, 31, 32, 42, 58, 79, 91	subgdisj2 19606	. 2 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍) = (((𝑙(._r‘𝐷)(𝐺‘𝑢))(+_g‘𝐷)(𝐺‘𝑣)) · 𝑍))
93	20, 21, 25, 12, 2, 13, 14, 18, 26	lshpne0 38972	. . . 4 ⊢ (𝜑 → 𝑍 ≠ (0_g‘𝑊))
94	4, 93	syl 17	. . 3 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → 𝑍 ≠ (0_g‘𝑊))
95	20, 36, 35, 37, 2, 6, 57, 78, 19, 94	lvecvscan2 21054	. 2 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → (((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍) = (((𝑙(._r‘𝐷)(𝐺‘𝑢))(+_g‘𝐷)(𝐺‘𝑣)) · 𝑍) ↔ (𝐺‘((𝑙 · 𝑢) + 𝑣)) = ((𝑙(._r‘𝐷)(𝐺‘𝑢))(+_g‘𝐷)(𝐺‘𝑣))))
96	92, 95	mpbid 232	1 ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → (𝐺‘((𝑙 · 𝑢) + 𝑣)) = ((𝑙(._r‘𝐷)(𝐺‘𝑢))(+_g‘𝐷)(𝐺‘𝑣)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ∃wrex 3053 ∩ cin 3910 ⊆ wss 3911 {csn 4585 ↦ cmpt 5183 ‘cfv 6499 ℩crio 7325 (class class class)co 7369 Basecbs 17155 +_gcplusg 17196 ._rcmulr 17197 Scalarcsca 17199 ·_𝑠 cvsca 17200 0_gc0g 17378 SubGrpcsubg 19034 Cntzccntz 19229 LSSumclsm 19548 Abelcabl 19695 LModclmod 20798 LSubSpclss 20869 LSpanclspn 20909 LVecclvec 21041 LSHypclsh 38961

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5229 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 ax-cnex 11100 ax-resscn 11101 ax-1cn 11102 ax-icn 11103 ax-addcl 11104 ax-addrcl 11105 ax-mulcl 11106 ax-mulrcl 11107 ax-mulcom 11108 ax-addass 11109 ax-mulass 11110 ax-distr 11111 ax-i2m1 11112 ax-1ne0 11113 ax-1rid 11114 ax-rnegex 11115 ax-rrecex 11116 ax-cnre 11117 ax-pre-lttri 11118 ax-pre-lttrn 11119 ax-pre-ltadd 11120 ax-pre-mulgt0 11121

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3351 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-int 4907 df-iun 4953 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6262 df-ord 6323 df-on 6324 df-lim 6325 df-suc 6326 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-riota 7326 df-ov 7372 df-oprab 7373 df-mpo 7374 df-om 7823 df-1st 7947 df-2nd 7948 df-tpos 8182 df-frecs 8237 df-wrecs 8268 df-recs 8317 df-rdg 8355 df-er 8648 df-en 8896 df-dom 8897 df-sdom 8898 df-pnf 11186 df-mnf 11187 df-xr 11188 df-ltxr 11189 df-le 11190 df-sub 11383 df-neg 11384 df-nn 12163 df-2 12225 df-3 12226 df-sets 17110 df-slot 17128 df-ndx 17140 df-base 17156 df-ress 17177 df-plusg 17209 df-mulr 17210 df-0g 17380 df-mgm 18549 df-sgrp 18628 df-mnd 18644 df-submnd 18693 df-grp 18850 df-minusg 18851 df-sbg 18852 df-subg 19037 df-cntz 19231 df-lsm 19550 df-cmn 19696 df-abl 19697 df-mgp 20061 df-rng 20073 df-ur 20102 df-ring 20155 df-oppr 20257 df-dvdsr 20277 df-unit 20278 df-invr 20308 df-drng 20651 df-lmod 20800 df-lss 20870 df-lsp 20910 df-lvec 21042 df-lshyp 38963

This theorem is referenced by: lshpkrlem6 39101

W3C validator