lshpkrlem1

Description: Lemma for lshpkrex . The value of tentative functional G is zero iff its argument belongs to hyperplane U . (Contributed by NM, 14-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	lshpkrlem1	$⊢ φ \to (X \in U \leftrightarrow G (X) = \underset{˙}{0})$

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		lveclmod	$⊢ W \in LVec \to W \in LMod$
17	6 16	syl	$⊢ φ \to W \in LMod$
18	11	lmodfgrp	$⊢ W \in LMod \to D \in Grp$
19	12 14	grpidcl	$⊢ D \in Grp \to \underset{˙}{0} \in K$
20	17 18 19	3syl	$⊢ φ \to \underset{˙}{0} \in K$
21	1 2 3 4 5 6 7 8 9 10 11 12 13	lshpsmreu	$⊢ φ \to \exists! k \in K \exists b \in U X = b \underset{˙}{+} (k \underset{˙}{\cdot} Z)$
22		oveq1	$⊢ k = \underset{˙}{0} \to k \underset{˙}{\cdot} Z = \underset{˙}{0} \underset{˙}{\cdot} Z$
23	22	oveq2d	$⊢ k = \underset{˙}{0} \to b \underset{˙}{+} (k \underset{˙}{\cdot} Z) = b \underset{˙}{+} (\underset{˙}{0} \underset{˙}{\cdot} Z)$
24	23	eqeq2d	$⊢ k = \underset{˙}{0} \to (X = b \underset{˙}{+} (k \underset{˙}{\cdot} Z) \leftrightarrow X = b \underset{˙}{+} (\underset{˙}{0} \underset{˙}{\cdot} Z))$
25	24	rexbidv	$⊢ k = \underset{˙}{0} \to (\exists b \in U X = b \underset{˙}{+} (k \underset{˙}{\cdot} Z) \leftrightarrow \exists b \in U X = b \underset{˙}{+} (\underset{˙}{0} \underset{˙}{\cdot} Z))$
26	25	riota2	$⊢ (\underset{˙}{0} \in K \land \exists! k \in K \exists b \in U X = b \underset{˙}{+} (k \underset{˙}{\cdot} Z)) \to (\exists b \in U X = b \underset{˙}{+} (\underset{˙}{0} \underset{˙}{\cdot} Z) \leftrightarrow (ι k \in K \| \exists b \in U X = b \underset{˙}{+} (k \underset{˙}{\cdot} Z)) = \underset{˙}{0})$
27	20 21 26	syl2anc	$⊢ φ \to (\exists b \in U X = b \underset{˙}{+} (\underset{˙}{0} \underset{˙}{\cdot} Z) \leftrightarrow (ι k \in K \| \exists b \in U X = b \underset{˙}{+} (k \underset{˙}{\cdot} Z)) = \underset{˙}{0})$
28		simpr	$⊢ (φ \land X \in U) \to X \in U$
29		eqidd	$⊢ (φ \land X \in U) \to X = X$
30		eqeq2	$⊢ b = X \to (X = b \leftrightarrow X = X)$
31	30	rspcev	$⊢ (X \in U \land X = X) \to \exists b \in U X = b$
32	28 29 31	syl2anc	$⊢ (φ \land X \in U) \to \exists b \in U X = b$
33	32	ex	$⊢ φ \to (X \in U \to \exists b \in U X = b)$
34		eleq1a	$⊢ b \in U \to (X = b \to X \in U)$
35	34	a1i	$⊢ φ \to (b \in U \to (X = b \to X \in U))$
36	35	rexlimdv	$⊢ φ \to (\exists b \in U X = b \to X \in U)$
37	33 36	impbid	$⊢ φ \to (X \in U \leftrightarrow \exists b \in U X = b)$
38		eqid	$⊢ 0_{W} = 0_{W}$
39	1 11 13 14 38	lmod0vs	$⊢ (W \in LMod \land Z \in V) \to \underset{˙}{0} \underset{˙}{\cdot} Z = 0_{W}$
40	17 8 39	syl2anc	$⊢ φ \to \underset{˙}{0} \underset{˙}{\cdot} Z = 0_{W}$
41	40	adantr	$⊢ (φ \land b \in U) \to \underset{˙}{0} \underset{˙}{\cdot} Z = 0_{W}$
42	41	oveq2d	$⊢ (φ \land b \in U) \to b \underset{˙}{+} (\underset{˙}{0} \underset{˙}{\cdot} Z) = b \underset{˙}{+} 0_{W}$
43	6	adantr	$⊢ (φ \land b \in U) \to W \in LVec$
44	43 16	syl	$⊢ (φ \land b \in U) \to W \in LMod$
45		eqid	$⊢ LSubSp (W) = LSubSp (W)$
46	45 5 17 7	lshplss	$⊢ φ \to U \in LSubSp (W)$
47	1 45	lssel	$⊢ (U \in LSubSp (W) \land b \in U) \to b \in V$
48	46 47	sylan	$⊢ (φ \land b \in U) \to b \in V$
49	1 2 38	lmod0vrid	$⊢ (W \in LMod \land b \in V) \to b \underset{˙}{+} 0_{W} = b$
50	44 48 49	syl2anc	$⊢ (φ \land b \in U) \to b \underset{˙}{+} 0_{W} = b$
51	42 50	eqtrd	$⊢ (φ \land b \in U) \to b \underset{˙}{+} (\underset{˙}{0} \underset{˙}{\cdot} Z) = b$
52	51	eqeq2d	$⊢ (φ \land b \in U) \to (X = b \underset{˙}{+} (\underset{˙}{0} \underset{˙}{\cdot} Z) \leftrightarrow X = b)$
53	52	bicomd	$⊢ (φ \land b \in U) \to (X = b \leftrightarrow X = b \underset{˙}{+} (\underset{˙}{0} \underset{˙}{\cdot} Z))$
54	53	rexbidva	$⊢ φ \to (\exists b \in U X = b \leftrightarrow \exists b \in U X = b \underset{˙}{+} (\underset{˙}{0} \underset{˙}{\cdot} Z))$
55	37 54	bitrd	$⊢ φ \to (X \in U \leftrightarrow \exists b \in U X = b \underset{˙}{+} (\underset{˙}{0} \underset{˙}{\cdot} Z))$
56		eqeq1	$⊢ x = X \to (x = y \underset{˙}{+} (k \underset{˙}{\cdot} Z) \leftrightarrow X = y \underset{˙}{+} (k \underset{˙}{\cdot} Z))$
57	56	rexbidv	$⊢ x = X \to (\exists y \in U x = y \underset{˙}{+} (k \underset{˙}{\cdot} Z) \leftrightarrow \exists y \in U X = y \underset{˙}{+} (k \underset{˙}{\cdot} Z))$
58	57	riotabidv	$⊢ x = X \to (ι k \in K \| \exists y \in U x = y \underset{˙}{+} (k \underset{˙}{\cdot} Z)) = (ι k \in K \| \exists y \in U X = y \underset{˙}{+} (k \underset{˙}{\cdot} Z))$
59		riotaex	$⊢ (ι k \in K \| \exists y \in U X = y \underset{˙}{+} (k \underset{˙}{\cdot} Z)) \in V$
60	58 15 59	fvmpt	$⊢ X \in V \to G (X) = (ι k \in K \| \exists y \in U X = y \underset{˙}{+} (k \underset{˙}{\cdot} Z))$
61		oveq1	$⊢ y = b \to y \underset{˙}{+} (k \underset{˙}{\cdot} Z) = b \underset{˙}{+} (k \underset{˙}{\cdot} Z)$
62	61	eqeq2d	$⊢ y = b \to (X = y \underset{˙}{+} (k \underset{˙}{\cdot} Z) \leftrightarrow X = b \underset{˙}{+} (k \underset{˙}{\cdot} Z))$
63	62	cbvrexvw	$⊢ \exists y \in U X = y \underset{˙}{+} (k \underset{˙}{\cdot} Z) \leftrightarrow \exists b \in U X = b \underset{˙}{+} (k \underset{˙}{\cdot} Z)$
64	63	a1i	$⊢ k \in K \to (\exists y \in U X = y \underset{˙}{+} (k \underset{˙}{\cdot} Z) \leftrightarrow \exists b \in U X = b \underset{˙}{+} (k \underset{˙}{\cdot} Z))$
65	64	riotabiia	$⊢ (ι k \in K \| \exists y \in U X = y \underset{˙}{+} (k \underset{˙}{\cdot} Z)) = (ι k \in K \| \exists b \in U X = b \underset{˙}{+} (k \underset{˙}{\cdot} Z))$
66	60 65	eqtrdi	$⊢ X \in V \to G (X) = (ι k \in K \| \exists b \in U X = b \underset{˙}{+} (k \underset{˙}{\cdot} Z))$
67	9 66	syl	$⊢ φ \to G (X) = (ι k \in K \| \exists b \in U X = b \underset{˙}{+} (k \underset{˙}{\cdot} Z))$
68	67	eqeq1d	$⊢ φ \to (G (X) = \underset{˙}{0} \leftrightarrow (ι k \in K \| \exists b \in U X = b \underset{˙}{+} (k \underset{˙}{\cdot} Z)) = \underset{˙}{0})$
69	27 55 68	3bitr4d	$⊢ φ \to (X \in U \leftrightarrow G (X) = \underset{˙}{0})$

Metamath Proof Explorer

Theorem lshpkrlem1

Proof