Theorem baerlem3lem2

Description: Lemma for baerlem3 . (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	baerlem3lem2	$$⊢\phi \to N\left(\left\{Y\underset{\dot{}}{-}Z\right\}\right)=\left(N\left(\left\{Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Z\right\}\right)\right)\cap \left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{X\underset{\dot{}}{-}Z\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	10	eldifad	$$⊢\phi \to Y\in V$$
23	11	eldifad	$$⊢\phi \to Z\in V$$
24	1 2 4 5	lspsntrim	$$⊢\left(W\in \mathrm{LMod}\wedge Y\in V\wedge Z\in V\right)\to N\left(\left\{Y\underset{\dot{}}{-}Z\right\}\right)\subseteq N\left(\left\{Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Z\right\}\right)$$
25	21 22 23 24	syl3anc	$$⊢\phi \to N\left(\left\{Y\underset{\dot{}}{-}Z\right\}\right)\subseteq N\left(\left\{Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Z\right\}\right)$$
26	1 2 5 21 22 23	lspsnsub	$$⊢\phi \to N\left(\left\{Y\underset{\dot{}}{-}Z\right\}\right)=N\left(\left\{Z\underset{\dot{}}{-}Y\right\}\right)$$
27		lmodabl	$$⊢W\in \mathrm{LMod}\to W\in \mathrm{Abel}$$
28	21 27	syl	$$⊢\phi \to W\in \mathrm{Abel}$$
29	1 2 28 7 22 23	ablnnncan1	$$⊢\phi \to \left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{-}\left(X\underset{\dot{}}{-}Z\right)=Z\underset{\dot{}}{-}Y$$
30	29	sneqd	$$⊢\phi \to \left\{\left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{-}\left(X\underset{\dot{}}{-}Z\right)\right\}=\left\{Z\underset{\dot{}}{-}Y\right\}$$
31	30	fveq2d	$$⊢\phi \to N\left(\left\{\left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{-}\left(X\underset{\dot{}}{-}Z\right)\right\}\right)=N\left(\left\{Z\underset{\dot{}}{-}Y\right\}\right)$$
32	26 31	eqtr4d	$$⊢\phi \to N\left(\left\{Y\underset{\dot{}}{-}Z\right\}\right)=N\left(\left\{\left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{-}\left(X\underset{\dot{}}{-}Z\right)\right\}\right)$$
33	1 2	lmodvsubcl	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\wedge Y\in V\right)\to X\underset{\dot{}}{-}Y\in V$$
34	21 7 22 33	syl3anc	$$⊢\phi \to X\underset{\dot{}}{-}Y\in V$$
35	1 2	lmodvsubcl	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\wedge Z\in V\right)\to X\underset{\dot{}}{-}Z\in V$$
36	21 7 23 35	syl3anc	$$⊢\phi \to X\underset{\dot{}}{-}Z\in V$$
37	1 2 4 5	lspsntrim	$$⊢\left(W\in \mathrm{LMod}\wedge X\underset{\dot{}}{-}Y\in V\wedge X\underset{\dot{}}{-}Z\in V\right)\to N\left(\left\{\left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{-}\left(X\underset{\dot{}}{-}Z\right)\right\}\right)\subseteq N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{X\underset{\dot{}}{-}Z\right\}\right)$$
38	21 34 36 37	syl3anc	$$⊢\phi \to N\left(\left\{\left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{-}\left(X\underset{\dot{}}{-}Z\right)\right\}\right)\subseteq N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{X\underset{\dot{}}{-}Z\right\}\right)$$
39	32 38	eqsstrd	$$⊢\phi \to N\left(\left\{Y\underset{\dot{}}{-}Z\right\}\right)\subseteq N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{X\underset{\dot{}}{-}Z\right\}\right)$$
40	25 39	ssind	$$⊢\phi \to N\left(\left\{Y\underset{\dot{}}{-}Z\right\}\right)\subseteq \left(N\left(\left\{Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Z\right\}\right)\right)\cap \left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{X\underset{\dot{}}{-}Z\right\}\right)\right)$$
41		elin	$$⊢j\in \left(\left(N\left(\left\{Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Z\right\}\right)\right)\cap \left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{X\underset{\dot{}}{-}Z\right\}\right)\right)\right)\leftrightarrow \left(j\in \left(N\left(\left\{Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Z\right\}\right)\right)\wedge j\in \left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{X\underset{\dot{}}{-}Z\right\}\right)\right)\right)$$
42	1 12 14 15 13 4 5 21 22 23	lsmspsn	$$⊢\phi \to \left(j\in \left(N\left(\left\{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{}}{·}Y\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\right)$$
43	1 12 14 15 13 4 5 21 34 36	lsmspsn	$$⊢\phi \to \left(j\in \left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{X\underset{\dot{}}{-}Z\right\}\right)\right)\leftrightarrow \exists d\in B\exists e\in Bj=\left(d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\right)$$
44	42 43	anbi12d	$$⊢\phi \to \left(\left(j\in \left(N\left(\left\{Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Z\right\}\right)\right)\wedge j\in \left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{X\underset{\dot{}}{-}Z\right\}\right)\right)\right)\leftrightarrow \left(\exists a\in B\exists b\in Bj=\left(a\underset{\dot{}}{·}Y\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{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\right)\right)$$
45	41 44	syl5bb	$$⊢\phi \to \left(j\in \left(\left(N\left(\left\{Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Z\right\}\right)\right)\cap \left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{X\underset{\dot{}}{-}Z\right\}\right)\right)\right)\leftrightarrow \left(\exists a\in B\exists b\in Bj=\left(a\underset{\dot{}}{·}Y\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{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\right)\right)$$
46		simp11	$$⊢\left(\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}Y\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{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\right)\to \phi$$
47	46 6	syl	$$⊢\left(\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}Y\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{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\right)\to W\in \mathrm{LVec}$$
48	46 7	syl	$$⊢\left(\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}Y\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{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\right)\to X\in V$$
49	46 8	syl	$$⊢\left(\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}Y\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{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\right)\to \neg X\in N\left(\left\{Y,Z\right\}\right)$$
50	46 9	syl	$$⊢\left(\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}Y\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{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\right)\to N\left(\left\{Y\right\}\right)\ne N\left(\left\{Z\right\}\right)$$
51	46 10	syl	$$⊢\left(\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}Y\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{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\right)\to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
52	46 11	syl	$$⊢\left(\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}Y\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{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\right)\to Z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
53		simp12l	$$⊢\left(\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}Y\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{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\right)\to a\in B$$
54		simp12r	$$⊢\left(\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}Y\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{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\right)\to b\in B$$
55		simp2l	$$⊢\left(\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}Y\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{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\right)\to d\in B$$
56		simp2r	$$⊢\left(\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}Y\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{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\right)\to e\in B$$
57		simp13	$$⊢\left(\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}Y\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{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\right)\to j=\left(a\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)$$
58		simp3	$$⊢\left(\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}Y\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{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\right)\to j=\left(d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)$$
59	1 2 3 4 5 47 48 49 50 51 52 12 13 14 15 16 17 18 19 53 54 55 56 57 58	baerlem3lem1	$$⊢\left(\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}Y\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{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\right)\to j=a\underset{\dot{}}{·}\left(Y\underset{\dot{}}{-}Z\right)$$
60	46 21	syl	$$⊢\left(\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}Y\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{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\right)\to W\in \mathrm{LMod}$$
61	1 2	lmodvsubcl	$$⊢\left(W\in \mathrm{LMod}\wedge Y\in V\wedge Z\in V\right)\to Y\underset{\dot{}}{-}Z\in V$$
62	21 22 23 61	syl3anc	$$⊢\phi \to Y\underset{\dot{}}{-}Z\in V$$
63	46 62	syl	$$⊢\left(\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}Y\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{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\right)\to Y\underset{\dot{}}{-}Z\in V$$
64	1 13 14 15 5 60 53 63	lspsneli	$$⊢\left(\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}Y\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{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\right)\to a\underset{\dot{}}{·}\left(Y\underset{\dot{}}{-}Z\right)\in N\left(\left\{Y\underset{\dot{}}{-}Z\right\}\right)$$
65	59 64	eqeltrd	$$⊢\left(\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}Y\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{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\right)\to j\in N\left(\left\{Y\underset{\dot{}}{-}Z\right\}\right)$$
66	65	3exp	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}Y\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{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\to j\in N\left(\left\{Y\underset{\dot{}}{-}Z\right\}\right)\right)\right)$$
67	66	rexlimdvv	$$⊢\left(\phi \wedge \left(a\in B\wedge b\in B\right)\wedge j=\left(a\underset{\dot{}}{·}Y\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{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\to j\in N\left(\left\{Y\underset{\dot{}}{-}Z\right\}\right)\right)$$
68	67	3exp	$$⊢\phi \to \left(\left(a\in B\wedge b\in B\right)\to \left(j=\left(a\underset{\dot{}}{·}Y\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{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\to j\in N\left(\left\{Y\underset{\dot{}}{-}Z\right\}\right)\right)\right)\right)$$
69	68	rexlimdvv	$$⊢\phi \to \left(\exists a\in B\exists b\in Bj=\left(a\underset{\dot{}}{·}Y\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{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\to j\in N\left(\left\{Y\underset{\dot{}}{-}Z\right\}\right)\right)\right)$$
70	69	impd	$$⊢\phi \to \left(\left(\exists a\in B\exists b\in Bj=\left(a\underset{\dot{}}{·}Y\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{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\right)\to j\in N\left(\left\{Y\underset{\dot{}}{-}Z\right\}\right)\right)$$
71	45 70	sylbid	$$⊢\phi \to \left(j\in \left(\left(N\left(\left\{Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Z\right\}\right)\right)\cap \left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{X\underset{\dot{}}{-}Z\right\}\right)\right)\right)\to j\in N\left(\left\{Y\underset{\dot{}}{-}Z\right\}\right)\right)$$
72	71	ssrdv	$$⊢\phi \to \left(N\left(\left\{Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Z\right\}\right)\right)\cap \left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{X\underset{\dot{}}{-}Z\right\}\right)\right)\subseteq N\left(\left\{Y\underset{\dot{}}{-}Z\right\}\right)$$
73	40 72	eqssd	$$⊢\phi \to N\left(\left\{Y\underset{\dot{}}{-}Z\right\}\right)=\left(N\left(\left\{Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Z\right\}\right)\right)\cap \left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{X\underset{\dot{}}{-}Z\right\}\right)\right)$$