lshpkrlem6

Description: Lemma for lshpkrex . Show linearlity of G . (Contributed by NM, 17-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	lshpkrlem6	$⊢ (φ \land (l \in K \land u \in V \land v \in V)) \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	6	adantr	$⊢ (φ \land (l \in K \land u \in V \land v \in V)) \to W \in LVec$
17	7	adantr	$⊢ (φ \land (l \in K \land u \in V \land v \in V)) \to U \in H$
18	8	adantr	$⊢ (φ \land (l \in K \land u \in V \land v \in V)) \to Z \in V$
19		simpr2	$⊢ (φ \land (l \in K \land u \in V \land v \in V)) \to u \in V$
20	10	adantr	$⊢ (φ \land (l \in K \land u \in V \land v \in V)) \to U \underset{˙}{\oplus} N (\{Z\}) = V$
21	1 2 3 4 5 16 17 18 19 20 11 12 13 14 15	lshpkrlem3	$⊢ (φ \land (l \in K \land u \in V \land v \in V)) \to \exists r \in U u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z)$
22		simpr3	$⊢ (φ \land (l \in K \land u \in V \land v \in V)) \to v \in V$
23	1 2 3 4 5 16 17 18 22 20 11 12 13 14 15	lshpkrlem3	$⊢ (φ \land (l \in K \land u \in V \land v \in V)) \to \exists s \in U v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z)$
24		lveclmod	$⊢ W \in LVec \to W \in LMod$
25	16 24	syl	$⊢ (φ \land (l \in K \land u \in V \land v \in V)) \to W \in LMod$
26		simpr1	$⊢ (φ \land (l \in K \land u \in V \land v \in V)) \to l \in K$
27	1 11 13 12	lmodvscl	$⊢ (W \in LMod \land l \in K \land u \in V) \to l \underset{˙}{\cdot} u \in V$
28	25 26 19 27	syl3anc	$⊢ (φ \land (l \in K \land u \in V \land v \in V)) \to l \underset{˙}{\cdot} u \in V$
29	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$
30	25 28 22 29	syl3anc	$⊢ (φ \land (l \in K \land u \in V \land v \in V)) \to (l \underset{˙}{\cdot} u) \underset{˙}{+} v \in V$
31	1 2 3 4 5 16 17 18 30 20 11 12 13 14 15	lshpkrlem3	$⊢ (φ \land (l \in K \land u \in V \land v \in V)) \to \exists z \in U (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z)$
32		3reeanv	$⊢ \exists r \in U \exists s \in U \exists z \in U (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)) \leftrightarrow (\exists r \in U u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land \exists s \in U v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land \exists z \in U (l \underset{˙}{\cdot} u) \underset{˙}{+} v = z \underset{˙}{+} (G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) \underset{˙}{\cdot} Z))$
33		simp1l	$⊢ ((φ \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 φ$
34		simp1r1	$⊢ ((φ \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$
35		simp1r2	$⊢ ((φ \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$
36		simp1r3	$⊢ ((φ \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$
37		simp2ll	$⊢ ((φ \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$
38		simp2lr	$⊢ ((φ \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$
39		simp2r	$⊢ ((φ \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$
40	38 39	jca	$⊢ ((φ \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 \land z \in U)$
41		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)$
42		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)$
43		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)$
44	1 2 3 4 5 6 7 8 8 10 11 12 13 14 15	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)$
45	33 34 35 36 37 40 41 42 43 44	syl333anc	$⊢ ((φ \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)$
46	45	3exp	$⊢ (φ \land (l \in K \land u \in V \land v \in V)) \to (((r \in U \land s \in U) \land z \in U) \to ((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)))$
47	46	expdimp	$⊢ ((φ \land (l \in K \land u \in V \land v \in V)) \land (r \in U \land s \in U)) \to (z \in U \to ((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)))$
48	47	rexlimdv	$⊢ ((φ \land (l \in K \land u \in V \land v \in V)) \land (r \in U \land s \in U)) \to (\exists z \in U (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))$
49	48	rexlimdvva	$⊢ (φ \land (l \in K \land u \in V \land v \in V)) \to (\exists r \in U \exists s \in U \exists z \in U (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))$
50	32 49	syl5bir	$⊢ (φ \land (l \in K \land u \in V \land v \in V)) \to ((\exists r \in U u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z) \land \exists s \in U v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z) \land \exists z \in U (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))$
51	21 23 31 50	mp3and	$⊢ (φ \land (l \in K \land u \in V \land v \in V)) \to G ((l \underset{˙}{\cdot} u) \underset{˙}{+} v) = (l \cdot_{D} G (u)) +_{D} G (v)$

Metamath Proof Explorer

Theorem lshpkrlem6

Proof