Theorem lcvexchlem3

Description: Lemma for lcvexch . (Contributed by NM, 10-Jan-2015)

	Ref	Expression
Hypotheses	lcvexch.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
	lcvexch.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(W\right)$$
	lcvexch.c	$$⊢C={⋖}_L\left(W\right)$$
	lcvexch.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	lcvexch.t	$$⊢\phi \to T\in S$$
	lcvexch.u	$$⊢\phi \to U\in S$$
	lcvexch.q	$$⊢\phi \to R\in S$$
	lcvexch.d	$$⊢\phi \to T\subseteq R$$
	lcvexch.e	$$⊢\phi \to R\subseteq T\underset{\dot{}}{\oplus }U$$
Assertion	lcvexchlem3	$$⊢\phi \to \left(R\cap U\right)\underset{\dot{}}{\oplus }T=R$$

Proof

Step	Hyp	Ref	Expression
1		lcvexch.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
2		lcvexch.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(W\right)$$
3		lcvexch.c	$$⊢C={⋖}_L\left(W\right)$$
4		lcvexch.w	$$⊢\phi \to W\in \mathrm{LMod}$$
5		lcvexch.t	$$⊢\phi \to T\in S$$
6		lcvexch.u	$$⊢\phi \to U\in S$$
7		lcvexch.q	$$⊢\phi \to R\in S$$
8		lcvexch.d	$$⊢\phi \to T\subseteq R$$
9		lcvexch.e	$$⊢\phi \to R\subseteq T\underset{\dot{}}{\oplus }U$$
10	1	lsssssubg	$$⊢W\in \mathrm{LMod}\to S\subseteq \mathrm{SubGrp}\left(W\right)$$
11	4 10	syl	$$⊢\phi \to S\subseteq \mathrm{SubGrp}\left(W\right)$$
12	11 7	sseldd	$$⊢\phi \to R\in \mathrm{SubGrp}\left(W\right)$$
13	11 6	sseldd	$$⊢\phi \to U\in \mathrm{SubGrp}\left(W\right)$$
14	11 5	sseldd	$$⊢\phi \to T\in \mathrm{SubGrp}\left(W\right)$$
15	2	lsmmod2	$$⊢\left(\left(R\in \mathrm{SubGrp}\left(W\right)\wedge U\in \mathrm{SubGrp}\left(W\right)\wedge T\in \mathrm{SubGrp}\left(W\right)\right)\wedge T\subseteq R\right)\to R\cap \left(U\underset{\dot{}}{\oplus }T\right)=\left(R\cap U\right)\underset{\dot{}}{\oplus }T$$
16	12 13 14 8 15	syl31anc	$$⊢\phi \to R\cap \left(U\underset{\dot{}}{\oplus }T\right)=\left(R\cap U\right)\underset{\dot{}}{\oplus }T$$
17		lmodabl	$$⊢W\in \mathrm{LMod}\to W\in \mathrm{Abel}$$
18	4 17	syl	$$⊢\phi \to W\in \mathrm{Abel}$$
19	2	lsmcom	$$⊢\left(W\in \mathrm{Abel}\wedge T\in \mathrm{SubGrp}\left(W\right)\wedge U\in \mathrm{SubGrp}\left(W\right)\right)\to T\underset{\dot{}}{\oplus }U=U\underset{\dot{}}{\oplus }T$$
20	18 14 13 19	syl3anc	$$⊢\phi \to T\underset{\dot{}}{\oplus }U=U\underset{\dot{}}{\oplus }T$$
21	9 20	sseqtrd	$$⊢\phi \to R\subseteq U\underset{\dot{}}{\oplus }T$$
22		dfss2	$$⊢R\subseteq U\underset{\dot{}}{\oplus }T\leftrightarrow R\cap \left(U\underset{\dot{}}{\oplus }T\right)=R$$
23	21 22	sylib	$$⊢\phi \to R\cap \left(U\underset{\dot{}}{\oplus }T\right)=R$$
24	16 23	eqtr3d	$$⊢\phi \to \left(R\cap U\right)\underset{\dot{}}{\oplus }T=R$$