lspsolvlem

	Ref	Expression
Hypotheses	lspsolv.v	$⊢ V = {Base}_{W}$
	lspsolv.s	$⊢ S = LSubSp (W)$
	lspsolv.n	$⊢ N = LSpan (W)$
	lspsolv.f	$⊢ F = Scalar (W)$
	lspsolv.b	$⊢ B = {Base}_{F}$
	lspsolv.p	$⊢ \underset{˙}{+} = +_{W}$
	lspsolv.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	lspsolv.q	$⊢ Q = \{z \in V \| \exists r \in B z \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A)\}$
	lspsolv.w	$⊢ φ \to W \in LMod$
	lspsolv.ss	$⊢ φ \to A \subseteq V$
	lspsolv.y	$⊢ φ \to Y \in V$
	lspsolv.x	$⊢ φ \to X \in N (A \cup \{Y\})$
Assertion	lspsolvlem	$⊢ φ \to \exists r \in B X \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A)$

Proof

Step	Hyp	Ref	Expression
1		lspsolv.v	$⊢ V = {Base}_{W}$
2		lspsolv.s	$⊢ S = LSubSp (W)$
3		lspsolv.n	$⊢ N = LSpan (W)$
4		lspsolv.f	$⊢ F = Scalar (W)$
5		lspsolv.b	$⊢ B = {Base}_{F}$
6		lspsolv.p	$⊢ \underset{˙}{+} = +_{W}$
7		lspsolv.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
8		lspsolv.q	$⊢ Q = \{z \in V \| \exists r \in B z \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A)\}$
9		lspsolv.w	$⊢ φ \to W \in LMod$
10		lspsolv.ss	$⊢ φ \to A \subseteq V$
11		lspsolv.y	$⊢ φ \to Y \in V$
12		lspsolv.x	$⊢ φ \to X \in N (A \cup \{Y\})$
13	8	ssrab3	$⊢ Q \subseteq V$
14	13	a1i	$⊢ φ \to Q \subseteq V$
15	9	adantr	$⊢ (φ \land z \in A) \to W \in LMod$
16		eqid	$⊢ 0_{F} = 0_{F}$
17	4 5 16	lmod0cl	$⊢ W \in LMod \to 0_{F} \in B$
18	15 17	syl	$⊢ (φ \land z \in A) \to 0_{F} \in B$
19		eqid	$⊢ 0_{W} = 0_{W}$
20	1 4 7 16 19	lmod0vs	$⊢ (W \in LMod \land Y \in V) \to 0_{F} \underset{˙}{\cdot} Y = 0_{W}$
21	9 11 20	syl2anc	$⊢ φ \to 0_{F} \underset{˙}{\cdot} Y = 0_{W}$
22	21	adantr	$⊢ (φ \land z \in A) \to 0_{F} \underset{˙}{\cdot} Y = 0_{W}$
23	22	oveq2d	$⊢ (φ \land z \in A) \to z \underset{˙}{+} (0_{F} \underset{˙}{\cdot} Y) = z \underset{˙}{+} 0_{W}$
24	10	sselda	$⊢ (φ \land z \in A) \to z \in V$
25	1 6 19	lmod0vrid	$⊢ (W \in LMod \land z \in V) \to z \underset{˙}{+} 0_{W} = z$
26	15 24 25	syl2anc	$⊢ (φ \land z \in A) \to z \underset{˙}{+} 0_{W} = z$
27	23 26	eqtrd	$⊢ (φ \land z \in A) \to z \underset{˙}{+} (0_{F} \underset{˙}{\cdot} Y) = z$
28	1 3	lspssid	$⊢ (W \in LMod \land A \subseteq V) \to A \subseteq N (A)$
29	9 10 28	syl2anc	$⊢ φ \to A \subseteq N (A)$
30	29	sselda	$⊢ (φ \land z \in A) \to z \in N (A)$
31	27 30	eqeltrd	$⊢ (φ \land z \in A) \to z \underset{˙}{+} (0_{F} \underset{˙}{\cdot} Y) \in N (A)$
32		oveq1	$⊢ r = 0_{F} \to r \underset{˙}{\cdot} Y = 0_{F} \underset{˙}{\cdot} Y$
33	32	oveq2d	$⊢ r = 0_{F} \to z \underset{˙}{+} (r \underset{˙}{\cdot} Y) = z \underset{˙}{+} (0_{F} \underset{˙}{\cdot} Y)$
34	33	eleq1d	$⊢ r = 0_{F} \to (z \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A) \leftrightarrow z \underset{˙}{+} (0_{F} \underset{˙}{\cdot} Y) \in N (A))$
35	34	rspcev	$⊢ (0_{F} \in B \land z \underset{˙}{+} (0_{F} \underset{˙}{\cdot} Y) \in N (A)) \to \exists r \in B z \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A)$
36	18 31 35	syl2anc	$⊢ (φ \land z \in A) \to \exists r \in B z \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A)$
37	10 36	ssrabdv	$⊢ φ \to A \subseteq \{z \in V \| \exists r \in B z \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A)\}$
38	37 8	sseqtrrdi	$⊢ φ \to A \subseteq Q$
39	4	lmodfgrp	$⊢ W \in LMod \to F \in Grp$
40	9 39	syl	$⊢ φ \to F \in Grp$
41		eqid	$⊢ 1_{F} = 1_{F}$
42	4 5 41	lmod1cl	$⊢ W \in LMod \to 1_{F} \in B$
43	9 42	syl	$⊢ φ \to 1_{F} \in B$
44		eqid	$⊢ {inv}_{g} (F) = {inv}_{g} (F)$
45	5 44	grpinvcl	$⊢ (F \in Grp \land 1_{F} \in B) \to {inv}_{g} (F) (1_{F}) \in B$
46	40 43 45	syl2anc	$⊢ φ \to {inv}_{g} (F) (1_{F}) \in B$
47		eqid	$⊢ {inv}_{g} (W) = {inv}_{g} (W)$
48	1 47 4 7 41 44	lmodvneg1	$⊢ (W \in LMod \land Y \in V) \to {inv}_{g} (F) (1_{F}) \underset{˙}{\cdot} Y = {inv}_{g} (W) (Y)$
49	9 11 48	syl2anc	$⊢ φ \to {inv}_{g} (F) (1_{F}) \underset{˙}{\cdot} Y = {inv}_{g} (W) (Y)$
50	49	oveq2d	$⊢ φ \to Y \underset{˙}{+} ({inv}_{g} (F) (1_{F}) \underset{˙}{\cdot} Y) = Y \underset{˙}{+} {inv}_{g} (W) (Y)$
51		lmodgrp	$⊢ W \in LMod \to W \in Grp$
52	9 51	syl	$⊢ φ \to W \in Grp$
53	1 6 19 47	grprinv	$⊢ (W \in Grp \land Y \in V) \to Y \underset{˙}{+} {inv}_{g} (W) (Y) = 0_{W}$
54	52 11 53	syl2anc	$⊢ φ \to Y \underset{˙}{+} {inv}_{g} (W) (Y) = 0_{W}$
55	50 54	eqtrd	$⊢ φ \to Y \underset{˙}{+} ({inv}_{g} (F) (1_{F}) \underset{˙}{\cdot} Y) = 0_{W}$
56	1 2 3	lspcl	$⊢ (W \in LMod \land A \subseteq V) \to N (A) \in S$
57	9 10 56	syl2anc	$⊢ φ \to N (A) \in S$
58	19 2	lss0cl	$⊢ (W \in LMod \land N (A) \in S) \to 0_{W} \in N (A)$
59	9 57 58	syl2anc	$⊢ φ \to 0_{W} \in N (A)$
60	55 59	eqeltrd	$⊢ φ \to Y \underset{˙}{+} ({inv}_{g} (F) (1_{F}) \underset{˙}{\cdot} Y) \in N (A)$
61		oveq1	$⊢ r = {inv}_{g} (F) (1_{F}) \to r \underset{˙}{\cdot} Y = {inv}_{g} (F) (1_{F}) \underset{˙}{\cdot} Y$
62	61	oveq2d	$⊢ r = {inv}_{g} (F) (1_{F}) \to Y \underset{˙}{+} (r \underset{˙}{\cdot} Y) = Y \underset{˙}{+} ({inv}_{g} (F) (1_{F}) \underset{˙}{\cdot} Y)$
63	62	eleq1d	$⊢ r = {inv}_{g} (F) (1_{F}) \to (Y \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A) \leftrightarrow Y \underset{˙}{+} ({inv}_{g} (F) (1_{F}) \underset{˙}{\cdot} Y) \in N (A))$
64	63	rspcev	$⊢ ({inv}_{g} (F) (1_{F}) \in B \land Y \underset{˙}{+} ({inv}_{g} (F) (1_{F}) \underset{˙}{\cdot} Y) \in N (A)) \to \exists r \in B Y \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A)$
65	46 60 64	syl2anc	$⊢ φ \to \exists r \in B Y \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A)$
66		oveq1	$⊢ z = Y \to z \underset{˙}{+} (r \underset{˙}{\cdot} Y) = Y \underset{˙}{+} (r \underset{˙}{\cdot} Y)$
67	66	eleq1d	$⊢ z = Y \to (z \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A) \leftrightarrow Y \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A))$
68	67	rexbidv	$⊢ z = Y \to (\exists r \in B z \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A) \leftrightarrow \exists r \in B Y \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A))$
69	68 8	elrab2	$⊢ Y \in Q \leftrightarrow (Y \in V \land \exists r \in B Y \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A))$
70	11 65 69	sylanbrc	$⊢ φ \to Y \in Q$
71	70	snssd	$⊢ φ \to \{Y\} \subseteq Q$
72	38 71	unssd	$⊢ φ \to A \cup \{Y\} \subseteq Q$
73	1 3	lspss	$⊢ (W \in LMod \land Q \subseteq V \land A \cup \{Y\} \subseteq Q) \to N (A \cup \{Y\}) \subseteq N (Q)$
74	9 14 72 73	syl3anc	$⊢ φ \to N (A \cup \{Y\}) \subseteq N (Q)$
75	4	a1i	$⊢ φ \to F = Scalar (W)$
76	5	a1i	$⊢ φ \to B = {Base}_{F}$
77	1	a1i	$⊢ φ \to V = {Base}_{W}$
78	6	a1i	$⊢ φ \to \underset{˙}{+} = +_{W}$
79	7	a1i	$⊢ φ \to \underset{˙}{\cdot} = \cdot_{W}$
80	2	a1i	$⊢ φ \to S = LSubSp (W)$
81	70	ne0d	$⊢ φ \to Q \neq \emptyset$
82		oveq1	$⊢ z = x \to z \underset{˙}{+} (r \underset{˙}{\cdot} Y) = x \underset{˙}{+} (r \underset{˙}{\cdot} Y)$
83	82	eleq1d	$⊢ z = x \to (z \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A) \leftrightarrow x \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A))$
84	83	rexbidv	$⊢ z = x \to (\exists r \in B z \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A) \leftrightarrow \exists r \in B x \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A))$
85		oveq1	$⊢ r = s \to r \underset{˙}{\cdot} Y = s \underset{˙}{\cdot} Y$
86	85	oveq2d	$⊢ r = s \to x \underset{˙}{+} (r \underset{˙}{\cdot} Y) = x \underset{˙}{+} (s \underset{˙}{\cdot} Y)$
87	86	eleq1d	$⊢ r = s \to (x \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A) \leftrightarrow x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A))$
88	87	cbvrexvw	$⊢ \exists r \in B x \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A) \leftrightarrow \exists s \in B x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A)$
89	84 88	bitrdi	$⊢ z = x \to (\exists r \in B z \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A) \leftrightarrow \exists s \in B x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A))$
90	89 8	elrab2	$⊢ x \in Q \leftrightarrow (x \in V \land \exists s \in B x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A))$
91		oveq1	$⊢ z = y \to z \underset{˙}{+} (r \underset{˙}{\cdot} Y) = y \underset{˙}{+} (r \underset{˙}{\cdot} Y)$
92	91	eleq1d	$⊢ z = y \to (z \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A) \leftrightarrow y \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A))$
93	92	rexbidv	$⊢ z = y \to (\exists r \in B z \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A) \leftrightarrow \exists r \in B y \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A))$
94		oveq1	$⊢ r = t \to r \underset{˙}{\cdot} Y = t \underset{˙}{\cdot} Y$
95	94	oveq2d	$⊢ r = t \to y \underset{˙}{+} (r \underset{˙}{\cdot} Y) = y \underset{˙}{+} (t \underset{˙}{\cdot} Y)$
96	95	eleq1d	$⊢ r = t \to (y \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A) \leftrightarrow y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))$
97	96	cbvrexvw	$⊢ \exists r \in B y \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A) \leftrightarrow \exists t \in B y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A)$
98	93 97	bitrdi	$⊢ z = y \to (\exists r \in B z \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A) \leftrightarrow \exists t \in B y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))$
99	98 8	elrab2	$⊢ y \in Q \leftrightarrow (y \in V \land \exists t \in B y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))$
100	90 99	anbi12i	$⊢ (x \in Q \land y \in Q) \leftrightarrow ((x \in V \land \exists s \in B x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A)) \land (y \in V \land \exists t \in B y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A)))$
101		an4	$⊢ ((x \in V \land \exists s \in B x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A)) \land (y \in V \land \exists t \in B y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))) \leftrightarrow ((x \in V \land y \in V) \land (\exists s \in B x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land \exists t \in B y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A)))$
102	100 101	bitri	$⊢ (x \in Q \land y \in Q) \leftrightarrow ((x \in V \land y \in V) \land (\exists s \in B x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land \exists t \in B y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A)))$
103		reeanv	$⊢ \exists s \in B \exists t \in B (x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A)) \leftrightarrow (\exists s \in B x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land \exists t \in B y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))$
104		simp1ll	$⊢ (((φ \land a \in B) \land (x \in V \land y \in V)) \land (s \in B \land t \in B) \land (x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))) \to φ$
105	104 9	syl	$⊢ (((φ \land a \in B) \land (x \in V \land y \in V)) \land (s \in B \land t \in B) \land (x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))) \to W \in LMod$
106		simp1lr	$⊢ (((φ \land a \in B) \land (x \in V \land y \in V)) \land (s \in B \land t \in B) \land (x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))) \to a \in B$
107		simp1rl	$⊢ (((φ \land a \in B) \land (x \in V \land y \in V)) \land (s \in B \land t \in B) \land (x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))) \to x \in V$
108	1 4 7 5	lmodvscl	$⊢ (W \in LMod \land a \in B \land x \in V) \to a \underset{˙}{\cdot} x \in V$
109	105 106 107 108	syl3anc	$⊢ (((φ \land a \in B) \land (x \in V \land y \in V)) \land (s \in B \land t \in B) \land (x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))) \to a \underset{˙}{\cdot} x \in V$
110		simp1rr	$⊢ (((φ \land a \in B) \land (x \in V \land y \in V)) \land (s \in B \land t \in B) \land (x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))) \to y \in V$
111	1 6	lmodvacl	$⊢ (W \in LMod \land a \underset{˙}{\cdot} x \in V \land y \in V) \to (a \underset{˙}{\cdot} x) \underset{˙}{+} y \in V$
112	105 109 110 111	syl3anc	$⊢ (((φ \land a \in B) \land (x \in V \land y \in V)) \land (s \in B \land t \in B) \land (x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))) \to (a \underset{˙}{\cdot} x) \underset{˙}{+} y \in V$
113		simp2l	$⊢ (((φ \land a \in B) \land (x \in V \land y \in V)) \land (s \in B \land t \in B) \land (x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))) \to s \in B$
114		eqid	$⊢ \cdot_{F} = \cdot_{F}$
115	4 5 114	lmodmcl	$⊢ (W \in LMod \land a \in B \land s \in B) \to a \cdot_{F} s \in B$
116	105 106 113 115	syl3anc	$⊢ (((φ \land a \in B) \land (x \in V \land y \in V)) \land (s \in B \land t \in B) \land (x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))) \to a \cdot_{F} s \in B$
117		simp2r	$⊢ (((φ \land a \in B) \land (x \in V \land y \in V)) \land (s \in B \land t \in B) \land (x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))) \to t \in B$
118		eqid	$⊢ +_{F} = +_{F}$
119	4 5 118	lmodacl	$⊢ (W \in LMod \land a \cdot_{F} s \in B \land t \in B) \to (a \cdot_{F} s) +_{F} t \in B$
120	105 116 117 119	syl3anc	$⊢ (((φ \land a \in B) \land (x \in V \land y \in V)) \land (s \in B \land t \in B) \land (x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))) \to (a \cdot_{F} s) +_{F} t \in B$
121	104 11	syl	$⊢ (((φ \land a \in B) \land (x \in V \land y \in V)) \land (s \in B \land t \in B) \land (x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))) \to Y \in V$
122	1 4 7 5	lmodvscl	$⊢ (W \in LMod \land s \in B \land Y \in V) \to s \underset{˙}{\cdot} Y \in V$
123	105 113 121 122	syl3anc	$⊢ (((φ \land a \in B) \land (x \in V \land y \in V)) \land (s \in B \land t \in B) \land (x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))) \to s \underset{˙}{\cdot} Y \in V$
124	1 4 7 5	lmodvscl	$⊢ (W \in LMod \land a \in B \land s \underset{˙}{\cdot} Y \in V) \to a \underset{˙}{\cdot} (s \underset{˙}{\cdot} Y) \in V$
125	105 106 123 124	syl3anc	$⊢ (((φ \land a \in B) \land (x \in V \land y \in V)) \land (s \in B \land t \in B) \land (x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))) \to a \underset{˙}{\cdot} (s \underset{˙}{\cdot} Y) \in V$
126	1 4 7 5	lmodvscl	$⊢ (W \in LMod \land t \in B \land Y \in V) \to t \underset{˙}{\cdot} Y \in V$
127	105 117 121 126	syl3anc	$⊢ (((φ \land a \in B) \land (x \in V \land y \in V)) \land (s \in B \land t \in B) \land (x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))) \to t \underset{˙}{\cdot} Y \in V$
128	1 6	lmod4	$⊢ (W \in LMod \land (a \underset{˙}{\cdot} x \in V \land y \in V) \land (a \underset{˙}{\cdot} (s \underset{˙}{\cdot} Y) \in V \land t \underset{˙}{\cdot} Y \in V)) \to ((a \underset{˙}{\cdot} x) \underset{˙}{+} y) \underset{˙}{+} ((a \underset{˙}{\cdot} (s \underset{˙}{\cdot} Y)) \underset{˙}{+} (t \underset{˙}{\cdot} Y)) = ((a \underset{˙}{\cdot} x) \underset{˙}{+} (a \underset{˙}{\cdot} (s \underset{˙}{\cdot} Y))) \underset{˙}{+} (y \underset{˙}{+} (t \underset{˙}{\cdot} Y))$
129	105 109 110 125 127 128	syl122anc	$⊢ (((φ \land a \in B) \land (x \in V \land y \in V)) \land (s \in B \land t \in B) \land (x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))) \to ((a \underset{˙}{\cdot} x) \underset{˙}{+} y) \underset{˙}{+} ((a \underset{˙}{\cdot} (s \underset{˙}{\cdot} Y)) \underset{˙}{+} (t \underset{˙}{\cdot} Y)) = ((a \underset{˙}{\cdot} x) \underset{˙}{+} (a \underset{˙}{\cdot} (s \underset{˙}{\cdot} Y))) \underset{˙}{+} (y \underset{˙}{+} (t \underset{˙}{\cdot} Y))$
130	1 6 4 7 5 118	lmodvsdir	$⊢ (W \in LMod \land (a \cdot_{F} s \in B \land t \in B \land Y \in V)) \to ((a \cdot_{F} s) +_{F} t) \underset{˙}{\cdot} Y = ((a \cdot_{F} s) \underset{˙}{\cdot} Y) \underset{˙}{+} (t \underset{˙}{\cdot} Y)$
131	105 116 117 121 130	syl13anc	$⊢ (((φ \land a \in B) \land (x \in V \land y \in V)) \land (s \in B \land t \in B) \land (x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))) \to ((a \cdot_{F} s) +_{F} t) \underset{˙}{\cdot} Y = ((a \cdot_{F} s) \underset{˙}{\cdot} Y) \underset{˙}{+} (t \underset{˙}{\cdot} Y)$
132	1 4 7 5 114	lmodvsass	$⊢ (W \in LMod \land (a \in B \land s \in B \land Y \in V)) \to (a \cdot_{F} s) \underset{˙}{\cdot} Y = a \underset{˙}{\cdot} (s \underset{˙}{\cdot} Y)$
133	105 106 113 121 132	syl13anc	$⊢ (((φ \land a \in B) \land (x \in V \land y \in V)) \land (s \in B \land t \in B) \land (x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))) \to (a \cdot_{F} s) \underset{˙}{\cdot} Y = a \underset{˙}{\cdot} (s \underset{˙}{\cdot} Y)$
134	133	oveq1d	$⊢ (((φ \land a \in B) \land (x \in V \land y \in V)) \land (s \in B \land t \in B) \land (x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))) \to ((a \cdot_{F} s) \underset{˙}{\cdot} Y) \underset{˙}{+} (t \underset{˙}{\cdot} Y) = (a \underset{˙}{\cdot} (s \underset{˙}{\cdot} Y)) \underset{˙}{+} (t \underset{˙}{\cdot} Y)$
135	131 134	eqtrd	$⊢ (((φ \land a \in B) \land (x \in V \land y \in V)) \land (s \in B \land t \in B) \land (x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))) \to ((a \cdot_{F} s) +_{F} t) \underset{˙}{\cdot} Y = (a \underset{˙}{\cdot} (s \underset{˙}{\cdot} Y)) \underset{˙}{+} (t \underset{˙}{\cdot} Y)$
136	135	oveq2d	$⊢ (((φ \land a \in B) \land (x \in V \land y \in V)) \land (s \in B \land t \in B) \land (x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))) \to ((a \underset{˙}{\cdot} x) \underset{˙}{+} y) \underset{˙}{+} (((a \cdot_{F} s) +_{F} t) \underset{˙}{\cdot} Y) = ((a \underset{˙}{\cdot} x) \underset{˙}{+} y) \underset{˙}{+} ((a \underset{˙}{\cdot} (s \underset{˙}{\cdot} Y)) \underset{˙}{+} (t \underset{˙}{\cdot} Y))$
137	1 6 4 7 5	lmodvsdi	$⊢ (W \in LMod \land (a \in B \land x \in V \land s \underset{˙}{\cdot} Y \in V)) \to a \underset{˙}{\cdot} (x \underset{˙}{+} (s \underset{˙}{\cdot} Y)) = (a \underset{˙}{\cdot} x) \underset{˙}{+} (a \underset{˙}{\cdot} (s \underset{˙}{\cdot} Y))$
138	105 106 107 123 137	syl13anc	$⊢ (((φ \land a \in B) \land (x \in V \land y \in V)) \land (s \in B \land t \in B) \land (x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))) \to a \underset{˙}{\cdot} (x \underset{˙}{+} (s \underset{˙}{\cdot} Y)) = (a \underset{˙}{\cdot} x) \underset{˙}{+} (a \underset{˙}{\cdot} (s \underset{˙}{\cdot} Y))$
139	138	oveq1d	$⊢ (((φ \land a \in B) \land (x \in V \land y \in V)) \land (s \in B \land t \in B) \land (x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))) \to (a \underset{˙}{\cdot} (x \underset{˙}{+} (s \underset{˙}{\cdot} Y))) \underset{˙}{+} (y \underset{˙}{+} (t \underset{˙}{\cdot} Y)) = ((a \underset{˙}{\cdot} x) \underset{˙}{+} (a \underset{˙}{\cdot} (s \underset{˙}{\cdot} Y))) \underset{˙}{+} (y \underset{˙}{+} (t \underset{˙}{\cdot} Y))$
140	129 136 139	3eqtr4d	$⊢ (((φ \land a \in B) \land (x \in V \land y \in V)) \land (s \in B \land t \in B) \land (x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))) \to ((a \underset{˙}{\cdot} x) \underset{˙}{+} y) \underset{˙}{+} (((a \cdot_{F} s) +_{F} t) \underset{˙}{\cdot} Y) = (a \underset{˙}{\cdot} (x \underset{˙}{+} (s \underset{˙}{\cdot} Y))) \underset{˙}{+} (y \underset{˙}{+} (t \underset{˙}{\cdot} Y))$
141	104 57	syl	$⊢ (((φ \land a \in B) \land (x \in V \land y \in V)) \land (s \in B \land t \in B) \land (x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))) \to N (A) \in S$
142		simp3l	$⊢ (((φ \land a \in B) \land (x \in V \land y \in V)) \land (s \in B \land t \in B) \land (x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))) \to x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A)$
143		simp3r	$⊢ (((φ \land a \in B) \land (x \in V \land y \in V)) \land (s \in B \land t \in B) \land (x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))) \to y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A)$
144	4 5 6 7 2	lsscl	$⊢ (N (A) \in S \land (a \in B \land x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))) \to (a \underset{˙}{\cdot} (x \underset{˙}{+} (s \underset{˙}{\cdot} Y))) \underset{˙}{+} (y \underset{˙}{+} (t \underset{˙}{\cdot} Y)) \in N (A)$
145	141 106 142 143 144	syl13anc	$⊢ (((φ \land a \in B) \land (x \in V \land y \in V)) \land (s \in B \land t \in B) \land (x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))) \to (a \underset{˙}{\cdot} (x \underset{˙}{+} (s \underset{˙}{\cdot} Y))) \underset{˙}{+} (y \underset{˙}{+} (t \underset{˙}{\cdot} Y)) \in N (A)$
146	140 145	eqeltrd	$⊢ (((φ \land a \in B) \land (x \in V \land y \in V)) \land (s \in B \land t \in B) \land (x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))) \to ((a \underset{˙}{\cdot} x) \underset{˙}{+} y) \underset{˙}{+} (((a \cdot_{F} s) +_{F} t) \underset{˙}{\cdot} Y) \in N (A)$
147		oveq1	$⊢ r = (a \cdot_{F} s) +_{F} t \to r \underset{˙}{\cdot} Y = ((a \cdot_{F} s) +_{F} t) \underset{˙}{\cdot} Y$
148	147	oveq2d	$⊢ r = (a \cdot_{F} s) +_{F} t \to ((a \underset{˙}{\cdot} x) \underset{˙}{+} y) \underset{˙}{+} (r \underset{˙}{\cdot} Y) = ((a \underset{˙}{\cdot} x) \underset{˙}{+} y) \underset{˙}{+} (((a \cdot_{F} s) +_{F} t) \underset{˙}{\cdot} Y)$
149	148	eleq1d	$⊢ r = (a \cdot_{F} s) +_{F} t \to (((a \underset{˙}{\cdot} x) \underset{˙}{+} y) \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A) \leftrightarrow ((a \underset{˙}{\cdot} x) \underset{˙}{+} y) \underset{˙}{+} (((a \cdot_{F} s) +_{F} t) \underset{˙}{\cdot} Y) \in N (A))$
150	149	rspcev	$⊢ ((a \cdot_{F} s) +_{F} t \in B \land ((a \underset{˙}{\cdot} x) \underset{˙}{+} y) \underset{˙}{+} (((a \cdot_{F} s) +_{F} t) \underset{˙}{\cdot} Y) \in N (A)) \to \exists r \in B ((a \underset{˙}{\cdot} x) \underset{˙}{+} y) \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A)$
151	120 146 150	syl2anc	$⊢ (((φ \land a \in B) \land (x \in V \land y \in V)) \land (s \in B \land t \in B) \land (x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))) \to \exists r \in B ((a \underset{˙}{\cdot} x) \underset{˙}{+} y) \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A)$
152		oveq1	$⊢ z = (a \underset{˙}{\cdot} x) \underset{˙}{+} y \to z \underset{˙}{+} (r \underset{˙}{\cdot} Y) = ((a \underset{˙}{\cdot} x) \underset{˙}{+} y) \underset{˙}{+} (r \underset{˙}{\cdot} Y)$
153	152	eleq1d	$⊢ z = (a \underset{˙}{\cdot} x) \underset{˙}{+} y \to (z \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A) \leftrightarrow ((a \underset{˙}{\cdot} x) \underset{˙}{+} y) \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A))$
154	153	rexbidv	$⊢ z = (a \underset{˙}{\cdot} x) \underset{˙}{+} y \to (\exists r \in B z \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A) \leftrightarrow \exists r \in B ((a \underset{˙}{\cdot} x) \underset{˙}{+} y) \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A))$
155	154 8	elrab2	$⊢ (a \underset{˙}{\cdot} x) \underset{˙}{+} y \in Q \leftrightarrow ((a \underset{˙}{\cdot} x) \underset{˙}{+} y \in V \land \exists r \in B ((a \underset{˙}{\cdot} x) \underset{˙}{+} y) \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A))$
156	112 151 155	sylanbrc	$⊢ (((φ \land a \in B) \land (x \in V \land y \in V)) \land (s \in B \land t \in B) \land (x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))) \to (a \underset{˙}{\cdot} x) \underset{˙}{+} y \in Q$
157	156	3exp	$⊢ ((φ \land a \in B) \land (x \in V \land y \in V)) \to ((s \in B \land t \in B) \to ((x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A)) \to (a \underset{˙}{\cdot} x) \underset{˙}{+} y \in Q))$
158	157	rexlimdvv	$⊢ ((φ \land a \in B) \land (x \in V \land y \in V)) \to (\exists s \in B \exists t \in B (x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A)) \to (a \underset{˙}{\cdot} x) \underset{˙}{+} y \in Q)$
159	103 158	syl5bir	$⊢ ((φ \land a \in B) \land (x \in V \land y \in V)) \to ((\exists s \in B x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land \exists t \in B y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A)) \to (a \underset{˙}{\cdot} x) \underset{˙}{+} y \in Q)$
160	159	expimpd	$⊢ (φ \land a \in B) \to (((x \in V \land y \in V) \land (\exists s \in B x \underset{˙}{+} (s \underset{˙}{\cdot} Y) \in N (A) \land \exists t \in B y \underset{˙}{+} (t \underset{˙}{\cdot} Y) \in N (A))) \to (a \underset{˙}{\cdot} x) \underset{˙}{+} y \in Q)$
161	102 160	syl5bi	$⊢ (φ \land a \in B) \to ((x \in Q \land y \in Q) \to (a \underset{˙}{\cdot} x) \underset{˙}{+} y \in Q)$
162	161	exp4b	$⊢ φ \to (a \in B \to (x \in Q \to (y \in Q \to (a \underset{˙}{\cdot} x) \underset{˙}{+} y \in Q)))$
163	162	3imp2	$⊢ (φ \land (a \in B \land x \in Q \land y \in Q)) \to (a \underset{˙}{\cdot} x) \underset{˙}{+} y \in Q$
164	75 76 77 78 79 80 14 81 163	islssd	$⊢ φ \to Q \in S$
165	2 3	lspid	$⊢ (W \in LMod \land Q \in S) \to N (Q) = Q$
166	9 164 165	syl2anc	$⊢ φ \to N (Q) = Q$
167	74 166	sseqtrd	$⊢ φ \to N (A \cup \{Y\}) \subseteq Q$
168	167 12	sseldd	$⊢ φ \to X \in Q$
169		oveq1	$⊢ z = X \to z \underset{˙}{+} (r \underset{˙}{\cdot} Y) = X \underset{˙}{+} (r \underset{˙}{\cdot} Y)$
170	169	eleq1d	$⊢ z = X \to (z \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A) \leftrightarrow X \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A))$
171	170	rexbidv	$⊢ z = X \to (\exists r \in B z \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A) \leftrightarrow \exists r \in B X \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A))$
172	171 8	elrab2	$⊢ X \in Q \leftrightarrow (X \in V \land \exists r \in B X \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A))$
173	172	simprbi	$⊢ X \in Q \to \exists r \in B X \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A)$
174	168 173	syl	$⊢ φ \to \exists r \in B X \underset{˙}{+} (r \underset{˙}{\cdot} Y) \in N (A)$

Metamath Proof Explorer

Theorem lspsolvlem

Proof