lshpsmreu

Description: Lemma for lshpkrex . Show uniqueness of ring multiplier k when a vector X is broken down into components, one in a hyperplane and the other outside of it . TODO: do we need the cbvrexv for a to c ? (Contributed by NM, 4-Jan-2015)

	Ref	Expression
Hypotheses	lshpsmreu.v	$⊢ V = {Base}_{W}$
	lshpsmreu.a	$⊢ \underset{˙}{+} = +_{W}$
	lshpsmreu.n	$⊢ N = LSpan (W)$
	lshpsmreu.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
	lshpsmreu.h	$⊢ H = LSHyp (W)$
	lshpsmreu.w	$⊢ φ \to W \in LVec$
	lshpsmreu.u	$⊢ φ \to U \in H$
	lshpsmreu.z	$⊢ φ \to Z \in V$
	lshpsmreu.x	$⊢ φ \to X \in V$
	lshpsmreu.e	$⊢ φ \to U \underset{˙}{\oplus} N (\{Z\}) = V$
	lshpsmreu.d	$⊢ D = Scalar (W)$
	lshpsmreu.k	$⊢ K = {Base}_{D}$
	lshpsmreu.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
Assertion	lshpsmreu	$⊢ φ \to \exists! k \in K \exists y \in U X = y \underset{˙}{+} (k \underset{˙}{\cdot} Z)$

Proof

Step	Hyp	Ref	Expression
1		lshpsmreu.v	$⊢ V = {Base}_{W}$
2		lshpsmreu.a	$⊢ \underset{˙}{+} = +_{W}$
3		lshpsmreu.n	$⊢ N = LSpan (W)$
4		lshpsmreu.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
5		lshpsmreu.h	$⊢ H = LSHyp (W)$
6		lshpsmreu.w	$⊢ φ \to W \in LVec$
7		lshpsmreu.u	$⊢ φ \to U \in H$
8		lshpsmreu.z	$⊢ φ \to Z \in V$
9		lshpsmreu.x	$⊢ φ \to X \in V$
10		lshpsmreu.e	$⊢ φ \to U \underset{˙}{\oplus} N (\{Z\}) = V$
11		lshpsmreu.d	$⊢ D = Scalar (W)$
12		lshpsmreu.k	$⊢ K = {Base}_{D}$
13		lshpsmreu.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
14	9 10	eleqtrrd	$⊢ φ \to X \in (U \underset{˙}{\oplus} N (\{Z\}))$
15		lveclmod	$⊢ W \in LVec \to W \in LMod$
16	6 15	syl	$⊢ φ \to W \in LMod$
17		eqid	$⊢ LSubSp (W) = LSubSp (W)$
18	17	lsssssubg	$⊢ W \in LMod \to LSubSp (W) \subseteq SubGrp (W)$
19	16 18	syl	$⊢ φ \to LSubSp (W) \subseteq SubGrp (W)$
20	17 5 16 7	lshplss	$⊢ φ \to U \in LSubSp (W)$
21	19 20	sseldd	$⊢ φ \to U \in SubGrp (W)$
22	1 17 3	lspsncl	$⊢ (W \in LMod \land Z \in V) \to N (\{Z\}) \in LSubSp (W)$
23	16 8 22	syl2anc	$⊢ φ \to N (\{Z\}) \in LSubSp (W)$
24	19 23	sseldd	$⊢ φ \to N (\{Z\}) \in SubGrp (W)$
25	2 4	lsmelval	$⊢ (U \in SubGrp (W) \land N (\{Z\}) \in SubGrp (W)) \to (X \in (U \underset{˙}{\oplus} N (\{Z\})) \leftrightarrow \exists c \in U \exists z \in N (\{Z\}) X = c \underset{˙}{+} z)$
26	21 24 25	syl2anc	$⊢ φ \to (X \in (U \underset{˙}{\oplus} N (\{Z\})) \leftrightarrow \exists c \in U \exists z \in N (\{Z\}) X = c \underset{˙}{+} z)$
27	14 26	mpbid	$⊢ φ \to \exists c \in U \exists z \in N (\{Z\}) X = c \underset{˙}{+} z$
28		df-rex	$⊢ \exists z \in N (\{Z\}) X = c \underset{˙}{+} z \leftrightarrow \exists z (z \in N (\{Z\}) \land X = c \underset{˙}{+} z)$
29	11 12 1 13 3	ellspsn	$⊢ (W \in LMod \land Z \in V) \to (z \in N (\{Z\}) \leftrightarrow \exists b \in K z = b \underset{˙}{\cdot} Z)$
30	16 8 29	syl2anc	$⊢ φ \to (z \in N (\{Z\}) \leftrightarrow \exists b \in K z = b \underset{˙}{\cdot} Z)$
31	30	anbi1d	$⊢ φ \to ((z \in N (\{Z\}) \land X = c \underset{˙}{+} z) \leftrightarrow (\exists b \in K z = b \underset{˙}{\cdot} Z \land X = c \underset{˙}{+} z))$
32		r19.41v	$⊢ \exists b \in K (z = b \underset{˙}{\cdot} Z \land X = c \underset{˙}{+} z) \leftrightarrow (\exists b \in K z = b \underset{˙}{\cdot} Z \land X = c \underset{˙}{+} z)$
33	31 32	bitr4di	$⊢ φ \to ((z \in N (\{Z\}) \land X = c \underset{˙}{+} z) \leftrightarrow \exists b \in K (z = b \underset{˙}{\cdot} Z \land X = c \underset{˙}{+} z))$
34	33	exbidv	$⊢ φ \to (\exists z (z \in N (\{Z\}) \land X = c \underset{˙}{+} z) \leftrightarrow \exists z \exists b \in K (z = b \underset{˙}{\cdot} Z \land X = c \underset{˙}{+} z))$
35		rexcom4	$⊢ \exists b \in K \exists z (z = b \underset{˙}{\cdot} Z \land X = c \underset{˙}{+} z) \leftrightarrow \exists z \exists b \in K (z = b \underset{˙}{\cdot} Z \land X = c \underset{˙}{+} z)$
36		ovex	$⊢ b \underset{˙}{\cdot} Z \in V$
37		oveq2	$⊢ z = b \underset{˙}{\cdot} Z \to c \underset{˙}{+} z = c \underset{˙}{+} (b \underset{˙}{\cdot} Z)$
38	37	eqeq2d	$⊢ z = b \underset{˙}{\cdot} Z \to (X = c \underset{˙}{+} z \leftrightarrow X = c \underset{˙}{+} (b \underset{˙}{\cdot} Z))$
39	36 38	ceqsexv	$⊢ \exists z (z = b \underset{˙}{\cdot} Z \land X = c \underset{˙}{+} z) \leftrightarrow X = c \underset{˙}{+} (b \underset{˙}{\cdot} Z)$
40	39	rexbii	$⊢ \exists b \in K \exists z (z = b \underset{˙}{\cdot} Z \land X = c \underset{˙}{+} z) \leftrightarrow \exists b \in K X = c \underset{˙}{+} (b \underset{˙}{\cdot} Z)$
41	35 40	bitr3i	$⊢ \exists z \exists b \in K (z = b \underset{˙}{\cdot} Z \land X = c \underset{˙}{+} z) \leftrightarrow \exists b \in K X = c \underset{˙}{+} (b \underset{˙}{\cdot} Z)$
42	34 41	bitrdi	$⊢ φ \to (\exists z (z \in N (\{Z\}) \land X = c \underset{˙}{+} z) \leftrightarrow \exists b \in K X = c \underset{˙}{+} (b \underset{˙}{\cdot} Z))$
43	28 42	bitrid	$⊢ φ \to (\exists z \in N (\{Z\}) X = c \underset{˙}{+} z \leftrightarrow \exists b \in K X = c \underset{˙}{+} (b \underset{˙}{\cdot} Z))$
44	43	rexbidv	$⊢ φ \to (\exists c \in U \exists z \in N (\{Z\}) X = c \underset{˙}{+} z \leftrightarrow \exists c \in U \exists b \in K X = c \underset{˙}{+} (b \underset{˙}{\cdot} Z))$
45	27 44	mpbid	$⊢ φ \to \exists c \in U \exists b \in K X = c \underset{˙}{+} (b \underset{˙}{\cdot} Z)$
46		rexcom	$⊢ \exists c \in U \exists b \in K X = c \underset{˙}{+} (b \underset{˙}{\cdot} Z) \leftrightarrow \exists b \in K \exists c \in U X = c \underset{˙}{+} (b \underset{˙}{\cdot} Z)$
47	45 46	sylib	$⊢ φ \to \exists b \in K \exists c \in U X = c \underset{˙}{+} (b \underset{˙}{\cdot} Z)$
48		oveq1	$⊢ c = a \to c \underset{˙}{+} (b \underset{˙}{\cdot} Z) = a \underset{˙}{+} (b \underset{˙}{\cdot} Z)$
49	48	eqeq2d	$⊢ c = a \to (X = c \underset{˙}{+} (b \underset{˙}{\cdot} Z) \leftrightarrow X = a \underset{˙}{+} (b \underset{˙}{\cdot} Z))$
50	49	cbvrexvw	$⊢ \exists c \in U X = c \underset{˙}{+} (b \underset{˙}{\cdot} Z) \leftrightarrow \exists a \in U X = a \underset{˙}{+} (b \underset{˙}{\cdot} Z)$
51		eqid	$⊢ 0_{W} = 0_{W}$
52		eqid	$⊢ Cntz (W) = Cntz (W)$
53		simp11l	$⊢ (((φ \land (b \in K \land l \in K)) \land a \in U \land X = a \underset{˙}{+} (b \underset{˙}{\cdot} Z)) \land c \in U \land X = c \underset{˙}{+} (l \underset{˙}{\cdot} Z)) \to φ$
54	53 21	syl	$⊢ (((φ \land (b \in K \land l \in K)) \land a \in U \land X = a \underset{˙}{+} (b \underset{˙}{\cdot} Z)) \land c \in U \land X = c \underset{˙}{+} (l \underset{˙}{\cdot} Z)) \to U \in SubGrp (W)$
55	53 24	syl	$⊢ (((φ \land (b \in K \land l \in K)) \land a \in U \land X = a \underset{˙}{+} (b \underset{˙}{\cdot} Z)) \land c \in U \land X = c \underset{˙}{+} (l \underset{˙}{\cdot} Z)) \to N (\{Z\}) \in SubGrp (W)$
56	1 51 3 4 5 6 7 8 10	lshpdisj	$⊢ φ \to U \cap N (\{Z\}) = \{0_{W}\}$
57	53 56	syl	$⊢ (((φ \land (b \in K \land l \in K)) \land a \in U \land X = a \underset{˙}{+} (b \underset{˙}{\cdot} Z)) \land c \in U \land X = c \underset{˙}{+} (l \underset{˙}{\cdot} Z)) \to U \cap N (\{Z\}) = \{0_{W}\}$
58	53 6	syl	$⊢ (((φ \land (b \in K \land l \in K)) \land a \in U \land X = a \underset{˙}{+} (b \underset{˙}{\cdot} Z)) \land c \in U \land X = c \underset{˙}{+} (l \underset{˙}{\cdot} Z)) \to W \in LVec$
59	58 15	syl	$⊢ (((φ \land (b \in K \land l \in K)) \land a \in U \land X = a \underset{˙}{+} (b \underset{˙}{\cdot} Z)) \land c \in U \land X = c \underset{˙}{+} (l \underset{˙}{\cdot} Z)) \to W \in LMod$
60		lmodabl	$⊢ W \in LMod \to W \in Abel$
61	59 60	syl	$⊢ (((φ \land (b \in K \land l \in K)) \land a \in U \land X = a \underset{˙}{+} (b \underset{˙}{\cdot} Z)) \land c \in U \land X = c \underset{˙}{+} (l \underset{˙}{\cdot} Z)) \to W \in Abel$
62	52 61 54 55	ablcntzd	$⊢ (((φ \land (b \in K \land l \in K)) \land a \in U \land X = a \underset{˙}{+} (b \underset{˙}{\cdot} Z)) \land c \in U \land X = c \underset{˙}{+} (l \underset{˙}{\cdot} Z)) \to U \subseteq Cntz (W) (N (\{Z\}))$
63		simp12	$⊢ (((φ \land (b \in K \land l \in K)) \land a \in U \land X = a \underset{˙}{+} (b \underset{˙}{\cdot} Z)) \land c \in U \land X = c \underset{˙}{+} (l \underset{˙}{\cdot} Z)) \to a \in U$
64		simp2	$⊢ (((φ \land (b \in K \land l \in K)) \land a \in U \land X = a \underset{˙}{+} (b \underset{˙}{\cdot} Z)) \land c \in U \land X = c \underset{˙}{+} (l \underset{˙}{\cdot} Z)) \to c \in U$
65		simp1rl	$⊢ ((φ \land (b \in K \land l \in K)) \land a \in U \land X = a \underset{˙}{+} (b \underset{˙}{\cdot} Z)) \to b \in K$
66	65	3ad2ant1	$⊢ (((φ \land (b \in K \land l \in K)) \land a \in U \land X = a \underset{˙}{+} (b \underset{˙}{\cdot} Z)) \land c \in U \land X = c \underset{˙}{+} (l \underset{˙}{\cdot} Z)) \to b \in K$
67	53 8	syl	$⊢ (((φ \land (b \in K \land l \in K)) \land a \in U \land X = a \underset{˙}{+} (b \underset{˙}{\cdot} Z)) \land c \in U \land X = c \underset{˙}{+} (l \underset{˙}{\cdot} Z)) \to Z \in V$
68	1 13 11 12 3 59 66 67	ellspsni	$⊢ (((φ \land (b \in K \land l \in K)) \land a \in U \land X = a \underset{˙}{+} (b \underset{˙}{\cdot} Z)) \land c \in U \land X = c \underset{˙}{+} (l \underset{˙}{\cdot} Z)) \to b \underset{˙}{\cdot} Z \in N (\{Z\})$
69		simp1rr	$⊢ ((φ \land (b \in K \land l \in K)) \land a \in U \land X = a \underset{˙}{+} (b \underset{˙}{\cdot} Z)) \to l \in K$
70	69	3ad2ant1	$⊢ (((φ \land (b \in K \land l \in K)) \land a \in U \land X = a \underset{˙}{+} (b \underset{˙}{\cdot} Z)) \land c \in U \land X = c \underset{˙}{+} (l \underset{˙}{\cdot} Z)) \to l \in K$
71	1 13 11 12 3 59 70 67	ellspsni	$⊢ (((φ \land (b \in K \land l \in K)) \land a \in U \land X = a \underset{˙}{+} (b \underset{˙}{\cdot} Z)) \land c \in U \land X = c \underset{˙}{+} (l \underset{˙}{\cdot} Z)) \to l \underset{˙}{\cdot} Z \in N (\{Z\})$
72		simp13	$⊢ (((φ \land (b \in K \land l \in K)) \land a \in U \land X = a \underset{˙}{+} (b \underset{˙}{\cdot} Z)) \land c \in U \land X = c \underset{˙}{+} (l \underset{˙}{\cdot} Z)) \to X = a \underset{˙}{+} (b \underset{˙}{\cdot} Z)$
73		simp3	$⊢ (((φ \land (b \in K \land l \in K)) \land a \in U \land X = a \underset{˙}{+} (b \underset{˙}{\cdot} Z)) \land c \in U \land X = c \underset{˙}{+} (l \underset{˙}{\cdot} Z)) \to X = c \underset{˙}{+} (l \underset{˙}{\cdot} Z)$
74	72 73	eqtr3d	$⊢ (((φ \land (b \in K \land l \in K)) \land a \in U \land X = a \underset{˙}{+} (b \underset{˙}{\cdot} Z)) \land c \in U \land X = c \underset{˙}{+} (l \underset{˙}{\cdot} Z)) \to a \underset{˙}{+} (b \underset{˙}{\cdot} Z) = c \underset{˙}{+} (l \underset{˙}{\cdot} Z)$
75	2 51 52 54 55 57 62 63 64 68 71 74	subgdisj2	$⊢ (((φ \land (b \in K \land l \in K)) \land a \in U \land X = a \underset{˙}{+} (b \underset{˙}{\cdot} Z)) \land c \in U \land X = c \underset{˙}{+} (l \underset{˙}{\cdot} Z)) \to b \underset{˙}{\cdot} Z = l \underset{˙}{\cdot} Z$
76	53 7	syl	$⊢ (((φ \land (b \in K \land l \in K)) \land a \in U \land X = a \underset{˙}{+} (b \underset{˙}{\cdot} Z)) \land c \in U \land X = c \underset{˙}{+} (l \underset{˙}{\cdot} Z)) \to U \in H$
77	53 10	syl	$⊢ (((φ \land (b \in K \land l \in K)) \land a \in U \land X = a \underset{˙}{+} (b \underset{˙}{\cdot} Z)) \land c \in U \land X = c \underset{˙}{+} (l \underset{˙}{\cdot} Z)) \to U \underset{˙}{\oplus} N (\{Z\}) = V$
78	1 3 4 5 51 59 76 67 77	lshpne0	$⊢ (((φ \land (b \in K \land l \in K)) \land a \in U \land X = a \underset{˙}{+} (b \underset{˙}{\cdot} Z)) \land c \in U \land X = c \underset{˙}{+} (l \underset{˙}{\cdot} Z)) \to Z \neq 0_{W}$
79	1 13 11 12 51 58 66 70 67 78	lvecvscan2	$⊢ (((φ \land (b \in K \land l \in K)) \land a \in U \land X = a \underset{˙}{+} (b \underset{˙}{\cdot} Z)) \land c \in U \land X = c \underset{˙}{+} (l \underset{˙}{\cdot} Z)) \to (b \underset{˙}{\cdot} Z = l \underset{˙}{\cdot} Z \leftrightarrow b = l)$
80	75 79	mpbid	$⊢ (((φ \land (b \in K \land l \in K)) \land a \in U \land X = a \underset{˙}{+} (b \underset{˙}{\cdot} Z)) \land c \in U \land X = c \underset{˙}{+} (l \underset{˙}{\cdot} Z)) \to b = l$
81	80	rexlimdv3a	$⊢ ((φ \land (b \in K \land l \in K)) \land a \in U \land X = a \underset{˙}{+} (b \underset{˙}{\cdot} Z)) \to (\exists c \in U X = c \underset{˙}{+} (l \underset{˙}{\cdot} Z) \to b = l)$
82	81	rexlimdv3a	$⊢ (φ \land (b \in K \land l \in K)) \to (\exists a \in U X = a \underset{˙}{+} (b \underset{˙}{\cdot} Z) \to (\exists c \in U X = c \underset{˙}{+} (l \underset{˙}{\cdot} Z) \to b = l))$
83	50 82	biimtrid	$⊢ (φ \land (b \in K \land l \in K)) \to (\exists c \in U X = c \underset{˙}{+} (b \underset{˙}{\cdot} Z) \to (\exists c \in U X = c \underset{˙}{+} (l \underset{˙}{\cdot} Z) \to b = l))$
84	83	impd	$⊢ (φ \land (b \in K \land l \in K)) \to ((\exists c \in U X = c \underset{˙}{+} (b \underset{˙}{\cdot} Z) \land \exists c \in U X = c \underset{˙}{+} (l \underset{˙}{\cdot} Z)) \to b = l)$
85	84	ralrimivva	$⊢ φ \to \forall b \in K \forall l \in K ((\exists c \in U X = c \underset{˙}{+} (b \underset{˙}{\cdot} Z) \land \exists c \in U X = c \underset{˙}{+} (l \underset{˙}{\cdot} Z)) \to b = l)$
86		oveq1	$⊢ b = l \to b \underset{˙}{\cdot} Z = l \underset{˙}{\cdot} Z$
87	86	oveq2d	$⊢ b = l \to c \underset{˙}{+} (b \underset{˙}{\cdot} Z) = c \underset{˙}{+} (l \underset{˙}{\cdot} Z)$
88	87	eqeq2d	$⊢ b = l \to (X = c \underset{˙}{+} (b \underset{˙}{\cdot} Z) \leftrightarrow X = c \underset{˙}{+} (l \underset{˙}{\cdot} Z))$
89	88	rexbidv	$⊢ b = l \to (\exists c \in U X = c \underset{˙}{+} (b \underset{˙}{\cdot} Z) \leftrightarrow \exists c \in U X = c \underset{˙}{+} (l \underset{˙}{\cdot} Z))$
90	89	reu4	$⊢ \exists! b \in K \exists c \in U X = c \underset{˙}{+} (b \underset{˙}{\cdot} Z) \leftrightarrow (\exists b \in K \exists c \in U X = c \underset{˙}{+} (b \underset{˙}{\cdot} Z) \land \forall b \in K \forall l \in K ((\exists c \in U X = c \underset{˙}{+} (b \underset{˙}{\cdot} Z) \land \exists c \in U X = c \underset{˙}{+} (l \underset{˙}{\cdot} Z)) \to b = l))$
91	47 85 90	sylanbrc	$⊢ φ \to \exists! b \in K \exists c \in U X = c \underset{˙}{+} (b \underset{˙}{\cdot} Z)$
92		oveq1	$⊢ b = k \to b \underset{˙}{\cdot} Z = k \underset{˙}{\cdot} Z$
93	92	oveq2d	$⊢ b = k \to c \underset{˙}{+} (b \underset{˙}{\cdot} Z) = c \underset{˙}{+} (k \underset{˙}{\cdot} Z)$
94	93	eqeq2d	$⊢ b = k \to (X = c \underset{˙}{+} (b \underset{˙}{\cdot} Z) \leftrightarrow X = c \underset{˙}{+} (k \underset{˙}{\cdot} Z))$
95	94	rexbidv	$⊢ b = k \to (\exists c \in U X = c \underset{˙}{+} (b \underset{˙}{\cdot} Z) \leftrightarrow \exists c \in U X = c \underset{˙}{+} (k \underset{˙}{\cdot} Z))$
96	95	cbvreuvw	$⊢ \exists! b \in K \exists c \in U X = c \underset{˙}{+} (b \underset{˙}{\cdot} Z) \leftrightarrow \exists! k \in K \exists c \in U X = c \underset{˙}{+} (k \underset{˙}{\cdot} Z)$
97		oveq1	$⊢ c = y \to c \underset{˙}{+} (k \underset{˙}{\cdot} Z) = y \underset{˙}{+} (k \underset{˙}{\cdot} Z)$
98	97	eqeq2d	$⊢ c = y \to (X = c \underset{˙}{+} (k \underset{˙}{\cdot} Z) \leftrightarrow X = y \underset{˙}{+} (k \underset{˙}{\cdot} Z))$
99	98	cbvrexvw	$⊢ \exists c \in U X = c \underset{˙}{+} (k \underset{˙}{\cdot} Z) \leftrightarrow \exists y \in U X = y \underset{˙}{+} (k \underset{˙}{\cdot} Z)$
100	99	reubii	$⊢ \exists! k \in K \exists c \in U X = c \underset{˙}{+} (k \underset{˙}{\cdot} Z) \leftrightarrow \exists! k \in K \exists y \in U X = y \underset{˙}{+} (k \underset{˙}{\cdot} Z)$
101	96 100	bitri	$⊢ \exists! b \in K \exists c \in U X = c \underset{˙}{+} (b \underset{˙}{\cdot} Z) \leftrightarrow \exists! k \in K \exists y \in U X = y \underset{˙}{+} (k \underset{˙}{\cdot} Z)$
102	91 101	sylib	$⊢ φ \to \exists! k \in K \exists y \in U X = y \underset{˙}{+} (k \underset{˙}{\cdot} Z)$

Metamath Proof Explorer

Theorem lshpsmreu

Proof