Theorem baerlem3lem1

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)$$
	baerlem3.a1	$$⊢\phi \to a\in B$$
	baerlem3.b1	$$⊢\phi \to b\in B$$
	baerlem3.d1	$$⊢\phi \to d\in B$$
	baerlem3.e1	$$⊢\phi \to e\in B$$
	baerlem3.j1	$$⊢\phi \to j=\left(a\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)$$
	baerlem3.j2	$$⊢\phi \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)$$
Assertion	baerlem3lem1	$$⊢\phi \to j=a\underset{\dot{}}{·}\left(Y\underset{\dot{}}{-}Z\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		baerlem3.a1	$$⊢\phi \to a\in B$$
21		baerlem3.b1	$$⊢\phi \to b\in B$$
22		baerlem3.d1	$$⊢\phi \to d\in B$$
23		baerlem3.e1	$$⊢\phi \to e\in B$$
24		baerlem3.j1	$$⊢\phi \to j=\left(a\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)$$
25		baerlem3.j2	$$⊢\phi \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)$$
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 14 13 15	lmodvscl	$$⊢\left(W\in \mathrm{LMod}\wedge a\in B\wedge Y\in V\right)\to a\underset{\dot{}}{·}Y\in V$$
30	27 20 28 29	syl3anc	$$⊢\phi \to a\underset{\dot{}}{·}Y\in V$$
31	11	eldifad	$$⊢\phi \to Z\in V$$
32	1 14 13 15	lmodvscl	$$⊢\left(W\in \mathrm{LMod}\wedge a\in B\wedge Z\in V\right)\to a\underset{\dot{}}{·}Z\in V$$
33	27 20 31 32	syl3anc	$$⊢\phi \to a\underset{\dot{}}{·}Z\in V$$
34		eqid	$$⊢1_R=1_R$$
35	1 12 2 14 13 19 34	lmodvsubval2	$$⊢\left(W\in \mathrm{LMod}\wedge a\underset{\dot{}}{·}Y\in V\wedge a\underset{\dot{}}{·}Z\in V\right)\to \left(a\underset{\dot{}}{·}Y\right)\underset{\dot{}}{-}\left(a\underset{\dot{}}{·}Z\right)=\left(a\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(I\left(1_R\right)\underset{\dot{}}{·}\left(a\underset{\dot{}}{·}Z\right)\right)$$
36	27 30 33 35	syl3anc	$$⊢\phi \to \left(a\underset{\dot{}}{·}Y\right)\underset{\dot{}}{-}\left(a\underset{\dot{}}{·}Z\right)=\left(a\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(I\left(1_R\right)\underset{\dot{}}{·}\left(a\underset{\dot{}}{·}Z\right)\right)$$
37	1 13 14 15 2 27 20 28 31	lmodsubdi	$$⊢\phi \to a\underset{\dot{}}{·}\left(Y\underset{\dot{}}{-}Z\right)=\left(a\underset{\dot{}}{·}Y\right)\underset{\dot{}}{-}\left(a\underset{\dot{}}{·}Z\right)$$
38	14	lmodring	$$⊢W\in \mathrm{LMod}\to R\in \mathrm{Ring}$$
39	27 38	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
40		ringgrp	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Grp}$$
41	39 40	syl	$$⊢\phi \to R\in \mathrm{Grp}$$
42	14 15 34	lmod1cl	$$⊢W\in \mathrm{LMod}\to 1_R\in B$$
43	27 42	syl	$$⊢\phi \to 1_R\in B$$
44	15 19	grpinvcl	$$⊢\left(R\in \mathrm{Grp}\wedge 1_R\in B\right)\to I\left(1_R\right)\in B$$
45	41 43 44	syl2anc	$$⊢\phi \to I\left(1_R\right)\in B$$
46		eqid	$$⊢{\cdot }_R={\cdot }_R$$
47	1 14 13 15 46	lmodvsass	$$⊢\left(W\in \mathrm{LMod}\wedge \left(I\left(1_R\right)\in B\wedge a\in B\wedge Z\in V\right)\right)\to \left(I\left(1_R\right){\cdot }_{R}a\right)\underset{\dot{}}{·}Z=I\left(1_R\right)\underset{\dot{}}{·}\left(a\underset{\dot{}}{·}Z\right)$$
48	27 45 20 31 47	syl13anc	$$⊢\phi \to \left(I\left(1_R\right){\cdot }_{R}a\right)\underset{\dot{}}{·}Z=I\left(1_R\right)\underset{\dot{}}{·}\left(a\underset{\dot{}}{·}Z\right)$$
49	15 46 34 19 39 20	ringnegl	$$⊢\phi \to I\left(1_R\right){\cdot }_{R}a=I\left(a\right)$$
50		ringabl	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Abel}$$
51	39 50	syl	$$⊢\phi \to R\in \mathrm{Abel}$$
52	15 16 19	ablinvadd	$$⊢\left(R\in \mathrm{Abel}\wedge d\in B\wedge e\in B\right)\to I\left(d\underset{\dot{}}{⨣}e\right)=I\left(d\right)\underset{\dot{}}{⨣}I\left(e\right)$$
53	51 22 23 52	syl3anc	$$⊢\phi \to I\left(d\underset{\dot{}}{⨣}e\right)=I\left(d\right)\underset{\dot{}}{⨣}I\left(e\right)$$
54		eqid	$$⊢\mathrm{LSubSp}\left(W\right)=\mathrm{LSubSp}\left(W\right)$$
55	1 54 5 27 28 31	lspprcl	$$⊢\phi \to N\left(\left\{Y,Z\right\}\right)\in \mathrm{LSubSp}\left(W\right)$$
56	1 12 13 14 15 5 27 20 21 28 31	lsppreli	$$⊢\phi \to \left(a\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\in N\left(\left\{Y,Z\right\}\right)$$
57	1 12 13 14 15 5 27 22 23 28 31	lsppreli	$$⊢\phi \to \left(d\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Z\right)\in N\left(\left\{Y,Z\right\}\right)$$
58		eqid	$$⊢{inv}_g\left(W\right)={inv}_g\left(W\right)$$
59	54 58	lssvnegcl	$$⊢\left(W\in \mathrm{LMod}\wedge N\left(\left\{Y,Z\right\}\right)\in \mathrm{LSubSp}\left(W\right)\wedge \left(d\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Z\right)\in N\left(\left\{Y,Z\right\}\right)\right)\to {inv}_g\left(W\right)\left(\left(d\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Z\right)\right)\in N\left(\left\{Y,Z\right\}\right)$$
60	27 55 57 59	syl3anc	$$⊢\phi \to {inv}_g\left(W\right)\left(\left(d\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Z\right)\right)\in N\left(\left\{Y,Z\right\}\right)$$
61	15 18	ring0cl	$$⊢R\in \mathrm{Ring}\to Q\in B$$
62	39 61	syl	$$⊢\phi \to Q\in B$$
63	15 16	ringacl	$$⊢\left(R\in \mathrm{Ring}\wedge d\in B\wedge e\in B\right)\to d\underset{\dot{}}{⨣}e\in B$$
64	39 22 23 63	syl3anc	$$⊢\phi \to d\underset{\dot{}}{⨣}e\in B$$
65	1 14 13 18 3	lmod0vs	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\right)\to Q\underset{\dot{}}{·}X=\underset{\dot{}}{0}$$
66	27 7 65	syl2anc	$$⊢\phi \to Q\underset{\dot{}}{·}X=\underset{\dot{}}{0}$$
67	66	oveq1d	$$⊢\phi \to \left(Q\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(\left(a\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\right)=\underset{\dot{}}{0}\underset{\dot{}}{+}\left(\left(a\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\right)$$
68		lmodgrp	$$⊢W\in \mathrm{LMod}\to W\in \mathrm{Grp}$$
69	27 68	syl	$$⊢\phi \to W\in \mathrm{Grp}$$
70	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$$
71	27 21 31 70	syl3anc	$$⊢\phi \to b\underset{\dot{}}{·}Z\in V$$
72	1 12	lmodvacl	$$⊢\left(W\in \mathrm{LMod}\wedge a\underset{\dot{}}{·}Y\in V\wedge b\underset{\dot{}}{·}Z\in V\right)\to \left(a\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\in V$$
73	27 30 71 72	syl3anc	$$⊢\phi \to \left(a\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\in V$$
74	1 12 3	grplid	$$⊢\left(W\in \mathrm{Grp}\wedge \left(a\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\in V\right)\to \underset{\dot{}}{0}\underset{\dot{}}{+}\left(\left(a\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\right)=\left(a\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)$$
75	69 73 74	syl2anc	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{+}\left(\left(a\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\right)=\left(a\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)$$
76		lmodabl	$$⊢W\in \mathrm{LMod}\to W\in \mathrm{Abel}$$
77	27 76	syl	$$⊢\phi \to W\in \mathrm{Abel}$$
78	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$$
79	27 22 7 78	syl3anc	$$⊢\phi \to d\underset{\dot{}}{·}X\in V$$
80	1 14 13 15	lmodvscl	$$⊢\left(W\in \mathrm{LMod}\wedge e\in B\wedge X\in V\right)\to e\underset{\dot{}}{·}X\in V$$
81	27 23 7 80	syl3anc	$$⊢\phi \to e\underset{\dot{}}{·}X\in V$$
82	1 14 13 15	lmodvscl	$$⊢\left(W\in \mathrm{LMod}\wedge d\in B\wedge Y\in V\right)\to d\underset{\dot{}}{·}Y\in V$$
83	27 22 28 82	syl3anc	$$⊢\phi \to d\underset{\dot{}}{·}Y\in V$$
84	1 14 13 15	lmodvscl	$$⊢\left(W\in \mathrm{LMod}\wedge e\in B\wedge Z\in V\right)\to e\underset{\dot{}}{·}Z\in V$$
85	27 23 31 84	syl3anc	$$⊢\phi \to e\underset{\dot{}}{·}Z\in V$$
86	1 12 2	ablsub4	$$⊢\left(W\in \mathrm{Abel}\wedge \left(d\underset{\dot{}}{·}X\in V\wedge e\underset{\dot{}}{·}X\in V\right)\wedge \left(d\underset{\dot{}}{·}Y\in V\wedge e\underset{\dot{}}{·}Z\in V\right)\right)\to \left(\left(d\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}X\right)\right)\underset{\dot{}}{-}\left(\left(d\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Z\right)\right)=\left(\left(d\underset{\dot{}}{·}X\right)\underset{\dot{}}{-}\left(d\underset{\dot{}}{·}Y\right)\right)\underset{\dot{}}{+}\left(\left(e\underset{\dot{}}{·}X\right)\underset{\dot{}}{-}\left(e\underset{\dot{}}{·}Z\right)\right)$$
87	77 79 81 83 85 86	syl122anc	$$⊢\phi \to \left(\left(d\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}X\right)\right)\underset{\dot{}}{-}\left(\left(d\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Z\right)\right)=\left(\left(d\underset{\dot{}}{·}X\right)\underset{\dot{}}{-}\left(d\underset{\dot{}}{·}Y\right)\right)\underset{\dot{}}{+}\left(\left(e\underset{\dot{}}{·}X\right)\underset{\dot{}}{-}\left(e\underset{\dot{}}{·}Z\right)\right)$$
88	1 12 14 13 15 16	lmodvsdir	$$⊢\left(W\in \mathrm{LMod}\wedge \left(d\in B\wedge e\in B\wedge X\in V\right)\right)\to \left(d\underset{\dot{}}{⨣}e\right)\underset{\dot{}}{·}X=\left(d\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}X\right)$$
89	27 22 23 7 88	syl13anc	$$⊢\phi \to \left(d\underset{\dot{}}{⨣}e\right)\underset{\dot{}}{·}X=\left(d\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}X\right)$$
90	89	oveq1d	$$⊢\phi \to \left(\left(d\underset{\dot{}}{⨣}e\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{-}\left(\left(d\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Z\right)\right)=\left(\left(d\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}X\right)\right)\underset{\dot{}}{-}\left(\left(d\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Z\right)\right)$$
91	1 13 14 15 2 27 22 7 28	lmodsubdi	$$⊢\phi \to d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Y\right)=\left(d\underset{\dot{}}{·}X\right)\underset{\dot{}}{-}\left(d\underset{\dot{}}{·}Y\right)$$
92	1 13 14 15 2 27 23 7 31	lmodsubdi	$$⊢\phi \to e\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)=\left(e\underset{\dot{}}{·}X\right)\underset{\dot{}}{-}\left(e\underset{\dot{}}{·}Z\right)$$
93	91 92	oveq12d	$$⊢\phi \to \left(d\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Y\right)\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}\left(X\underset{\dot{}}{-}Z\right)\right)=\left(\left(d\underset{\dot{}}{·}X\right)\underset{\dot{}}{-}\left(d\underset{\dot{}}{·}Y\right)\right)\underset{\dot{}}{+}\left(\left(e\underset{\dot{}}{·}X\right)\underset{\dot{}}{-}\left(e\underset{\dot{}}{·}Z\right)\right)$$
94	25 93	eqtrd	$$⊢\phi \to j=\left(\left(d\underset{\dot{}}{·}X\right)\underset{\dot{}}{-}\left(d\underset{\dot{}}{·}Y\right)\right)\underset{\dot{}}{+}\left(\left(e\underset{\dot{}}{·}X\right)\underset{\dot{}}{-}\left(e\underset{\dot{}}{·}Z\right)\right)$$
95	87 90 94	3eqtr4rd	$$⊢\phi \to j=\left(\left(d\underset{\dot{}}{⨣}e\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{-}\left(\left(d\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Z\right)\right)$$
96	1 14 13 15	lmodvscl	$$⊢\left(W\in \mathrm{LMod}\wedge d\underset{\dot{}}{⨣}e\in B\wedge X\in V\right)\to \left(d\underset{\dot{}}{⨣}e\right)\underset{\dot{}}{·}X\in V$$
97	27 64 7 96	syl3anc	$$⊢\phi \to \left(d\underset{\dot{}}{⨣}e\right)\underset{\dot{}}{·}X\in V$$
98	1 12	lmodvacl	$$⊢\left(W\in \mathrm{LMod}\wedge d\underset{\dot{}}{·}Y\in V\wedge e\underset{\dot{}}{·}Z\in V\right)\to \left(d\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Z\right)\in V$$
99	27 83 85 98	syl3anc	$$⊢\phi \to \left(d\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Z\right)\in V$$
100	1 12 58 2	grpsubval	$$⊢\left(\left(d\underset{\dot{}}{⨣}e\right)\underset{\dot{}}{·}X\in V\wedge \left(d\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Z\right)\in V\right)\to \left(\left(d\underset{\dot{}}{⨣}e\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{-}\left(\left(d\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Z\right)\right)=\left(\left(d\underset{\dot{}}{⨣}e\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}{inv}_g\left(W\right)\left(\left(d\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Z\right)\right)$$
101	97 99 100	syl2anc	$$⊢\phi \to \left(\left(d\underset{\dot{}}{⨣}e\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{-}\left(\left(d\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Z\right)\right)=\left(\left(d\underset{\dot{}}{⨣}e\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}{inv}_g\left(W\right)\left(\left(d\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Z\right)\right)$$
102	95 24 101	3eqtr3d	$$⊢\phi \to \left(a\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)=\left(\left(d\underset{\dot{}}{⨣}e\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}{inv}_g\left(W\right)\left(\left(d\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Z\right)\right)$$
103	67 75 102	3eqtrd	$$⊢\phi \to \left(Q\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(\left(a\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)\right)=\left(\left(d\underset{\dot{}}{⨣}e\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}{inv}_g\left(W\right)\left(\left(d\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Z\right)\right)$$
104	1 12 14 15 13 54 6 55 7 8 56 60 62 64 103	lvecindp	$$⊢\phi \to \left(Q=d\underset{\dot{}}{⨣}e\wedge \left(a\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)={inv}_g\left(W\right)\left(\left(d\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Z\right)\right)\right)$$
105	104	simpld	$$⊢\phi \to Q=d\underset{\dot{}}{⨣}e$$
106	105	fveq2d	$$⊢\phi \to I\left(Q\right)=I\left(d\underset{\dot{}}{⨣}e\right)$$
107	15 19	grpinvcl	$$⊢\left(R\in \mathrm{Grp}\wedge d\in B\right)\to I\left(d\right)\in B$$
108	41 22 107	syl2anc	$$⊢\phi \to I\left(d\right)\in B$$
109	15 19	grpinvcl	$$⊢\left(R\in \mathrm{Grp}\wedge e\in B\right)\to I\left(e\right)\in B$$
110	41 23 109	syl2anc	$$⊢\phi \to I\left(e\right)\in B$$
111	104	simprd	$$⊢\phi \to \left(a\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)={inv}_g\left(W\right)\left(\left(d\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Z\right)\right)$$
112	1 12 13 58 14 15 19 27 22 23 28 31	lmodnegadd	$$⊢\phi \to {inv}_g\left(W\right)\left(\left(d\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(e\underset{\dot{}}{·}Z\right)\right)=\left(I\left(d\right)\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(I\left(e\right)\underset{\dot{}}{·}Z\right)$$
113	111 112	eqtrd	$$⊢\phi \to \left(a\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)=\left(I\left(d\right)\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(I\left(e\right)\underset{\dot{}}{·}Z\right)$$
114	1 12 14 15 13 3 5 6 10 11 20 21 108 110 9 113	lvecindp2	$$⊢\phi \to \left(a=I\left(d\right)\wedge b=I\left(e\right)\right)$$
115		oveq12	$$⊢\left(a=I\left(d\right)\wedge b=I\left(e\right)\right)\to a\underset{\dot{}}{⨣}b=I\left(d\right)\underset{\dot{}}{⨣}I\left(e\right)$$
116	114 115	syl	$$⊢\phi \to a\underset{\dot{}}{⨣}b=I\left(d\right)\underset{\dot{}}{⨣}I\left(e\right)$$
117	53 106 116	3eqtr4rd	$$⊢\phi \to a\underset{\dot{}}{⨣}b=I\left(Q\right)$$
118	18 19	grpinvid	$$⊢R\in \mathrm{Grp}\to I\left(Q\right)=Q$$
119	41 118	syl	$$⊢\phi \to I\left(Q\right)=Q$$
120	117 119	eqtrd	$$⊢\phi \to a\underset{\dot{}}{⨣}b=Q$$
121	15 16 18 19	grpinvid1	$$⊢\left(R\in \mathrm{Grp}\wedge a\in B\wedge b\in B\right)\to \left(I\left(a\right)=b\leftrightarrow a\underset{\dot{}}{⨣}b=Q\right)$$
122	41 20 21 121	syl3anc	$$⊢\phi \to \left(I\left(a\right)=b\leftrightarrow a\underset{\dot{}}{⨣}b=Q\right)$$
123	120 122	mpbird	$$⊢\phi \to I\left(a\right)=b$$
124	49 123	eqtrd	$$⊢\phi \to I\left(1_R\right){\cdot }_{R}a=b$$
125	124	oveq1d	$$⊢\phi \to \left(I\left(1_R\right){\cdot }_{R}a\right)\underset{\dot{}}{·}Z=b\underset{\dot{}}{·}Z$$
126	48 125	eqtr3d	$$⊢\phi \to I\left(1_R\right)\underset{\dot{}}{·}\left(a\underset{\dot{}}{·}Z\right)=b\underset{\dot{}}{·}Z$$
127	126	oveq2d	$$⊢\phi \to \left(a\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(I\left(1_R\right)\underset{\dot{}}{·}\left(a\underset{\dot{}}{·}Z\right)\right)=\left(a\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}Z\right)$$
128	24 127	eqtr4d	$$⊢\phi \to j=\left(a\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(I\left(1_R\right)\underset{\dot{}}{·}\left(a\underset{\dot{}}{·}Z\right)\right)$$
129	36 37 128	3eqtr4rd	$$⊢\phi \to j=a\underset{\dot{}}{·}\left(Y\underset{\dot{}}{-}Z\right)$$