lshpkrlem5

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

	Ref	Expression
Hypotheses	lshpkrlem.v	$⊢ V = {Base}_{W}$
	lshpkrlem.a	$⊢ \underset{˙}{+} = +_{W}$
	lshpkrlem.n	$⊢ N = LSpan (W)$
	lshpkrlem.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
	lshpkrlem.h	$⊢ H = LSHyp (W)$
	lshpkrlem.w	$⊢ φ \to W \in LVec$
	lshpkrlem.u	$⊢ φ \to U \in H$
	lshpkrlem.z	$⊢ φ \to Z \in V$
	lshpkrlem.x	$⊢ φ \to X \in V$
	lshpkrlem.e	$⊢ φ \to U \underset{˙}{\oplus} N (\{Z\}) = V$
	lshpkrlem.d	$⊢ D = Scalar (W)$
	lshpkrlem.k	$⊢ K = {Base}_{D}$
	lshpkrlem.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	lshpkrlem.o	$⊢ \underset{˙}{0} = 0_{D}$
	lshpkrlem.g	$⊢ G = (x \in V ⟼ (ι k \in K \| \exists y \in U x = y \underset{˙}{+} (k \underset{˙}{\cdot} Z)))$
Assertion	lshpkrlem5	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) = (l \cdot_{D} G (u)) +_{D} G (v)$

Proof

Step	Hyp	Ref	Expression
1		lshpkrlem.v	$⊢ V = {Base}_{W}$
2		lshpkrlem.a	$⊢ \underset{˙}{+} = +_{W}$
3		lshpkrlem.n	$⊢ N = LSpan (W)$
4		lshpkrlem.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
5		lshpkrlem.h	$⊢ H = LSHyp (W)$
6		lshpkrlem.w	$⊢ φ \to W \in LVec$
7		lshpkrlem.u	$⊢ φ \to U \in H$
8		lshpkrlem.z	$⊢ φ \to Z \in V$
9		lshpkrlem.x	$⊢ φ \to X \in V$
10		lshpkrlem.e	$⊢ φ \to U \underset{˙}{\oplus} N (\{Z\}) = V$
11		lshpkrlem.d	$⊢ D = Scalar (W)$
12		lshpkrlem.k	$⊢ K = {Base}_{D}$
13		lshpkrlem.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
14		lshpkrlem.o	$⊢ \underset{˙}{0} = 0_{D}$
15		lshpkrlem.g	$⊢ G = (x \in V ⟼ (ι k \in K \| \exists y \in U x = y \underset{˙}{+} (k \underset{˙}{\cdot} Z)))$
16		eqid	$⊢ 0_{W} = 0_{W}$
17		eqid	$⊢ Cntz (W) = Cntz (W)$
18		simp11	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to φ$
19	18 6	syl	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to W \in LVec$
20		lveclmod	$⊢ W \in LVec \to W \in LMod$
21	19 20	syl	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to W \in LMod$
22		eqid	$⊢ LSubSp (W) = LSubSp (W)$
23	22	lsssssubg	$⊢ W \in LMod \to LSubSp (W) \subseteq SubGrp (W)$
24	21 23	syl	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to LSubSp (W) \subseteq SubGrp (W)$
25	6 20	syl	$⊢ φ \to W \in LMod$
26	22 5 25 7	lshplss	$⊢ φ \to U \in LSubSp (W)$
27	18 26	syl	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to U \in LSubSp (W)$
28	24 27	sseldd	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to U \in SubGrp (W)$
29	18 8	syl	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to Z \in V$
30	1 22 3	lspsncl	$⊢ (W \in LMod \land Z \in V) \to N (\{Z\}) \in LSubSp (W)$
31	21 29 30	syl2anc	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to N (\{Z\}) \in LSubSp (W)$
32	24 31	sseldd	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to N (\{Z\}) \in SubGrp (W)$
33	1 16 3 4 5 6 7 8 10	lshpdisj	$⊢ φ \to U \cap N (\{Z\}) = \{0_{W}\}$
34	18 33	syl	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to U \cap N (\{Z\}) = \{0_{W}\}$
35		lmodabl	$⊢ W \in LMod \to W \in Abel$
36	21 35	syl	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to W \in Abel$
37	17 36 28 32	ablcntzd	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to U \subseteq Cntz (W) (N (\{Z\}))$
38		simp23r	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to z \in U$
39		simp12	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to l \in K$
40		simp22	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to r \in U$
41	11 13 12 22	lssvscl	$⊢ ((W \in LMod \land U \in LSubSp (W)) \land (l \in K \land r \in U)) \to l \underset{˙}{\cdot} r \in U$
42	21 27 39 40 41	syl22anc	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to l \underset{˙}{\cdot} r \in U$
43		simp23l	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to s \in U$
44	2 22	lssvacl	$⊢ ((W \in LMod \land U \in LSubSp (W)) \land (l \underset{˙}{\cdot} r \in U \land s \in U)) \to (l \underset{˙}{\cdot} r) \underset{˙}{+} s \in U$
45	21 27 42 43 44	syl22anc	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to (l \underset{˙}{\cdot} r) \underset{˙}{+} s \in U$
46		simp13	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to u \in V$
47	1 11 13 12	lmodvscl	$⊢ (W \in LMod \land l \in K \land u \in V) \to l \underset{˙}{\cdot} u \in V$
48	21 39 46 47	syl3anc	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to l \underset{˙}{\cdot} u \in V$
49		simp21	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to v \in V$
50	1 2	lmodvacl	$⊢ (W \in LMod \land l \underset{˙}{\cdot} u \in V \land v \in V) \to (l \underset{˙}{\cdot} u) \underset{˙}{+} v \in V$
51	21 48 49 50	syl3anc	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to (l \underset{˙}{\cdot} u) \underset{˙}{+} v \in V$
52	6	adantr	$⊢ (φ \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v \in V) \to W \in LVec$
53	7	adantr	$⊢ (φ \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v \in V) \to U \in H$
54	8	adantr	$⊢ (φ \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v \in V) \to Z \in V$
55		simpr	$⊢ (φ \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v \in V) \to (l \underset{˙}{\cdot} u) \underset{˙}{+} v \in V$
56	10	adantr	$⊢ (φ \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v \in V) \to U \underset{˙}{\oplus} N (\{Z\}) = V$
57	1 2 3 4 5 52 53 54 55 56 11 12 13 14 15	lshpkrlem2	$⊢ (φ \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v \in V) \to G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \in K$
58	18 51 57	syl2anc	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \in K$
59	1 13 11 12 3 21 58 29	ellspsni	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z \in N (\{Z\})$
60	6	adantr	$⊢ (φ \land u \in V) \to W \in LVec$
61	7	adantr	$⊢ (φ \land u \in V) \to U \in H$
62	8	adantr	$⊢ (φ \land u \in V) \to Z \in V$
63		simpr	$⊢ (φ \land u \in V) \to u \in V$
64	10	adantr	$⊢ (φ \land u \in V) \to U \underset{˙}{\oplus} N (\{Z\}) = V$
65	1 2 3 4 5 60 61 62 63 64 11 12 13 14 15	lshpkrlem2	$⊢ (φ \land u \in V) \to G (u) \in K$
66	18 46 65	syl2anc	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to G (u) \in K$
67		eqid	$⊢ \cdot_{D} = \cdot_{D}$
68	11 12 67	lmodmcl	$⊢ (W \in LMod \land l \in K \land G (u) \in K) \to l \cdot_{D} G (u) \in K$
69	21 39 66 68	syl3anc	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to l \cdot_{D} G (u) \in K$
70	6	adantr	$⊢ (φ \land v \in V) \to W \in LVec$
71	7	adantr	$⊢ (φ \land v \in V) \to U \in H$
72	8	adantr	$⊢ (φ \land v \in V) \to Z \in V$
73		simpr	$⊢ (φ \land v \in V) \to v \in V$
74	10	adantr	$⊢ (φ \land v \in V) \to U \underset{˙}{\oplus} N (\{Z\}) = V$
75	1 2 3 4 5 70 71 72 73 74 11 12 13 14 15	lshpkrlem2	$⊢ (φ \land v \in V) \to G (v) \in K$
76	18 49 75	syl2anc	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to G (v) \in K$
77		eqid	$⊢ +_{D} = +_{D}$
78	11 12 77	lmodacl	$⊢ (W \in LMod \land l \cdot_{D} G (u) \in K \land G (v) \in K) \to (l \cdot_{D} G (u)) +_{D} G (v) \in K$
79	21 69 76 78	syl3anc	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to (l \cdot_{D} G (u)) +_{D} G (v) \in K$
80	1 13 11 12 3 21 79 29	ellspsni	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to ((l \cdot_{D} G (u)) +_{D} G (v)) \underset{˙}{\cdot} Z \in N (\{Z\})$
81		simp33	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z)$
82		simp1	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to (φ \land l \in K \land u \in V)$
83	1 22	lssel	$⊢ (U \in LSubSp (W) \land r \in U) \to r \in V$
84	27 40 83	syl2anc	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to r \in V$
85	1 22	lssel	$⊢ (U \in LSubSp (W) \land s \in U) \to s \in V$
86	27 43 85	syl2anc	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to s \in V$
87		simp31	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z)$
88		simp32	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z)$
89	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	lshpkrlem4	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in V \land s \in V) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z))) \to (l \underset{˙}{\cdot} u) \underset{˙}{+} v = ((l \underset{˙}{\cdot} r) \underset{˙}{+} s) \underset{˙}{+} (((l \cdot_{D} G (u)) +_{D} G (v)) \underset{˙}{\cdot} Z)$
90	82 49 84 86 87 88 89	syl132anc	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to (l \underset{˙}{\cdot} u) \underset{˙}{+} v = ((l \underset{˙}{\cdot} r) \underset{˙}{+} s) \underset{˙}{+} (((l \cdot_{D} G (u)) +_{D} G (v)) \underset{˙}{\cdot} Z)$
91	81 90	eqtr3d	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z) = ((l \underset{˙}{\cdot} r) \underset{˙}{+} s) \underset{˙}{+} (((l \cdot_{D} G (u)) +_{D} G (v)) \underset{˙}{\cdot} Z)$
92	2 16 17 28 32 34 37 38 45 59 80 91	subgdisj2	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z = ((l \cdot_{D} G (u)) +_{D} G (v)) \underset{˙}{\cdot} Z$
93	1 3 4 5 16 25 7 8 10	lshpne0	$⊢ φ \to Z \neq 0_{W}$
94	18 93	syl	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to Z \neq 0_{W}$
95	1 13 11 12 16 19 58 79 29 94	lvecvscan2	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z = ((l \cdot_{D} G (u)) +_{D} G (v)) \underset{˙}{\cdot} Z \leftrightarrow G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) = (l \cdot_{D} G (u)) +_{D} G (v))$
96	92 95	mpbid	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in U \land (s \in U \land z \in U)) \land (u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))) \to G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) = (l \cdot_{D} G (u)) +_{D} G (v)$

Metamath Proof Explorer

Theorem lshpkrlem5

Proof