Theorem lcvexchlem5

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.g	$$⊢\phi \to \left(T\cap U\right)CU$$
Assertion	lcvexchlem5	$$⊢\phi \to TC\left(T\underset{\dot{}}{\oplus }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		lcvexch.g	$$⊢\phi \to \left(T\cap U\right)CU$$
8	1	lssincl	$$⊢\left(W\in \mathrm{LMod}\wedge T\in S\wedge U\in S\right)\to T\cap U\in S$$
9	4 5 6 8	syl3anc	$$⊢\phi \to T\cap U\in S$$
10	1 3 4 9 6 7	lcvpss	$$⊢\phi \to T\cap U\subset U$$
11	1 2 3 4 5 6	lcvexchlem1	$$⊢\phi \to \left(T\subset T\underset{\dot{}}{\oplus }U\leftrightarrow T\cap U\subset U\right)$$
12	10 11	mpbird	$$⊢\phi \to T\subset T\underset{\dot{}}{\oplus }U$$
13		simp3l	$$⊢\left(\phi \wedge s\in S\wedge \left(T\subseteq s\wedge s\subseteq T\underset{\dot{}}{\oplus }U\right)\right)\to T\subseteq s$$
14	13	ssrind	$$⊢\left(\phi \wedge s\in S\wedge \left(T\subseteq s\wedge s\subseteq T\underset{\dot{}}{\oplus }U\right)\right)\to T\cap U\subseteq s\cap U$$
15		inss2	$$⊢s\cap U\subseteq U$$
16	14 15	jctir	$$⊢\left(\phi \wedge s\in S\wedge \left(T\subseteq s\wedge s\subseteq T\underset{\dot{}}{\oplus }U\right)\right)\to \left(T\cap U\subseteq s\cap U\wedge s\cap U\subseteq U\right)$$
17	7	3ad2ant1	$$⊢\left(\phi \wedge s\in S\wedge \left(T\subseteq s\wedge s\subseteq T\underset{\dot{}}{\oplus }U\right)\right)\to \left(T\cap U\right)CU$$
18	1 3 4 9 6	lcvbr3	$$⊢\phi \to \left(\left(T\cap U\right)CU\leftrightarrow \left(T\cap U\subset U\wedge \forall r\in S\left(\left(T\cap U\subseteq r\wedge r\subseteq U\right)\to \left(r=T\cap U\vee r=U\right)\right)\right)\right)$$
19	18	adantr	$$⊢\left(\phi \wedge s\in S\right)\to \left(\left(T\cap U\right)CU\leftrightarrow \left(T\cap U\subset U\wedge \forall r\in S\left(\left(T\cap U\subseteq r\wedge r\subseteq U\right)\to \left(r=T\cap U\vee r=U\right)\right)\right)\right)$$
20	4	adantr	$$⊢\left(\phi \wedge s\in S\right)\to W\in \mathrm{LMod}$$
21		simpr	$$⊢\left(\phi \wedge s\in S\right)\to s\in S$$
22	6	adantr	$$⊢\left(\phi \wedge s\in S\right)\to U\in S$$
23	1	lssincl	$$⊢\left(W\in \mathrm{LMod}\wedge s\in S\wedge U\in S\right)\to s\cap U\in S$$
24	20 21 22 23	syl3anc	$$⊢\left(\phi \wedge s\in S\right)\to s\cap U\in S$$
25		sseq2	$$⊢r=s\cap U\to \left(T\cap U\subseteq r\leftrightarrow T\cap U\subseteq s\cap U\right)$$
26		sseq1	$$⊢r=s\cap U\to \left(r\subseteq U\leftrightarrow s\cap U\subseteq U\right)$$
27	25 26	anbi12d	$$⊢r=s\cap U\to \left(\left(T\cap U\subseteq r\wedge r\subseteq U\right)\leftrightarrow \left(T\cap U\subseteq s\cap U\wedge s\cap U\subseteq U\right)\right)$$
28		eqeq1	$$⊢r=s\cap U\to \left(r=T\cap U\leftrightarrow s\cap U=T\cap U\right)$$
29		eqeq1	$$⊢r=s\cap U\to \left(r=U\leftrightarrow s\cap U=U\right)$$
30	28 29	orbi12d	$$⊢r=s\cap U\to \left(\left(r=T\cap U\vee r=U\right)\leftrightarrow \left(s\cap U=T\cap U\vee s\cap U=U\right)\right)$$
31	27 30	imbi12d	$$⊢r=s\cap U\to \left(\left(\left(T\cap U\subseteq r\wedge r\subseteq U\right)\to \left(r=T\cap U\vee r=U\right)\right)\leftrightarrow \left(\left(T\cap U\subseteq s\cap U\wedge s\cap U\subseteq U\right)\to \left(s\cap U=T\cap U\vee s\cap U=U\right)\right)\right)$$
32	31	rspcv	$$⊢s\cap U\in S\to \left(\forall r\in S\left(\left(T\cap U\subseteq r\wedge r\subseteq U\right)\to \left(r=T\cap U\vee r=U\right)\right)\to \left(\left(T\cap U\subseteq s\cap U\wedge s\cap U\subseteq U\right)\to \left(s\cap U=T\cap U\vee s\cap U=U\right)\right)\right)$$
33	24 32	syl	$$⊢\left(\phi \wedge s\in S\right)\to \left(\forall r\in S\left(\left(T\cap U\subseteq r\wedge r\subseteq U\right)\to \left(r=T\cap U\vee r=U\right)\right)\to \left(\left(T\cap U\subseteq s\cap U\wedge s\cap U\subseteq U\right)\to \left(s\cap U=T\cap U\vee s\cap U=U\right)\right)\right)$$
34	33	adantld	$$⊢\left(\phi \wedge s\in S\right)\to \left(\left(T\cap U\subset U\wedge \forall r\in S\left(\left(T\cap U\subseteq r\wedge r\subseteq U\right)\to \left(r=T\cap U\vee r=U\right)\right)\right)\to \left(\left(T\cap U\subseteq s\cap U\wedge s\cap U\subseteq U\right)\to \left(s\cap U=T\cap U\vee s\cap U=U\right)\right)\right)$$
35	19 34	sylbid	$$⊢\left(\phi \wedge s\in S\right)\to \left(\left(T\cap U\right)CU\to \left(\left(T\cap U\subseteq s\cap U\wedge s\cap U\subseteq U\right)\to \left(s\cap U=T\cap U\vee s\cap U=U\right)\right)\right)$$
36	35	3adant3	$$⊢\left(\phi \wedge s\in S\wedge \left(T\subseteq s\wedge s\subseteq T\underset{\dot{}}{\oplus }U\right)\right)\to \left(\left(T\cap U\right)CU\to \left(\left(T\cap U\subseteq s\cap U\wedge s\cap U\subseteq U\right)\to \left(s\cap U=T\cap U\vee s\cap U=U\right)\right)\right)$$
37	17 36	mpd	$$⊢\left(\phi \wedge s\in S\wedge \left(T\subseteq s\wedge s\subseteq T\underset{\dot{}}{\oplus }U\right)\right)\to \left(\left(T\cap U\subseteq s\cap U\wedge s\cap U\subseteq U\right)\to \left(s\cap U=T\cap U\vee s\cap U=U\right)\right)$$
38	16 37	mpd	$$⊢\left(\phi \wedge s\in S\wedge \left(T\subseteq s\wedge s\subseteq T\underset{\dot{}}{\oplus }U\right)\right)\to \left(s\cap U=T\cap U\vee s\cap U=U\right)$$
39		oveq1	$$⊢s\cap U=T\cap U\to \left(s\cap U\right)\underset{\dot{}}{\oplus }T=\left(T\cap U\right)\underset{\dot{}}{\oplus }T$$
40	4	3ad2ant1	$$⊢\left(\phi \wedge s\in S\wedge \left(T\subseteq s\wedge s\subseteq T\underset{\dot{}}{\oplus }U\right)\right)\to W\in \mathrm{LMod}$$
41	5	3ad2ant1	$$⊢\left(\phi \wedge s\in S\wedge \left(T\subseteq s\wedge s\subseteq T\underset{\dot{}}{\oplus }U\right)\right)\to T\in S$$
42	6	3ad2ant1	$$⊢\left(\phi \wedge s\in S\wedge \left(T\subseteq s\wedge s\subseteq T\underset{\dot{}}{\oplus }U\right)\right)\to U\in S$$
43		simp2	$$⊢\left(\phi \wedge s\in S\wedge \left(T\subseteq s\wedge s\subseteq T\underset{\dot{}}{\oplus }U\right)\right)\to s\in S$$
44		simp3r	$$⊢\left(\phi \wedge s\in S\wedge \left(T\subseteq s\wedge s\subseteq T\underset{\dot{}}{\oplus }U\right)\right)\to s\subseteq T\underset{\dot{}}{\oplus }U$$
45	1 2 3 40 41 42 43 13 44	lcvexchlem3	$$⊢\left(\phi \wedge s\in S\wedge \left(T\subseteq s\wedge s\subseteq T\underset{\dot{}}{\oplus }U\right)\right)\to \left(s\cap U\right)\underset{\dot{}}{\oplus }T=s$$
46	1	lsssssubg	$$⊢W\in \mathrm{LMod}\to S\subseteq \mathrm{SubGrp}\left(W\right)$$
47	4 46	syl	$$⊢\phi \to S\subseteq \mathrm{SubGrp}\left(W\right)$$
48	47 9	sseldd	$$⊢\phi \to T\cap U\in \mathrm{SubGrp}\left(W\right)$$
49	47 5	sseldd	$$⊢\phi \to T\in \mathrm{SubGrp}\left(W\right)$$
50		inss1	$$⊢T\cap U\subseteq T$$
51	50	a1i	$$⊢\phi \to T\cap U\subseteq T$$
52	2	lsmss1	$$⊢\left(T\cap U\in \mathrm{SubGrp}\left(W\right)\wedge T\in \mathrm{SubGrp}\left(W\right)\wedge T\cap U\subseteq T\right)\to \left(T\cap U\right)\underset{\dot{}}{\oplus }T=T$$
53	48 49 51 52	syl3anc	$$⊢\phi \to \left(T\cap U\right)\underset{\dot{}}{\oplus }T=T$$
54	53	3ad2ant1	$$⊢\left(\phi \wedge s\in S\wedge \left(T\subseteq s\wedge s\subseteq T\underset{\dot{}}{\oplus }U\right)\right)\to \left(T\cap U\right)\underset{\dot{}}{\oplus }T=T$$
55	45 54	eqeq12d	$$⊢\left(\phi \wedge s\in S\wedge \left(T\subseteq s\wedge s\subseteq T\underset{\dot{}}{\oplus }U\right)\right)\to \left(\left(s\cap U\right)\underset{\dot{}}{\oplus }T=\left(T\cap U\right)\underset{\dot{}}{\oplus }T\leftrightarrow s=T\right)$$
56	39 55	syl5ib	$$⊢\left(\phi \wedge s\in S\wedge \left(T\subseteq s\wedge s\subseteq T\underset{\dot{}}{\oplus }U\right)\right)\to \left(s\cap U=T\cap U\to s=T\right)$$
57		oveq1	$$⊢s\cap U=U\to \left(s\cap U\right)\underset{\dot{}}{\oplus }T=U\underset{\dot{}}{\oplus }T$$
58		lmodabl	$$⊢W\in \mathrm{LMod}\to W\in \mathrm{Abel}$$
59	4 58	syl	$$⊢\phi \to W\in \mathrm{Abel}$$
60	47 6	sseldd	$$⊢\phi \to U\in \mathrm{SubGrp}\left(W\right)$$
61	2	lsmcom	$$⊢\left(W\in \mathrm{Abel}\wedge U\in \mathrm{SubGrp}\left(W\right)\wedge T\in \mathrm{SubGrp}\left(W\right)\right)\to U\underset{\dot{}}{\oplus }T=T\underset{\dot{}}{\oplus }U$$
62	59 60 49 61	syl3anc	$$⊢\phi \to U\underset{\dot{}}{\oplus }T=T\underset{\dot{}}{\oplus }U$$
63	62	3ad2ant1	$$⊢\left(\phi \wedge s\in S\wedge \left(T\subseteq s\wedge s\subseteq T\underset{\dot{}}{\oplus }U\right)\right)\to U\underset{\dot{}}{\oplus }T=T\underset{\dot{}}{\oplus }U$$
64	45 63	eqeq12d	$$⊢\left(\phi \wedge s\in S\wedge \left(T\subseteq s\wedge s\subseteq T\underset{\dot{}}{\oplus }U\right)\right)\to \left(\left(s\cap U\right)\underset{\dot{}}{\oplus }T=U\underset{\dot{}}{\oplus }T\leftrightarrow s=T\underset{\dot{}}{\oplus }U\right)$$
65	57 64	syl5ib	$$⊢\left(\phi \wedge s\in S\wedge \left(T\subseteq s\wedge s\subseteq T\underset{\dot{}}{\oplus }U\right)\right)\to \left(s\cap U=U\to s=T\underset{\dot{}}{\oplus }U\right)$$
66	56 65	orim12d	$$⊢\left(\phi \wedge s\in S\wedge \left(T\subseteq s\wedge s\subseteq T\underset{\dot{}}{\oplus }U\right)\right)\to \left(\left(s\cap U=T\cap U\vee s\cap U=U\right)\to \left(s=T\vee s=T\underset{\dot{}}{\oplus }U\right)\right)$$
67	38 66	mpd	$$⊢\left(\phi \wedge s\in S\wedge \left(T\subseteq s\wedge s\subseteq T\underset{\dot{}}{\oplus }U\right)\right)\to \left(s=T\vee s=T\underset{\dot{}}{\oplus }U\right)$$
68	67	3exp	$$⊢\phi \to \left(s\in S\to \left(\left(T\subseteq s\wedge s\subseteq T\underset{\dot{}}{\oplus }U\right)\to \left(s=T\vee s=T\underset{\dot{}}{\oplus }U\right)\right)\right)$$
69	68	ralrimiv	$$⊢\phi \to \forall s\in S\left(\left(T\subseteq s\wedge s\subseteq T\underset{\dot{}}{\oplus }U\right)\to \left(s=T\vee s=T\underset{\dot{}}{\oplus }U\right)\right)$$
70	1 2	lsmcl	$$⊢\left(W\in \mathrm{LMod}\wedge T\in S\wedge U\in S\right)\to T\underset{\dot{}}{\oplus }U\in S$$
71	4 5 6 70	syl3anc	$$⊢\phi \to T\underset{\dot{}}{\oplus }U\in S$$
72	1 3 4 5 71	lcvbr3	$$⊢\phi \to \left(TC\left(T\underset{\dot{}}{\oplus }U\right)\leftrightarrow \left(T\subset T\underset{\dot{}}{\oplus }U\wedge \forall s\in S\left(\left(T\subseteq s\wedge s\subseteq T\underset{\dot{}}{\oplus }U\right)\to \left(s=T\vee s=T\underset{\dot{}}{\oplus }U\right)\right)\right)\right)$$
73	12 69 72	mpbir2and	$$⊢\phi \to TC\left(T\underset{\dot{}}{\oplus }U\right)$$