Theorem baerlem5blem1

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