Theorem baerlem5blem2

Description: Lemma for baerlem5b . (Contributed by NM, 13-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	baerlem5blem2	$$⊢\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{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{X\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 12 5 4	lspsntri	$$⊢\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 12	lmodvacl	$$⊢\left(W\in \mathrm{LMod}\wedge Y\in V\wedge Z\in V\right)\to Y\underset{\dot{}}{+}Z\in V$$
27	21 22 23 26	syl3anc	$$⊢\phi \to Y\underset{\dot{}}{+}Z\in V$$
28	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$$
29	21 7 27 28	syl3anc	$$⊢\phi \to X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\in V$$
30	1 2 5 21 29 7	lspsnsub	$$⊢\phi \to N\left(\left\{\left(X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)\underset{\dot{}}{-}X\right\}\right)=N\left(\left\{X\underset{\dot{}}{-}\left(X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)\right\}\right)$$
31		lmodabl	$$⊢W\in \mathrm{LMod}\to W\in \mathrm{Abel}$$
32	21 31	syl	$$⊢\phi \to W\in \mathrm{Abel}$$
33	1 2 32 7 27	ablnncan	$$⊢\phi \to X\underset{\dot{}}{-}\left(X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)=Y\underset{\dot{}}{+}Z$$
34	33	sneqd	$$⊢\phi \to \left\{X\underset{\dot{}}{-}\left(X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)\right\}=\left\{Y\underset{\dot{}}{+}Z\right\}$$
35	34	fveq2d	$$⊢\phi \to N\left(\left\{X\underset{\dot{}}{-}\left(X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)\right\}\right)=N\left(\left\{Y\underset{\dot{}}{+}Z\right\}\right)$$
36	30 35	eqtrd	$$⊢\phi \to N\left(\left\{\left(X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)\underset{\dot{}}{-}X\right\}\right)=N\left(\left\{Y\underset{\dot{}}{+}Z\right\}\right)$$
37	1 2 4 5	lspsntrim	$$⊢\left(W\in \mathrm{LMod}\wedge X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\in V\wedge X\in V\right)\to N\left(\left\{\left(X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)\underset{\dot{}}{-}X\right\}\right)\subseteq N\left(\left\{X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{X\right\}\right)$$
38	21 29 7 37	syl3anc	$$⊢\phi \to N\left(\left\{\left(X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)\underset{\dot{}}{-}X\right\}\right)\subseteq N\left(\left\{X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{X\right\}\right)$$
39	36 38	eqsstrrd	$$⊢\phi \to N\left(\left\{Y\underset{\dot{}}{+}Z\right\}\right)\subseteq N\left(\left\{X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{X\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{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{X\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{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{X\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{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{X\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 29 7	lsmspsn	$$⊢\phi \to \left(j\in \left(N\left(\left\{X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{X\right\}\right)\right)\leftrightarrow \exists d\in B\exists e\in Bj=\left(d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}X\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{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{X\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{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}X\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{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{X\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{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}X\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{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}X\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{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}X\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{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}X\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{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}X\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{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}X\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{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}X\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{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}X\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{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}X\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{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}X\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{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}X\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{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}X\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{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}X\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{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}X\right)\right)\to j=\left(d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}X\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	baerlem5blem1	$$⊢\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{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}X\right)\right)\to j=I\left(d\right)\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{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}X\right)\right)\to W\in \mathrm{LMod}$$
61	14	lmodring	$$⊢W\in \mathrm{LMod}\to R\in \mathrm{Ring}$$
62		ringgrp	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Grp}$$
63	46 21 61 62	4syl	$$⊢\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{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}X\right)\right)\to R\in \mathrm{Grp}$$
64	15 19	grpinvcl	$$⊢\left(R\in \mathrm{Grp}\wedge d\in B\right)\to I\left(d\right)\in B$$
65	63 55 64	syl2anc	$$⊢\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{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}X\right)\right)\to I\left(d\right)\in B$$
66	46 27	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{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}X\right)\right)\to Y\underset{\dot{}}{+}Z\in V$$
67	1 13 14 15 5 60 65 66	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{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}X\right)\right)\to I\left(d\right)\underset{\dot{}}{·}\left(Y\underset{\dot{}}{+}Z\right)\in N\left(\left\{Y\underset{\dot{}}{+}Z\right\}\right)$$
68	59 67	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{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}X\right)\right)\to j\in N\left(\left\{Y\underset{\dot{}}{+}Z\right\}\right)$$
69	68	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{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}X\right)\to j\in N\left(\left\{Y\underset{\dot{}}{+}Z\right\}\right)\right)\right)$$
70	69	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{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}X\right)\to j\in N\left(\left\{Y\underset{\dot{}}{+}Z\right\}\right)\right)$$
71	70	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{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}X\right)\to j\in N\left(\left\{Y\underset{\dot{}}{+}Z\right\}\right)\right)\right)\right)$$
72	71	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{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}X\right)\to j\in N\left(\left\{Y\underset{\dot{}}{+}Z\right\}\right)\right)\right)$$
73	72	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{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}X\right)\right)\to j\in N\left(\left\{Y\underset{\dot{}}{+}Z\right\}\right)\right)$$
74	45 73	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{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{X\right\}\right)\right)\right)\to j\in N\left(\left\{Y\underset{\dot{}}{+}Z\right\}\right)\right)$$
75	74	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{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{X\right\}\right)\right)\subseteq N\left(\left\{Y\underset{\dot{}}{+}Z\right\}\right)$$
76	40 75	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{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{X\right\}\right)\right)$$