Theorem baerlem5alem2

Description: Lemma for baerlem5a . (Contributed by NM, 9-Apr-2015)

	Ref	Expression
Hypotheses	baerlem3.v	$$⊢V={\mathrm{Base}}_W$$
	baerlem3.m	$$⊢\underset{\dot{}}{-}={-}_W$$
	baerlem3.o	$$⊢\underset{\dot{}}{0}=0_W$$
	baerlem3.s	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(W\right)$$
	baerlem3.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
	baerlem3.w	$$⊢\phi \to W\in \mathrm{LVec}$$
	baerlem3.x	$$⊢\phi \to X\in V$$
	baerlem3.c	$$⊢\phi \to \neg X\in N\left(\left\{Y,Z\right\}\right)$$
	baerlem3.d	$$⊢\phi \to N\left(\left\{Y\right\}\right)\ne N\left(\left\{Z\right\}\right)$$
	baerlem3.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	baerlem3.z	$$⊢\phi \to Z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	baerlem3.p	$$⊢\underset{\dot{}}{+}={+}_W$$
	baerlem3.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	baerlem3.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
	baerlem3.b	$$⊢B={\mathrm{Base}}_R$$
	baerlem3.a	$$⊢\underset{\dot{}}{⨣}={+}_R$$
	baerlem3.l	$$⊢L={-}_R$$
	baerlem3.q	$$⊢Q=0_R$$
	baerlem3.i	$$⊢I={inv}_g\left(R\right)$$
Assertion	baerlem5alem2	$$⊢\phi \to N\left(\left\{X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right\}\right)=\left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Z\right\}\right)\right)\cap \left(N\left(\left\{X\underset{\dot{}}{-}Z\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Y\right\}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		baerlem3.v	$$⊢V={\mathrm{Base}}_W$$
2		baerlem3.m	$$⊢\underset{\dot{}}{-}={-}_W$$
3		baerlem3.o	$$⊢\underset{\dot{}}{0}=0_W$$
4		baerlem3.s	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(W\right)$$
5		baerlem3.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
6		baerlem3.w	$$⊢\phi \to W\in \mathrm{LVec}$$
7		baerlem3.x	$$⊢\phi \to X\in V$$
8		baerlem3.c	$$⊢\phi \to \neg X\in N\left(\left\{Y,Z\right\}\right)$$
9		baerlem3.d	$$⊢\phi \to N\left(\left\{Y\right\}\right)\ne N\left(\left\{Z\right\}\right)$$
10		baerlem3.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
11		baerlem3.z	$$⊢\phi \to Z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
12		baerlem3.p	$$⊢\underset{\dot{}}{+}={+}_W$$
13		baerlem3.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
14		baerlem3.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
15		baerlem3.b	$$⊢B={\mathrm{Base}}_R$$
16		baerlem3.a	$$⊢\underset{\dot{}}{⨣}={+}_R$$
17		baerlem3.l	$$⊢L={-}_R$$
18		baerlem3.q	$$⊢Q=0_R$$
19		baerlem3.i	$$⊢I={inv}_g\left(R\right)$$
20		lveclmod	$$⊢W\in \mathrm{LVec}\to W\in \mathrm{LMod}$$
21	6 20	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
22		lmodabl	$$⊢W\in \mathrm{LMod}\to W\in \mathrm{Abel}$$
23	21 22	syl	$$⊢\phi \to W\in \mathrm{Abel}$$
24	10	eldifad	$$⊢\phi \to Y\in V$$
25	11	eldifad	$$⊢\phi \to Z\in V$$
26	1 12 2 23 7 24 25	ablsubsub4	$$⊢\phi \to \left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{-}Z=X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)$$
27	26	sneqd	$$⊢\phi \to \left\{\left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{-}Z\right\}=\left\{X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right\}$$
28	27	fveq2d	$$⊢\phi \to N\left(\left\{\left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{-}Z\right\}\right)=N\left(\left\{X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right\}\right)$$
29	1 2	lmodvsubcl	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\wedge Y\in V\right)\to X\underset{\dot{}}{-}Y\in V$$
30	21 7 24 29	syl3anc	$$⊢\phi \to X\underset{\dot{}}{-}Y\in V$$
31	1 2 4 5	lspsntrim	$$⊢\left(W\in \mathrm{LMod}\wedge X\underset{\dot{}}{-}Y\in V\wedge Z\in V\right)\to N\left(\left\{\left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{-}Z\right\}\right)\subseteq N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Z\right\}\right)$$
32	21 30 25 31	syl3anc	$$⊢\phi \to N\left(\left\{\left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{-}Z\right\}\right)\subseteq N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Z\right\}\right)$$
33	28 32	eqsstrrd	$$⊢\phi \to N\left(\left\{X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right\}\right)\subseteq N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Z\right\}\right)$$
34	1 2 23 7 25 24	ablsub32	$$⊢\phi \to \left(X\underset{\dot{}}{-}Z\right)\underset{\dot{}}{-}Y=\left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{-}Z$$
35	34 26	eqtrd	$$⊢\phi \to \left(X\underset{\dot{}}{-}Z\right)\underset{\dot{}}{-}Y=X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)$$
36	35	sneqd	$$⊢\phi \to \left\{\left(X\underset{\dot{}}{-}Z\right)\underset{\dot{}}{-}Y\right\}=\left\{X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right\}$$
37	36	fveq2d	$$⊢\phi \to N\left(\left\{\left(X\underset{\dot{}}{-}Z\right)\underset{\dot{}}{-}Y\right\}\right)=N\left(\left\{X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right\}\right)$$
38	1 2	lmodvsubcl	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\wedge Z\in V\right)\to X\underset{\dot{}}{-}Z\in V$$
39	21 7 25 38	syl3anc	$$⊢\phi \to X\underset{\dot{}}{-}Z\in V$$
40	1 2 4 5	lspsntrim	$$⊢\left(W\in \mathrm{LMod}\wedge X\underset{\dot{}}{-}Z\in V\wedge Y\in V\right)\to N\left(\left\{\left(X\underset{\dot{}}{-}Z\right)\underset{\dot{}}{-}Y\right\}\right)\subseteq N\left(\left\{X\underset{\dot{}}{-}Z\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Y\right\}\right)$$
41	21 39 24 40	syl3anc	$$⊢\phi \to N\left(\left\{\left(X\underset{\dot{}}{-}Z\right)\underset{\dot{}}{-}Y\right\}\right)\subseteq N\left(\left\{X\underset{\dot{}}{-}Z\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Y\right\}\right)$$
42	37 41	eqsstrrd	$$⊢\phi \to N\left(\left\{X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right\}\right)\subseteq N\left(\left\{X\underset{\dot{}}{-}Z\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Y\right\}\right)$$
43	33 42	ssind	$$⊢\phi \to N\left(\left\{X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right\}\right)\subseteq \left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Z\right\}\right)\right)\cap \left(N\left(\left\{X\underset{\dot{}}{-}Z\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Y\right\}\right)\right)$$
44		elin	$$⊢j\in \left(\left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Z\right\}\right)\right)\cap \left(N\left(\left\{X\underset{\dot{}}{-}Z\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Y\right\}\right)\right)\right)\leftrightarrow \left(j\in \left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Z\right\}\right)\right)\wedge j\in \left(N\left(\left\{X\underset{\dot{}}{-}Z\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Y\right\}\right)\right)\right)$$
45	1 12 14 15 13 4 5 21 30 25	lsmspsn	$$⊢\phi \to \left(j\in \left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Z\right\}\right)\right)\leftrightarrow \exists a\in B\exists b\in Bj=\left(a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\right)$$
46	1 12 14 15 13 4 5 21 39 24	lsmspsn	$$⊢\phi \to \left(j\in \left(N\left(\left\{X\underset{\dot{}}{-}Z\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Y\right\}\right)\right)\leftrightarrow \exists d\in B\exists e\in Bj=\left(d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Y\right)\right)$$
47	45 46	anbi12d	$$⊢\phi \to \left(\left(j\in \left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Z\right\}\right)\right)\wedge j\in \left(N\left(\left\{X\underset{\dot{}}{-}Z\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Y\right\}\right)\right)\right)\leftrightarrow \left(\exists a\in B\exists b\in Bj=\left(a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\wedge \exists d\in B\exists e\in Bj=\left(d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Y\right)\right)\right)$$
48	44 47	syl5bb	$$⊢\phi \to \left(j\in \left(\left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Z\right\}\right)\right)\cap \left(N\left(\left\{X\underset{\dot{}}{-}Z\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Y\right\}\right)\right)\right)\leftrightarrow \left(\exists a\in B\exists b\in Bj=\left(a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\wedge \exists d\in B\exists e\in Bj=\left(d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Y\right)\right)\right)$$
49		simp11	$$⊢\left(\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\right)\wedge \left(d\in B\wedge e\in B\right)\wedge j=\left(d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Y\right)\right)\to \phi$$
50	49 6	syl	$$⊢\left(\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\right)\wedge \left(d\in B\wedge e\in B\right)\wedge j=\left(d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Y\right)\right)\to W\in \mathrm{LVec}$$
51	49 7	syl	$$⊢\left(\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\right)\wedge \left(d\in B\wedge e\in B\right)\wedge j=\left(d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Y\right)\right)\to X\in V$$
52	49 8	syl	$$⊢\left(\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\right)\wedge \left(d\in B\wedge e\in B\right)\wedge j=\left(d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Y\right)\right)\to \neg X\in N\left(\left\{Y,Z\right\}\right)$$
53	49 9	syl	$$⊢\left(\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\right)\wedge \left(d\in B\wedge e\in B\right)\wedge j=\left(d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Y\right)\right)\to N\left(\left\{Y\right\}\right)\ne N\left(\left\{Z\right\}\right)$$
54	49 10	syl	$$⊢\left(\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\right)\wedge \left(d\in B\wedge e\in B\right)\wedge j=\left(d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Y\right)\right)\to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
55	49 11	syl	$$⊢\left(\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\right)\wedge \left(d\in B\wedge e\in B\right)\wedge j=\left(d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Y\right)\right)\to Z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
56		simp12l	$$⊢\left(\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\right)\wedge \left(d\in B\wedge e\in B\right)\wedge j=\left(d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Y\right)\right)\to a\in B$$
57		simp12r	$$⊢\left(\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\right)\wedge \left(d\in B\wedge e\in B\right)\wedge j=\left(d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Y\right)\right)\to b\in B$$
58		simp2l	$$⊢\left(\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\right)\wedge \left(d\in B\wedge e\in B\right)\wedge j=\left(d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Y\right)\right)\to d\in B$$
59		simp2r	$$⊢\left(\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\right)\wedge \left(d\in B\wedge e\in B\right)\wedge j=\left(d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Y\right)\right)\to e\in B$$
60		simp13	$$⊢\left(\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\right)\wedge \left(d\in B\wedge e\in B\right)\wedge j=\left(d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Y\right)\right)\to j=\left(a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)$$
61		simp3	$$⊢\left(\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\right)\wedge \left(d\in B\wedge e\in B\right)\wedge j=\left(d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Y\right)\right)\to j=\left(d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Y\right)$$
62	1 2 3 4 5 50 51 52 53 54 55 12 13 14 15 16 17 18 19 56 57 58 59 60 61	baerlem5alem1	$$⊢\left(\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\right)\wedge \left(d\in B\wedge e\in B\right)\wedge j=\left(d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Y\right)\right)\to j=a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)$$
63	49 21	syl	$$⊢\left(\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\right)\wedge \left(d\in B\wedge e\in B\right)\wedge j=\left(d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Y\right)\right)\to W\in \mathrm{LMod}$$
64	1 12	lmodvacl	$$⊢\left(W\in \mathrm{LMod}\wedge Y\in V\wedge Z\in V\right)\to Y\underset{\dot{}}{+}Z\in V$$
65	21 24 25 64	syl3anc	$$⊢\phi \to Y\underset{\dot{}}{+}Z\in V$$
66	1 2	lmodvsubcl	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\wedge Y\underset{\dot{}}{+}Z\in V\right)\to X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\in V$$
67	21 7 65 66	syl3anc	$$⊢\phi \to X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\in V$$
68	49 67	syl	$$⊢\left(\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\right)\wedge \left(d\in B\wedge e\in B\right)\wedge j=\left(d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Y\right)\right)\to X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\in V$$
69	1 13 14 15 5 63 56 68	lspsneli	$$⊢\left(\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\right)\wedge \left(d\in B\wedge e\in B\right)\wedge j=\left(d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Y\right)\right)\to a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)\in N\left(\left\{X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right\}\right)$$
70	62 69	eqeltrd	$$⊢\left(\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\right)\wedge \left(d\in B\wedge e\in B\right)\wedge j=\left(d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Y\right)\right)\to j\in N\left(\left\{X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right\}\right)$$
71	70	3exp	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\right)\to \left(\left(d\in B\wedge e\in B\right)\to \left(j=\left(d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Y\right)\to j\in N\left(\left\{X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right\}\right)\right)\right)$$
72	71	rexlimdvv	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\right)\to \left(\exists d\in B\exists e\in Bj=\left(d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Y\right)\to j\in N\left(\left\{X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right\}\right)\right)$$
73	72	3exp	$$⊢\phi \to \left(\left(a\in B\wedge b\in B\right)\to \left(j=\left(a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\to \left(\exists d\in B\exists e\in Bj=\left(d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Y\right)\to j\in N\left(\left\{X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right\}\right)\right)\right)\right)$$
74	73	rexlimdvv	$$⊢\phi \to \left(\exists a\in B\exists b\in Bj=\left(a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\to \left(\exists d\in B\exists e\in Bj=\left(d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Y\right)\to j\in N\left(\left\{X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right\}\right)\right)\right)$$
75	74	impd	$$⊢\phi \to \left(\left(\exists a\in B\exists b\in Bj=\left(a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\wedge \exists d\in B\exists e\in Bj=\left(d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Y\right)\right)\to j\in N\left(\left\{X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right\}\right)\right)$$
76	48 75	sylbid	$$⊢\phi \to \left(j\in \left(\left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Z\right\}\right)\right)\cap \left(N\left(\left\{X\underset{\dot{}}{-}Z\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Y\right\}\right)\right)\right)\to j\in N\left(\left\{X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right\}\right)\right)$$
77	76	ssrdv	$$⊢\phi \to \left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Z\right\}\right)\right)\cap \left(N\left(\left\{X\underset{\dot{}}{-}Z\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Y\right\}\right)\right)\subseteq N\left(\left\{X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right\}\right)$$
78	43 77	eqssd	$$⊢\phi \to N\left(\left\{X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right\}\right)=\left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Z\right\}\right)\right)\cap \left(N\left(\left\{X\underset{\dot{}}{-}Z\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Y\right\}\right)\right)$$