lshpkrlem4

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	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)$

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		simp3l	$⊢ ((φ \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 u = r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z)$
17	16	oveq2d	$⊢ ((φ \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 = l \underset{˙}{\cdot} (r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z))$
18		simp3r	$⊢ ((φ \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 v = s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z)$
19	17 18	oveq12d	$⊢ ((φ \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{˙}{+} (G (u) \underset{˙}{\cdot} Z))) \underset{˙}{+} (s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z))$
20		simpl1	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in V \land s \in V)) \to φ$
21		lveclmod	$⊢ W \in LVec \to W \in LMod$
22	20 6 21	3syl	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in V \land s \in V)) \to W \in LMod$
23		simpl2	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in V \land s \in V)) \to l \in K$
24		simpr2	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in V \land s \in V)) \to r \in V$
25		simpl3	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in V \land s \in V)) \to u \in V$
26	6	adantr	$⊢ (φ \land u \in V) \to W \in LVec$
27	7	adantr	$⊢ (φ \land u \in V) \to U \in H$
28	8	adantr	$⊢ (φ \land u \in V) \to Z \in V$
29		simpr	$⊢ (φ \land u \in V) \to u \in V$
30	10	adantr	$⊢ (φ \land u \in V) \to U \underset{˙}{\oplus} N (\{Z\}) = V$
31	1 2 3 4 5 26 27 28 29 30 11 12 13 14 15	lshpkrlem2	$⊢ (φ \land u \in V) \to G (u) \in K$
32	20 25 31	syl2anc	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in V \land s \in V)) \to G (u) \in K$
33	20 8	syl	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in V \land s \in V)) \to Z \in V$
34	1 11 13 12	lmodvscl	$⊢ (W \in LMod \land G (u) \in K \land Z \in V) \to G (u) \underset{˙}{\cdot} Z \in V$
35	22 32 33 34	syl3anc	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in V \land s \in V)) \to G (u) \underset{˙}{\cdot} Z \in V$
36	1 2 11 13 12	lmodvsdi	$⊢ (W \in LMod \land (l \in K \land r \in V \land G (u) \underset{˙}{\cdot} Z \in V)) \to l \underset{˙}{\cdot} (r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z)) = (l \underset{˙}{\cdot} r) \underset{˙}{+} (l \underset{˙}{\cdot} (G (u) \underset{˙}{\cdot} Z))$
37	22 23 24 35 36	syl13anc	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in V \land s \in V)) \to l \underset{˙}{\cdot} (r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z)) = (l \underset{˙}{\cdot} r) \underset{˙}{+} (l \underset{˙}{\cdot} (G (u) \underset{˙}{\cdot} Z))$
38		eqid	$⊢ \cdot_{D} = \cdot_{D}$
39	1 11 13 12 38	lmodvsass	$⊢ (W \in LMod \land (l \in K \land G (u) \in K \land Z \in V)) \to (l \cdot_{D} G (u)) \underset{˙}{\cdot} Z = l \underset{˙}{\cdot} (G (u) \underset{˙}{\cdot} Z)$
40	22 23 32 33 39	syl13anc	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in V \land s \in V)) \to (l \cdot_{D} G (u)) \underset{˙}{\cdot} Z = l \underset{˙}{\cdot} (G (u) \underset{˙}{\cdot} Z)$
41	40	oveq2d	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in V \land s \in V)) \to (l \underset{˙}{\cdot} r) \underset{˙}{+} ((l \cdot_{D} G (u)) \underset{˙}{\cdot} Z) = (l \underset{˙}{\cdot} r) \underset{˙}{+} (l \underset{˙}{\cdot} (G (u) \underset{˙}{\cdot} Z))$
42	37 41	eqtr4d	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in V \land s \in V)) \to l \underset{˙}{\cdot} (r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z)) = (l \underset{˙}{\cdot} r) \underset{˙}{+} ((l \cdot_{D} G (u)) \underset{˙}{\cdot} Z)$
43	42	oveq1d	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in V \land s \in V)) \to (l \underset{˙}{\cdot} (r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z))) \underset{˙}{+} (s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z)) = ((l \underset{˙}{\cdot} r) \underset{˙}{+} ((l \cdot_{D} G (u)) \underset{˙}{\cdot} Z)) \underset{˙}{+} (s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z))$
44	1 11 13 12	lmodvscl	$⊢ (W \in LMod \land l \in K \land r \in V) \to l \underset{˙}{\cdot} r \in V$
45	22 23 24 44	syl3anc	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in V \land s \in V)) \to l \underset{˙}{\cdot} r \in V$
46	11 12 38	lmodmcl	$⊢ (W \in LMod \land l \in K \land G (u) \in K) \to l \cdot_{D} G (u) \in K$
47	22 23 32 46	syl3anc	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in V \land s \in V)) \to l \cdot_{D} G (u) \in K$
48	1 11 13 12	lmodvscl	$⊢ (W \in LMod \land l \cdot_{D} G (u) \in K \land Z \in V) \to (l \cdot_{D} G (u)) \underset{˙}{\cdot} Z \in V$
49	22 47 33 48	syl3anc	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in V \land s \in V)) \to (l \cdot_{D} G (u)) \underset{˙}{\cdot} Z \in V$
50		simpr3	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in V \land s \in V)) \to s \in V$
51		simpr1	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in V \land s \in V)) \to v \in V$
52	6	adantr	$⊢ (φ \land v \in V) \to W \in LVec$
53	7	adantr	$⊢ (φ \land v \in V) \to U \in H$
54	8	adantr	$⊢ (φ \land v \in V) \to Z \in V$
55		simpr	$⊢ (φ \land v \in V) \to v \in V$
56	10	adantr	$⊢ (φ \land 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 v \in V) \to G (v) \in K$
58	20 51 57	syl2anc	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in V \land s \in V)) \to G (v) \in K$
59	1 11 13 12	lmodvscl	$⊢ (W \in LMod \land G (v) \in K \land Z \in V) \to G (v) \underset{˙}{\cdot} Z \in V$
60	22 58 33 59	syl3anc	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in V \land s \in V)) \to G (v) \underset{˙}{\cdot} Z \in V$
61	1 2	lmod4	$⊢ (W \in LMod \land (l \underset{˙}{\cdot} r \in V \land (l \cdot_{D} G (u)) \underset{˙}{\cdot} Z \in V) \land (s \in V \land G (v) \underset{˙}{\cdot} Z \in V)) \to ((l \underset{˙}{\cdot} r) \underset{˙}{+} ((l \cdot_{D} G (u)) \underset{˙}{\cdot} Z)) \underset{˙}{+} (s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z)) = ((l \underset{˙}{\cdot} r) \underset{˙}{+} s) \underset{˙}{+} (((l \cdot_{D} G (u)) \underset{˙}{\cdot} Z) \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z))$
62	22 45 49 50 60 61	syl122anc	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in V \land s \in V)) \to ((l \underset{˙}{\cdot} r) \underset{˙}{+} ((l \cdot_{D} G (u)) \underset{˙}{\cdot} Z)) \underset{˙}{+} (s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z)) = ((l \underset{˙}{\cdot} r) \underset{˙}{+} s) \underset{˙}{+} (((l \cdot_{D} G (u)) \underset{˙}{\cdot} Z) \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z))$
63		eqid	$⊢ +_{D} = +_{D}$
64	1 2 11 13 12 63	lmodvsdir	$⊢ (W \in LMod \land (l \cdot_{D} G (u) \in K \land G (v) \in K \land Z \in V)) \to ((l \cdot_{D} G (u)) +_{D} G (v)) \underset{˙}{\cdot} Z = ((l \cdot_{D} G (u)) \underset{˙}{\cdot} Z) \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z)$
65	22 47 58 33 64	syl13anc	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in V \land s \in V)) \to ((l \cdot_{D} G (u)) +_{D} G (v)) \underset{˙}{\cdot} Z = ((l \cdot_{D} G (u)) \underset{˙}{\cdot} Z) \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z)$
66	65	oveq2d	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in V \land s \in V)) \to ((l \underset{˙}{\cdot} r) \underset{˙}{+} s) \underset{˙}{+} (((l \cdot_{D} G (u)) +_{D} G (v)) \underset{˙}{\cdot} Z) = ((l \underset{˙}{\cdot} r) \underset{˙}{+} s) \underset{˙}{+} (((l \cdot_{D} G (u)) \underset{˙}{\cdot} Z) \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z))$
67	62 66	eqtr4d	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in V \land s \in V)) \to ((l \underset{˙}{\cdot} r) \underset{˙}{+} ((l \cdot_{D} G (u)) \underset{˙}{\cdot} Z)) \underset{˙}{+} (s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z)) = ((l \underset{˙}{\cdot} r) \underset{˙}{+} s) \underset{˙}{+} (((l \cdot_{D} G (u)) +_{D} G (v)) \underset{˙}{\cdot} Z)$
68	43 67	eqtrd	$⊢ ((φ \land l \in K \land u \in V) \land (v \in V \land r \in V \land s \in V)) \to (l \underset{˙}{\cdot} (r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z))) \underset{˙}{+} (s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z)) = ((l \underset{˙}{\cdot} r) \underset{˙}{+} s) \underset{˙}{+} (((l \cdot_{D} G (u)) +_{D} G (v)) \underset{˙}{\cdot} Z)$
69	68	3adant3	$⊢ ((φ \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} (r \underset{˙}{+} (G (u) \underset{˙}{\cdot} Z))) \underset{˙}{+} (s \underset{˙}{+} (G (v) \underset{˙}{\cdot} Z)) = ((l \underset{˙}{\cdot} r) \underset{˙}{+} s) \underset{˙}{+} (((l \cdot_{D} G (u)) +_{D} G (v)) \underset{˙}{\cdot} Z)$
70	19 69	eqtrd	$⊢ ((φ \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)$

Metamath Proof Explorer

Theorem lshpkrlem4

Proof