lindsunlem

	Ref	Expression
Hypotheses	lindsun.n	$⊢ N = LSpan (W)$
	lindsun.0	$⊢ \underset{˙}{0} = 0_{W}$
	lindsun.w	$⊢ φ \to W \in LVec$
	lindsun.u	$⊢ φ \to U \in LIndS (W)$
	lindsun.v	$⊢ φ \to V \in LIndS (W)$
	lindsun.2	$⊢ φ \to N (U) \cap N (V) = \{\underset{˙}{0}\}$
	lindsunlem.o	$⊢ O = 0_{Scalar (W)}$
	lindsunlem.f	$⊢ F = {Base}_{Scalar (W)}$
	lindsunlem.c	$⊢ φ \to C \in U$
	lindsunlem.k	$⊢ φ \to K \in (F ∖ \{O\})$
	lindsunlem.1	$⊢ φ \to K \cdot_{W} C \in N ((U \cup V) ∖ \{C\})$
Assertion	lindsunlem	$⊢ φ \to ⊥$

Proof

Step	Hyp	Ref	Expression
1		lindsun.n	$⊢ N = LSpan (W)$
2		lindsun.0	$⊢ \underset{˙}{0} = 0_{W}$
3		lindsun.w	$⊢ φ \to W \in LVec$
4		lindsun.u	$⊢ φ \to U \in LIndS (W)$
5		lindsun.v	$⊢ φ \to V \in LIndS (W)$
6		lindsun.2	$⊢ φ \to N (U) \cap N (V) = \{\underset{˙}{0}\}$
7		lindsunlem.o	$⊢ O = 0_{Scalar (W)}$
8		lindsunlem.f	$⊢ F = {Base}_{Scalar (W)}$
9		lindsunlem.c	$⊢ φ \to C \in U$
10		lindsunlem.k	$⊢ φ \to K \in (F ∖ \{O\})$
11		lindsunlem.1	$⊢ φ \to K \cdot_{W} C \in N ((U \cup V) ∖ \{C\})$
12		simpr	$⊢ (((φ \land x \in N (U ∖ \{C\})) \land y \in N (V)) \land K \cdot_{W} C = x +_{W} y) \to K \cdot_{W} C = x +_{W} y$
13		lveclmod	$⊢ W \in LVec \to W \in LMod$
14	3 13	syl	$⊢ φ \to W \in LMod$
15		lmodgrp	$⊢ W \in LMod \to W \in Grp$
16	14 15	syl	$⊢ φ \to W \in Grp$
17	16	ad3antrrr	$⊢ (((φ \land x \in N (U ∖ \{C\})) \land y \in N (V)) \land K \cdot_{W} C = x +_{W} y) \to W \in Grp$
18		lmodabl	$⊢ W \in LMod \to W \in Abel$
19	14 18	syl	$⊢ φ \to W \in Abel$
20	19	ad3antrrr	$⊢ (((φ \land x \in N (U ∖ \{C\})) \land y \in N (V)) \land K \cdot_{W} C = x +_{W} y) \to W \in Abel$
21		eqid	$⊢ {Base}_{W} = {Base}_{W}$
22	21	linds1	$⊢ U \in LIndS (W) \to U \subseteq {Base}_{W}$
23	4 22	syl	$⊢ φ \to U \subseteq {Base}_{W}$
24	21 1	lspssv	$⊢ (W \in LMod \land U \subseteq {Base}_{W}) \to N (U) \subseteq {Base}_{W}$
25	14 23 24	syl2anc	$⊢ φ \to N (U) \subseteq {Base}_{W}$
26	25	ad3antrrr	$⊢ (((φ \land x \in N (U ∖ \{C\})) \land y \in N (V)) \land K \cdot_{W} C = x +_{W} y) \to N (U) \subseteq {Base}_{W}$
27		difssd	$⊢ φ \to U ∖ \{C\} \subseteq U$
28	21 1	lspss	$⊢ (W \in LMod \land U \subseteq {Base}_{W} \land U ∖ \{C\} \subseteq U) \to N (U ∖ \{C\}) \subseteq N (U)$
29	14 23 27 28	syl3anc	$⊢ φ \to N (U ∖ \{C\}) \subseteq N (U)$
30	29	ad3antrrr	$⊢ (((φ \land x \in N (U ∖ \{C\})) \land y \in N (V)) \land K \cdot_{W} C = x +_{W} y) \to N (U ∖ \{C\}) \subseteq N (U)$
31		simpllr	$⊢ (((φ \land x \in N (U ∖ \{C\})) \land y \in N (V)) \land K \cdot_{W} C = x +_{W} y) \to x \in N (U ∖ \{C\})$
32	30 31	sseldd	$⊢ (((φ \land x \in N (U ∖ \{C\})) \land y \in N (V)) \land K \cdot_{W} C = x +_{W} y) \to x \in N (U)$
33	26 32	sseldd	$⊢ (((φ \land x \in N (U ∖ \{C\})) \land y \in N (V)) \land K \cdot_{W} C = x +_{W} y) \to x \in {Base}_{W}$
34	21	linds1	$⊢ V \in LIndS (W) \to V \subseteq {Base}_{W}$
35	5 34	syl	$⊢ φ \to V \subseteq {Base}_{W}$
36	21 1	lspssv	$⊢ (W \in LMod \land V \subseteq {Base}_{W}) \to N (V) \subseteq {Base}_{W}$
37	14 35 36	syl2anc	$⊢ φ \to N (V) \subseteq {Base}_{W}$
38	37	ad3antrrr	$⊢ (((φ \land x \in N (U ∖ \{C\})) \land y \in N (V)) \land K \cdot_{W} C = x +_{W} y) \to N (V) \subseteq {Base}_{W}$
39		simplr	$⊢ (((φ \land x \in N (U ∖ \{C\})) \land y \in N (V)) \land K \cdot_{W} C = x +_{W} y) \to y \in N (V)$
40	38 39	sseldd	$⊢ (((φ \land x \in N (U ∖ \{C\})) \land y \in N (V)) \land K \cdot_{W} C = x +_{W} y) \to y \in {Base}_{W}$
41		eqid	$⊢ +_{W} = +_{W}$
42	21 41	ablcom	$⊢ (W \in Abel \land x \in {Base}_{W} \land y \in {Base}_{W}) \to x +_{W} y = y +_{W} x$
43	20 33 40 42	syl3anc	$⊢ (((φ \land x \in N (U ∖ \{C\})) \land y \in N (V)) \land K \cdot_{W} C = x +_{W} y) \to x +_{W} y = y +_{W} x$
44	12 43	eqtr2d	$⊢ (((φ \land x \in N (U ∖ \{C\})) \land y \in N (V)) \land K \cdot_{W} C = x +_{W} y) \to y +_{W} x = K \cdot_{W} C$
45	10	eldifad	$⊢ φ \to K \in F$
46	23 9	sseldd	$⊢ φ \to C \in {Base}_{W}$
47		eqid	$⊢ Scalar (W) = Scalar (W)$
48		eqid	$⊢ \cdot_{W} = \cdot_{W}$
49	21 47 48 8	lmodvscl	$⊢ (W \in LMod \land K \in F \land C \in {Base}_{W}) \to K \cdot_{W} C \in {Base}_{W}$
50	14 45 46 49	syl3anc	$⊢ φ \to K \cdot_{W} C \in {Base}_{W}$
51	50	ad3antrrr	$⊢ (((φ \land x \in N (U ∖ \{C\})) \land y \in N (V)) \land K \cdot_{W} C = x +_{W} y) \to K \cdot_{W} C \in {Base}_{W}$
52		eqid	$⊢ -_{W} = -_{W}$
53	21 41 52	grpsubadd	$⊢ (W \in Grp \land (K \cdot_{W} C \in {Base}_{W} \land x \in {Base}_{W} \land y \in {Base}_{W})) \to ((K \cdot_{W} C) -_{W} x = y \leftrightarrow y +_{W} x = K \cdot_{W} C)$
54	53	biimpar	$⊢ ((W \in Grp \land (K \cdot_{W} C \in {Base}_{W} \land x \in {Base}_{W} \land y \in {Base}_{W})) \land y +_{W} x = K \cdot_{W} C) \to (K \cdot_{W} C) -_{W} x = y$
55	54	an32s	$⊢ ((W \in Grp \land y +_{W} x = K \cdot_{W} C) \land (K \cdot_{W} C \in {Base}_{W} \land x \in {Base}_{W} \land y \in {Base}_{W})) \to (K \cdot_{W} C) -_{W} x = y$
56	17 44 51 33 40 55	syl23anc	$⊢ (((φ \land x \in N (U ∖ \{C\})) \land y \in N (V)) \land K \cdot_{W} C = x +_{W} y) \to (K \cdot_{W} C) -_{W} x = y$
57	14	ad3antrrr	$⊢ (((φ \land x \in N (U ∖ \{C\})) \land y \in N (V)) \land K \cdot_{W} C = x +_{W} y) \to W \in LMod$
58		eqid	$⊢ LSubSp (W) = LSubSp (W)$
59	21 58 1	lspcl	$⊢ (W \in LMod \land U \subseteq {Base}_{W}) \to N (U) \in LSubSp (W)$
60	14 23 59	syl2anc	$⊢ φ \to N (U) \in LSubSp (W)$
61	60	ad3antrrr	$⊢ (((φ \land x \in N (U ∖ \{C\})) \land y \in N (V)) \land K \cdot_{W} C = x +_{W} y) \to N (U) \in LSubSp (W)$
62	45	ad3antrrr	$⊢ (((φ \land x \in N (U ∖ \{C\})) \land y \in N (V)) \land K \cdot_{W} C = x +_{W} y) \to K \in F$
63	21 1	lspssid	$⊢ (W \in LMod \land U \subseteq {Base}_{W}) \to U \subseteq N (U)$
64	14 23 63	syl2anc	$⊢ φ \to U \subseteq N (U)$
65	64 9	sseldd	$⊢ φ \to C \in N (U)$
66	65	ad3antrrr	$⊢ (((φ \land x \in N (U ∖ \{C\})) \land y \in N (V)) \land K \cdot_{W} C = x +_{W} y) \to C \in N (U)$
67	47 48 8 58	lssvscl	$⊢ ((W \in LMod \land N (U) \in LSubSp (W)) \land (K \in F \land C \in N (U))) \to K \cdot_{W} C \in N (U)$
68	57 61 62 66 67	syl22anc	$⊢ (((φ \land x \in N (U ∖ \{C\})) \land y \in N (V)) \land K \cdot_{W} C = x +_{W} y) \to K \cdot_{W} C \in N (U)$
69	52 58	lssvsubcl	$⊢ ((W \in LMod \land N (U) \in LSubSp (W)) \land (K \cdot_{W} C \in N (U) \land x \in N (U))) \to (K \cdot_{W} C) -_{W} x \in N (U)$
70	57 61 68 32 69	syl22anc	$⊢ (((φ \land x \in N (U ∖ \{C\})) \land y \in N (V)) \land K \cdot_{W} C = x +_{W} y) \to (K \cdot_{W} C) -_{W} x \in N (U)$
71	56 70	eqeltrrd	$⊢ (((φ \land x \in N (U ∖ \{C\})) \land y \in N (V)) \land K \cdot_{W} C = x +_{W} y) \to y \in N (U)$
72	71 39	elind	$⊢ (((φ \land x \in N (U ∖ \{C\})) \land y \in N (V)) \land K \cdot_{W} C = x +_{W} y) \to y \in (N (U) \cap N (V))$
73	6	ad3antrrr	$⊢ (((φ \land x \in N (U ∖ \{C\})) \land y \in N (V)) \land K \cdot_{W} C = x +_{W} y) \to N (U) \cap N (V) = \{\underset{˙}{0}\}$
74	72 73	eleqtrd	$⊢ (((φ \land x \in N (U ∖ \{C\})) \land y \in N (V)) \land K \cdot_{W} C = x +_{W} y) \to y \in \{\underset{˙}{0}\}$
75		elsni	$⊢ y \in \{\underset{˙}{0}\} \to y = \underset{˙}{0}$
76	74 75	syl	$⊢ (((φ \land x \in N (U ∖ \{C\})) \land y \in N (V)) \land K \cdot_{W} C = x +_{W} y) \to y = \underset{˙}{0}$
77	76	oveq2d	$⊢ (((φ \land x \in N (U ∖ \{C\})) \land y \in N (V)) \land K \cdot_{W} C = x +_{W} y) \to x +_{W} y = x +_{W} \underset{˙}{0}$
78	21 41 2	grprid	$⊢ (W \in Grp \land x \in {Base}_{W}) \to x +_{W} \underset{˙}{0} = x$
79	17 33 78	syl2anc	$⊢ (((φ \land x \in N (U ∖ \{C\})) \land y \in N (V)) \land K \cdot_{W} C = x +_{W} y) \to x +_{W} \underset{˙}{0} = x$
80	12 77 79	3eqtrd	$⊢ (((φ \land x \in N (U ∖ \{C\})) \land y \in N (V)) \land K \cdot_{W} C = x +_{W} y) \to K \cdot_{W} C = x$
81	80 31	eqeltrd	$⊢ (((φ \land x \in N (U ∖ \{C\})) \land y \in N (V)) \land K \cdot_{W} C = x +_{W} y) \to K \cdot_{W} C \in N (U ∖ \{C\})$
82	9	ad3antrrr	$⊢ (((φ \land x \in N (U ∖ \{C\})) \land y \in N (V)) \land K \cdot_{W} C = x +_{W} y) \to C \in U$
83	10	ad3antrrr	$⊢ (((φ \land x \in N (U ∖ \{C\})) \land y \in N (V)) \land K \cdot_{W} C = x +_{W} y) \to K \in (F ∖ \{O\})$
84	3	ad3antrrr	$⊢ (((φ \land x \in N (U ∖ \{C\})) \land y \in N (V)) \land K \cdot_{W} C = x +_{W} y) \to W \in LVec$
85	4	ad3antrrr	$⊢ (((φ \land x \in N (U ∖ \{C\})) \land y \in N (V)) \land K \cdot_{W} C = x +_{W} y) \to U \in LIndS (W)$
86	21 48 1 47 8 7	islinds2	$⊢ W \in LVec \to (U \in LIndS (W) \leftrightarrow (U \subseteq {Base}_{W} \land \forall c \in U \forall k \in (F ∖ \{O\}) \neg k \cdot_{W} c \in N (U ∖ \{c\})))$
87	86	simplbda	$⊢ (W \in LVec \land U \in LIndS (W)) \to \forall c \in U \forall k \in (F ∖ \{O\}) \neg k \cdot_{W} c \in N (U ∖ \{c\})$
88	84 85 87	syl2anc	$⊢ (((φ \land x \in N (U ∖ \{C\})) \land y \in N (V)) \land K \cdot_{W} C = x +_{W} y) \to \forall c \in U \forall k \in (F ∖ \{O\}) \neg k \cdot_{W} c \in N (U ∖ \{c\})$
89		oveq2	$⊢ c = C \to k \cdot_{W} c = k \cdot_{W} C$
90		sneq	$⊢ c = C \to \{c\} = \{C\}$
91	90	difeq2d	$⊢ c = C \to U ∖ \{c\} = U ∖ \{C\}$
92	91	fveq2d	$⊢ c = C \to N (U ∖ \{c\}) = N (U ∖ \{C\})$
93	89 92	eleq12d	$⊢ c = C \to (k \cdot_{W} c \in N (U ∖ \{c\}) \leftrightarrow k \cdot_{W} C \in N (U ∖ \{C\}))$
94	93	notbid	$⊢ c = C \to (\neg k \cdot_{W} c \in N (U ∖ \{c\}) \leftrightarrow \neg k \cdot_{W} C \in N (U ∖ \{C\}))$
95		oveq1	$⊢ k = K \to k \cdot_{W} C = K \cdot_{W} C$
96	95	eleq1d	$⊢ k = K \to (k \cdot_{W} C \in N (U ∖ \{C\}) \leftrightarrow K \cdot_{W} C \in N (U ∖ \{C\}))$
97	96	notbid	$⊢ k = K \to (\neg k \cdot_{W} C \in N (U ∖ \{C\}) \leftrightarrow \neg K \cdot_{W} C \in N (U ∖ \{C\}))$
98	94 97	rspc2va	$⊢ ((C \in U \land K \in (F ∖ \{O\})) \land \forall c \in U \forall k \in (F ∖ \{O\}) \neg k \cdot_{W} c \in N (U ∖ \{c\})) \to \neg K \cdot_{W} C \in N (U ∖ \{C\})$
99	82 83 88 98	syl21anc	$⊢ (((φ \land x \in N (U ∖ \{C\})) \land y \in N (V)) \land K \cdot_{W} C = x +_{W} y) \to \neg K \cdot_{W} C \in N (U ∖ \{C\})$
100	81 99	pm2.21fal	$⊢ (((φ \land x \in N (U ∖ \{C\})) \land y \in N (V)) \land K \cdot_{W} C = x +_{W} y) \to ⊥$
101	23	ssdifssd	$⊢ φ \to U ∖ \{C\} \subseteq {Base}_{W}$
102	21 58 1	lspcl	$⊢ (W \in LMod \land U ∖ \{C\} \subseteq {Base}_{W}) \to N (U ∖ \{C\}) \in LSubSp (W)$
103	14 101 102	syl2anc	$⊢ φ \to N (U ∖ \{C\}) \in LSubSp (W)$
104	58	lsssubg	$⊢ (W \in LMod \land N (U ∖ \{C\}) \in LSubSp (W)) \to N (U ∖ \{C\}) \in SubGrp (W)$
105	14 103 104	syl2anc	$⊢ φ \to N (U ∖ \{C\}) \in SubGrp (W)$
106	21 58 1	lspcl	$⊢ (W \in LMod \land V \subseteq {Base}_{W}) \to N (V) \in LSubSp (W)$
107	14 35 106	syl2anc	$⊢ φ \to N (V) \in LSubSp (W)$
108	58	lsssubg	$⊢ (W \in LMod \land N (V) \in LSubSp (W)) \to N (V) \in SubGrp (W)$
109	14 107 108	syl2anc	$⊢ φ \to N (V) \in SubGrp (W)$
110		eqid	$⊢ LSSum (W) = LSSum (W)$
111	21 1 110	lsmsp2	$⊢ (W \in LMod \land U ∖ \{C\} \subseteq {Base}_{W} \land V \subseteq {Base}_{W}) \to N (U ∖ \{C\}) LSSum (W) N (V) = N ((U ∖ \{C\}) \cup V)$
112	14 101 35 111	syl3anc	$⊢ φ \to N (U ∖ \{C\}) LSSum (W) N (V) = N ((U ∖ \{C\}) \cup V)$
113	65	adantr	$⊢ (φ \land C \in V) \to C \in N (U)$
114	21 1	lspssid	$⊢ (W \in LMod \land V \subseteq {Base}_{W}) \to V \subseteq N (V)$
115	14 35 114	syl2anc	$⊢ φ \to V \subseteq N (V)$
116	115	sselda	$⊢ (φ \land C \in V) \to C \in N (V)$
117	113 116	elind	$⊢ (φ \land C \in V) \to C \in (N (U) \cap N (V))$
118	6	adantr	$⊢ (φ \land C \in V) \to N (U) \cap N (V) = \{\underset{˙}{0}\}$
119	117 118	eleqtrd	$⊢ (φ \land C \in V) \to C \in \{\underset{˙}{0}\}$
120		elsni	$⊢ C \in \{\underset{˙}{0}\} \to C = \underset{˙}{0}$
121	119 120	syl	$⊢ (φ \land C \in V) \to C = \underset{˙}{0}$
122	2	0nellinds	$⊢ (W \in LVec \land U \in LIndS (W)) \to \neg \underset{˙}{0} \in U$
123	3 4 122	syl2anc	$⊢ φ \to \neg \underset{˙}{0} \in U$
124		nelne2	$⊢ (C \in U \land \neg \underset{˙}{0} \in U) \to C \neq \underset{˙}{0}$
125	9 123 124	syl2anc	$⊢ φ \to C \neq \underset{˙}{0}$
126	125	adantr	$⊢ (φ \land C \in V) \to C \neq \underset{˙}{0}$
127	126	neneqd	$⊢ (φ \land C \in V) \to \neg C = \underset{˙}{0}$
128	121 127	pm2.65da	$⊢ φ \to \neg C \in V$
129		disjsn	$⊢ V \cap \{C\} = \emptyset \leftrightarrow \neg C \in V$
130	128 129	sylibr	$⊢ φ \to V \cap \{C\} = \emptyset$
131		undif4	$⊢ V \cap \{C\} = \emptyset \to V \cup (U ∖ \{C\}) = (V \cup U) ∖ \{C\}$
132	130 131	syl	$⊢ φ \to V \cup (U ∖ \{C\}) = (V \cup U) ∖ \{C\}$
133		uncom	$⊢ (U ∖ \{C\}) \cup V = V \cup (U ∖ \{C\})$
134		uncom	$⊢ U \cup V = V \cup U$
135	134	difeq1i	$⊢ (U \cup V) ∖ \{C\} = (V \cup U) ∖ \{C\}$
136	132 133 135	3eqtr4g	$⊢ φ \to (U ∖ \{C\}) \cup V = (U \cup V) ∖ \{C\}$
137	136	fveq2d	$⊢ φ \to N ((U ∖ \{C\}) \cup V) = N ((U \cup V) ∖ \{C\})$
138	112 137	eqtrd	$⊢ φ \to N (U ∖ \{C\}) LSSum (W) N (V) = N ((U \cup V) ∖ \{C\})$
139	11 138	eleqtrrd	$⊢ φ \to K \cdot_{W} C \in (N (U ∖ \{C\}) LSSum (W) N (V))$
140	41 110	lsmelval	$⊢ (N (U ∖ \{C\}) \in SubGrp (W) \land N (V) \in SubGrp (W)) \to (K \cdot_{W} C \in (N (U ∖ \{C\}) LSSum (W) N (V)) \leftrightarrow \exists x \in N (U ∖ \{C\}) \exists y \in N (V) K \cdot_{W} C = x +_{W} y)$
141	140	biimpa	$⊢ ((N (U ∖ \{C\}) \in SubGrp (W) \land N (V) \in SubGrp (W)) \land K \cdot_{W} C \in (N (U ∖ \{C\}) LSSum (W) N (V))) \to \exists x \in N (U ∖ \{C\}) \exists y \in N (V) K \cdot_{W} C = x +_{W} y$
142	105 109 139 141	syl21anc	$⊢ φ \to \exists x \in N (U ∖ \{C\}) \exists y \in N (V) K \cdot_{W} C = x +_{W} y$
143	100 142	r19.29vva	$⊢ φ \to ⊥$

Metamath Proof Explorer

Theorem lindsunlem

Proof