Theorem lcvexchlem1

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$$
Assertion	lcvexchlem1	$$⊢\phi \to \left(T\subset T\underset{\dot{}}{\oplus }U\leftrightarrow T\cap U\subset U\right)$$

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	1	lsssssubg	$$⊢W\in \mathrm{LMod}\to S\subseteq \mathrm{SubGrp}\left(W\right)$$
8	4 7	syl	$$⊢\phi \to S\subseteq \mathrm{SubGrp}\left(W\right)$$
9	8 5	sseldd	$$⊢\phi \to T\in \mathrm{SubGrp}\left(W\right)$$
10	8 6	sseldd	$$⊢\phi \to U\in \mathrm{SubGrp}\left(W\right)$$
11	2	lsmub1	$$⊢\left(T\in \mathrm{SubGrp}\left(W\right)\wedge U\in \mathrm{SubGrp}\left(W\right)\right)\to T\subseteq T\underset{\dot{}}{\oplus }U$$
12	9 10 11	syl2anc	$$⊢\phi \to T\subseteq T\underset{\dot{}}{\oplus }U$$
13		inss2	$$⊢T\cap U\subseteq U$$
14	13	a1i	$$⊢\phi \to T\cap U\subseteq U$$
15	12 14	2thd	$$⊢\phi \to \left(T\subseteq T\underset{\dot{}}{\oplus }U\leftrightarrow T\cap U\subseteq U\right)$$
16	2	lsmss2b	$$⊢\left(T\in \mathrm{SubGrp}\left(W\right)\wedge U\in \mathrm{SubGrp}\left(W\right)\right)\to \left(U\subseteq T\leftrightarrow T\underset{\dot{}}{\oplus }U=T\right)$$
17	9 10 16	syl2anc	$$⊢\phi \to \left(U\subseteq T\leftrightarrow T\underset{\dot{}}{\oplus }U=T\right)$$
18		eqcom	$$⊢T\underset{\dot{}}{\oplus }U=T\leftrightarrow T=T\underset{\dot{}}{\oplus }U$$
19	17 18	bitrdi	$$⊢\phi \to \left(U\subseteq T\leftrightarrow T=T\underset{\dot{}}{\oplus }U\right)$$
20		sseqin2	$$⊢U\subseteq T\leftrightarrow T\cap U=U$$
21	19 20	bitr3di	$$⊢\phi \to \left(T=T\underset{\dot{}}{\oplus }U\leftrightarrow T\cap U=U\right)$$
22	21	necon3bid	$$⊢\phi \to \left(T\ne T\underset{\dot{}}{\oplus }U\leftrightarrow T\cap U\ne U\right)$$
23	15 22	anbi12d	$$⊢\phi \to \left(\left(T\subseteq T\underset{\dot{}}{\oplus }U\wedge T\ne T\underset{\dot{}}{\oplus }U\right)\leftrightarrow \left(T\cap U\subseteq U\wedge T\cap U\ne U\right)\right)$$
24		df-pss	$$⊢T\subset T\underset{\dot{}}{\oplus }U\leftrightarrow \left(T\subseteq T\underset{\dot{}}{\oplus }U\wedge T\ne T\underset{\dot{}}{\oplus }U\right)$$
25		df-pss	$$⊢T\cap U\subset U\leftrightarrow \left(T\cap U\subseteq U\wedge T\cap U\ne U\right)$$
26	23 24 25	3bitr4g	$$⊢\phi \to \left(T\subset T\underset{\dot{}}{\oplus }U\leftrightarrow T\cap U\subset U\right)$$