Theorem baerlem5alem1

Description: Lemma for baerlem5a . (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)$$
	baerlem5a.a1	$$⊢\phi \to a\in B$$
	baerlem5a.b1	$$⊢\phi \to b\in B$$
	baerlem5a.d1	$$⊢\phi \to d\in B$$
	baerlem5a.e1	$$⊢\phi \to e\in B$$
	baerlem5a.j1	$$⊢\phi \to j=\left(a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)$$
	baerlem5a.j2	$$⊢\phi \to j=\left(d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Y\right)$$
Assertion	baerlem5alem1	$$⊢\phi \to j=a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\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		baerlem5a.a1	$$⊢\phi \to a\in B$$
21		baerlem5a.b1	$$⊢\phi \to b\in B$$
22		baerlem5a.d1	$$⊢\phi \to d\in B$$
23		baerlem5a.e1	$$⊢\phi \to e\in B$$
24		baerlem5a.j1	$$⊢\phi \to j=\left(a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)$$
25		baerlem5a.j2	$$⊢\phi \to j=\left(d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Y\right)$$
26		lveclmod	$$⊢W\in \mathrm{LVec}\to W\in \mathrm{LMod}$$
27	6 26	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
28	10	eldifad	$$⊢\phi \to Y\in V$$
29	1 13 14 15 2 27 20 7 28	lmodsubdi	$$⊢\phi \to a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Y\right)=\left(a\underset{\dot{}}{·}X\right)\underset{\dot{}}{-}\left(a\underset{\dot{}}{·}Y\right)$$
30	1 14 13 15	lmodvscl	$$⊢\left(W\in \mathrm{LMod}\wedge a\in B\wedge X\in V\right)\to a\underset{\dot{}}{·}X\in V$$
31	27 20 7 30	syl3anc	$$⊢\phi \to a\underset{\dot{}}{·}X\in V$$
32	1 12 2 13 14 15 19 27 20 31 28	lmodsubvs	$$⊢\phi \to \left(a\underset{\dot{}}{·}X\right)\underset{\dot{}}{-}\left(a\underset{\dot{}}{·}Y\right)=\left(a\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(I\left(a\right)\underset{\dot{}}{·}Y\right)$$
33	29 32	eqtrd	$$⊢\phi \to a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Y\right)=\left(a\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(I\left(a\right)\underset{\dot{}}{·}Y\right)$$
34	33	oveq1d	$$⊢\phi \to \left(a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)=\left(\left(a\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(I\left(a\right)\underset{\dot{}}{·}Y\right)\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)$$
35	14	lmodring	$$⊢W\in \mathrm{LMod}\to R\in \mathrm{Ring}$$
36		ringgrp	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Grp}$$
37	27 35 36	3syl	$$⊢\phi \to R\in \mathrm{Grp}$$
38	15 19	grpinvcl	$$⊢\left(R\in \mathrm{Grp}\wedge a\in B\right)\to I\left(a\right)\in B$$
39	37 20 38	syl2anc	$$⊢\phi \to I\left(a\right)\in B$$
40	1 14 13 15	lmodvscl	$$⊢\left(W\in \mathrm{LMod}\wedge I\left(a\right)\in B\wedge Y\in V\right)\to I\left(a\right)\underset{\dot{}}{·}Y\in V$$
41	27 39 28 40	syl3anc	$$⊢\phi \to I\left(a\right)\underset{\dot{}}{·}Y\in V$$
42	11	eldifad	$$⊢\phi \to Z\in V$$
43	1 14 13 15	lmodvscl	$$⊢\left(W\in \mathrm{LMod}\wedge b\in B\wedge Z\in V\right)\to b\underset{\dot{}}{·}Z\in V$$
44	27 21 42 43	syl3anc	$$⊢\phi \to b\underset{\dot{}}{·}Z\in V$$
45	1 12	lmodass	$$⊢\left(W\in \mathrm{LMod}\wedge \left(a\underset{\dot{}}{·}X\in V\wedge I\left(a\right)\underset{\dot{}}{·}Y\in V\wedge b\underset{\dot{}}{·}Z\in V\right)\right)\to \left(\left(a\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(I\left(a\right)\underset{\dot{}}{·}Y\right)\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)=\left(a\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(\left(I\left(a\right)\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\right)$$
46	27 31 41 44 45	syl13anc	$$⊢\phi \to \left(\left(a\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(I\left(a\right)\underset{\dot{}}{·}Y\right)\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)=\left(a\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(\left(I\left(a\right)\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\right)$$
47	24 34 46	3eqtrd	$$⊢\phi \to j=\left(a\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(\left(I\left(a\right)\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\right)$$
48	1 12	lmodvacl	$$⊢\left(W\in \mathrm{LMod}\wedge Y\in V\wedge Z\in V\right)\to Y\underset{\dot{}}{+}Z\in V$$
49	27 28 42 48	syl3anc	$$⊢\phi \to Y\underset{\dot{}}{+}Z\in V$$
50	1 14 13 15	lmodvscl	$$⊢\left(W\in \mathrm{LMod}\wedge a\in B\wedge Y\underset{\dot{}}{+}Z\in V\right)\to a\underset{\dot{}}{·}\left(Y\underset{\dot{}}{+}Z\right)\in V$$
51	27 20 49 50	syl3anc	$$⊢\phi \to a\underset{\dot{}}{·}\left(Y\underset{\dot{}}{+}Z\right)\in V$$
52		eqid	$$⊢{inv}_g\left(W\right)={inv}_g\left(W\right)$$
53	1 12 52 2	grpsubval	$$⊢\left(a\underset{\dot{}}{·}X\in V\wedge a\underset{\dot{}}{·}\left(Y\underset{\dot{}}{+}Z\right)\in V\right)\to \left(a\underset{\dot{}}{·}X\right)\underset{\dot{}}{-}\left(a\underset{\dot{}}{·}\left(Y\underset{\dot{}}{+}Z\right)\right)=\left(a\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}{inv}_g\left(W\right)\left(a\underset{\dot{}}{·}\left(Y\underset{\dot{}}{+}Z\right)\right)$$
54	31 51 53	syl2anc	$$⊢\phi \to \left(a\underset{\dot{}}{·}X\right)\underset{\dot{}}{-}\left(a\underset{\dot{}}{·}\left(Y\underset{\dot{}}{+}Z\right)\right)=\left(a\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}{inv}_g\left(W\right)\left(a\underset{\dot{}}{·}\left(Y\underset{\dot{}}{+}Z\right)\right)$$
55	1 13 14 15 2 27 20 7 49	lmodsubdi	$$⊢\phi \to a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)=\left(a\underset{\dot{}}{·}X\right)\underset{\dot{}}{-}\left(a\underset{\dot{}}{·}\left(Y\underset{\dot{}}{+}Z\right)\right)$$
56	1 12 14 13 15	lmodvsdi	$$⊢\left(W\in \mathrm{LMod}\wedge \left(I\left(a\right)\in B\wedge Y\in V\wedge Z\in V\right)\right)\to I\left(a\right)\underset{\dot{}}{·}\left(Y\underset{\dot{}}{+}Z\right)=\left(I\left(a\right)\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(I\left(a\right)\underset{\dot{}}{·}Z\right)$$
57	27 39 28 42 56	syl13anc	$$⊢\phi \to I\left(a\right)\underset{\dot{}}{·}\left(Y\underset{\dot{}}{+}Z\right)=\left(I\left(a\right)\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(I\left(a\right)\underset{\dot{}}{·}Z\right)$$
58	1 14 13 52 15 19 27 49 20	lmodvsneg	$$⊢\phi \to {inv}_g\left(W\right)\left(a\underset{\dot{}}{·}\left(Y\underset{\dot{}}{+}Z\right)\right)=I\left(a\right)\underset{\dot{}}{·}\left(Y\underset{\dot{}}{+}Z\right)$$
59	15 19	grpinvcl	$$⊢\left(R\in \mathrm{Grp}\wedge d\in B\right)\to I\left(d\right)\in B$$
60	37 22 59	syl2anc	$$⊢\phi \to I\left(d\right)\in B$$
61		eqid	$$⊢\mathrm{LSubSp}\left(W\right)=\mathrm{LSubSp}\left(W\right)$$
62	1 61 5 27 28 42	lspprcl	$$⊢\phi \to N\left(\left\{Y,Z\right\}\right)\in \mathrm{LSubSp}\left(W\right)$$
63	1 12 13 14 15 5 27 39 21 28 42	lsppreli	$$⊢\phi \to \left(I\left(a\right)\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\in N\left(\left\{Y,Z\right\}\right)$$
64	1 12 13 14 15 5 27 23 60 28 42	lsppreli	$$⊢\phi \to \left(e\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(I\left(d\right)\underset{\dot{}}{·}Z\right)\in N\left(\left\{Y,Z\right\}\right)$$
65	1 13 14 15 2 27 22 7 42	lmodsubdi	$$⊢\phi \to d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)=\left(d\underset{\dot{}}{·}X\right)\underset{\dot{}}{-}\left(d\underset{\dot{}}{·}Z\right)$$
66	1 14 13 15	lmodvscl	$$⊢\left(W\in \mathrm{LMod}\wedge d\in B\wedge X\in V\right)\to d\underset{\dot{}}{·}X\in V$$
67	27 22 7 66	syl3anc	$$⊢\phi \to d\underset{\dot{}}{·}X\in V$$
68	1 12 2 13 14 15 19 27 22 67 42	lmodsubvs	$$⊢\phi \to \left(d\underset{\dot{}}{·}X\right)\underset{\dot{}}{-}\left(d\underset{\dot{}}{·}Z\right)=\left(d\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(I\left(d\right)\underset{\dot{}}{·}Z\right)$$
69	65 68	eqtrd	$$⊢\phi \to d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)=\left(d\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(I\left(d\right)\underset{\dot{}}{·}Z\right)$$
70	69	oveq1d	$$⊢\phi \to \left(d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Y\right)=\left(\left(d\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(I\left(d\right)\underset{\dot{}}{·}Z\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Y\right)$$
71		lmodabl	$$⊢W\in \mathrm{LMod}\to W\in \mathrm{Abel}$$
72	6 26 71	3syl	$$⊢\phi \to W\in \mathrm{Abel}$$
73	1 14 13 15	lmodvscl	$$⊢\left(W\in \mathrm{LMod}\wedge I\left(d\right)\in B\wedge Z\in V\right)\to I\left(d\right)\underset{\dot{}}{·}Z\in V$$
74	27 60 42 73	syl3anc	$$⊢\phi \to I\left(d\right)\underset{\dot{}}{·}Z\in V$$
75	1 14 13 15	lmodvscl	$$⊢\left(W\in \mathrm{LMod}\wedge e\in B\wedge Y\in V\right)\to e\underset{\dot{}}{·}Y\in V$$
76	27 23 28 75	syl3anc	$$⊢\phi \to e\underset{\dot{}}{·}Y\in V$$
77	1 12 72 67 74 76	abl32	$$⊢\phi \to \left(\left(d\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(I\left(d\right)\underset{\dot{}}{·}Z\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Y\right)=\left(\left(d\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Y\right)\right)\underset{\dot{}}{+}\left(I\left(d\right)\underset{\dot{}}{·}Z\right)$$
78	1 12	lmodass	$$⊢\left(W\in \mathrm{LMod}\wedge \left(d\underset{\dot{}}{·}X\in V\wedge e\underset{\dot{}}{·}Y\in V\wedge I\left(d\right)\underset{\dot{}}{·}Z\in V\right)\right)\to \left(\left(d\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Y\right)\right)\underset{\dot{}}{+}\left(I\left(d\right)\underset{\dot{}}{·}Z\right)=\left(d\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(\left(e\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(I\left(d\right)\underset{\dot{}}{·}Z\right)\right)$$
79	27 67 76 74 78	syl13anc	$$⊢\phi \to \left(\left(d\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Y\right)\right)\underset{\dot{}}{+}\left(I\left(d\right)\underset{\dot{}}{·}Z\right)=\left(d\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(\left(e\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(I\left(d\right)\underset{\dot{}}{·}Z\right)\right)$$
80	70 77 79	3eqtrd	$$⊢\phi \to \left(d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Y\right)=\left(d\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(\left(e\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(I\left(d\right)\underset{\dot{}}{·}Z\right)\right)$$
81	25 47 80	3eqtr3d	$$⊢\phi \to \left(a\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(\left(I\left(a\right)\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\right)=\left(d\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(\left(e\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(I\left(d\right)\underset{\dot{}}{·}Z\right)\right)$$
82	1 12 14 15 13 61 6 62 7 8 63 64 20 22 81	lvecindp	$$⊢\phi \to \left(a=d\wedge \left(I\left(a\right)\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)=\left(e\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(I\left(d\right)\underset{\dot{}}{·}Z\right)\right)$$
83	82	simprd	$$⊢\phi \to \left(I\left(a\right)\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)=\left(e\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(I\left(d\right)\underset{\dot{}}{·}Z\right)$$
84	1 12 14 15 13 3 5 6 10 11 39 21 23 60 9 83	lvecindp2	$$⊢\phi \to \left(I\left(a\right)=e\wedge b=I\left(d\right)\right)$$
85	84	simprd	$$⊢\phi \to b=I\left(d\right)$$
86	82	simpld	$$⊢\phi \to a=d$$
87	86	fveq2d	$$⊢\phi \to I\left(a\right)=I\left(d\right)$$
88	85 87	eqtr4d	$$⊢\phi \to b=I\left(a\right)$$
89	88	oveq1d	$$⊢\phi \to b\underset{\dot{}}{·}Z=I\left(a\right)\underset{\dot{}}{·}Z$$
90	89	oveq2d	$$⊢\phi \to \left(I\left(a\right)\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)=\left(I\left(a\right)\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(I\left(a\right)\underset{\dot{}}{·}Z\right)$$
91	57 58 90	3eqtr4rd	$$⊢\phi \to \left(I\left(a\right)\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)={inv}_g\left(W\right)\left(a\underset{\dot{}}{·}\left(Y\underset{\dot{}}{+}Z\right)\right)$$
92	91	oveq2d	$$⊢\phi \to \left(a\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(\left(I\left(a\right)\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\right)=\left(a\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}{inv}_g\left(W\right)\left(a\underset{\dot{}}{·}\left(Y\underset{\dot{}}{+}Z\right)\right)$$
93	54 55 92	3eqtr4rd	$$⊢\phi \to \left(a\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(\left(I\left(a\right)\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\right)=a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)$$
94	47 93	eqtrd	$$⊢\phi \to j=a\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right)$$