lcvexchlem4

	Ref	Expression
Hypotheses	lcvexch.s	$⊢ S = LSubSp (W)$
	lcvexch.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
	lcvexch.c	$⊢ C = ⋖_{L} (W)$
	lcvexch.w	$⊢ φ \to W \in LMod$
	lcvexch.t	$⊢ φ \to T \in S$
	lcvexch.u	$⊢ φ \to U \in S$
	lcvexch.f	$⊢ φ \to T C (T \underset{˙}{\oplus} U)$
Assertion	lcvexchlem4	$⊢ φ \to (T \cap U) C U$

Proof

Step	Hyp	Ref	Expression
1		lcvexch.s	$⊢ S = LSubSp (W)$
2		lcvexch.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
3		lcvexch.c	$⊢ C = ⋖_{L} (W)$
4		lcvexch.w	$⊢ φ \to W \in LMod$
5		lcvexch.t	$⊢ φ \to T \in S$
6		lcvexch.u	$⊢ φ \to U \in S$
7		lcvexch.f	$⊢ φ \to T C (T \underset{˙}{\oplus} U)$
8	1 2	lsmcl	$⊢ (W \in LMod \land T \in S \land U \in S) \to T \underset{˙}{\oplus} U \in S$
9	4 5 6 8	syl3anc	$⊢ φ \to T \underset{˙}{\oplus} U \in S$
10	1 3 4 5 9 7	lcvpss	$⊢ φ \to T \subset T \underset{˙}{\oplus} U$
11	1 2 3 4 5 6	lcvexchlem1	$⊢ φ \to (T \subset T \underset{˙}{\oplus} U \leftrightarrow T \cap U \subset U)$
12	10 11	mpbid	$⊢ φ \to T \cap U \subset U$
13	4	3ad2ant1	$⊢ (φ \land s \in S \land (T \cap U \subseteq s \land s \subseteq U)) \to W \in LMod$
14	1	lsssssubg	$⊢ W \in LMod \to S \subseteq SubGrp (W)$
15	13 14	syl	$⊢ (φ \land s \in S \land (T \cap U \subseteq s \land s \subseteq U)) \to S \subseteq SubGrp (W)$
16		simp2	$⊢ (φ \land s \in S \land (T \cap U \subseteq s \land s \subseteq U)) \to s \in S$
17	15 16	sseldd	$⊢ (φ \land s \in S \land (T \cap U \subseteq s \land s \subseteq U)) \to s \in SubGrp (W)$
18	5	3ad2ant1	$⊢ (φ \land s \in S \land (T \cap U \subseteq s \land s \subseteq U)) \to T \in S$
19	15 18	sseldd	$⊢ (φ \land s \in S \land (T \cap U \subseteq s \land s \subseteq U)) \to T \in SubGrp (W)$
20	2	lsmub2	$⊢ (s \in SubGrp (W) \land T \in SubGrp (W)) \to T \subseteq s \underset{˙}{\oplus} T$
21	17 19 20	syl2anc	$⊢ (φ \land s \in S \land (T \cap U \subseteq s \land s \subseteq U)) \to T \subseteq s \underset{˙}{\oplus} T$
22	6	3ad2ant1	$⊢ (φ \land s \in S \land (T \cap U \subseteq s \land s \subseteq U)) \to U \in S$
23	15 22	sseldd	$⊢ (φ \land s \in S \land (T \cap U \subseteq s \land s \subseteq U)) \to U \in SubGrp (W)$
24		simp3r	$⊢ (φ \land s \in S \land (T \cap U \subseteq s \land s \subseteq U)) \to s \subseteq U$
25	2	lsmless1	$⊢ (U \in SubGrp (W) \land T \in SubGrp (W) \land s \subseteq U) \to s \underset{˙}{\oplus} T \subseteq U \underset{˙}{\oplus} T$
26	23 19 24 25	syl3anc	$⊢ (φ \land s \in S \land (T \cap U \subseteq s \land s \subseteq U)) \to s \underset{˙}{\oplus} T \subseteq U \underset{˙}{\oplus} T$
27		lmodabl	$⊢ W \in LMod \to W \in Abel$
28	4 27	syl	$⊢ φ \to W \in Abel$
29	4 14	syl	$⊢ φ \to S \subseteq SubGrp (W)$
30	29 5	sseldd	$⊢ φ \to T \in SubGrp (W)$
31	29 6	sseldd	$⊢ φ \to U \in SubGrp (W)$
32	2	lsmcom	$⊢ (W \in Abel \land T \in SubGrp (W) \land U \in SubGrp (W)) \to T \underset{˙}{\oplus} U = U \underset{˙}{\oplus} T$
33	28 30 31 32	syl3anc	$⊢ φ \to T \underset{˙}{\oplus} U = U \underset{˙}{\oplus} T$
34	33	3ad2ant1	$⊢ (φ \land s \in S \land (T \cap U \subseteq s \land s \subseteq U)) \to T \underset{˙}{\oplus} U = U \underset{˙}{\oplus} T$
35	26 34	sseqtrrd	$⊢ (φ \land s \in S \land (T \cap U \subseteq s \land s \subseteq U)) \to s \underset{˙}{\oplus} T \subseteq T \underset{˙}{\oplus} U$
36	7	3ad2ant1	$⊢ (φ \land s \in S \land (T \cap U \subseteq s \land s \subseteq U)) \to T C (T \underset{˙}{\oplus} U)$
37	1 3 4 5 9	lcvbr3	$⊢ φ \to (T C (T \underset{˙}{\oplus} U) \leftrightarrow (T \subset T \underset{˙}{\oplus} U \land \forall r \in S ((T \subseteq r \land r \subseteq T \underset{˙}{\oplus} U) \to (r = T \lor r = T \underset{˙}{\oplus} U))))$
38	37	adantr	$⊢ (φ \land s \in S) \to (T C (T \underset{˙}{\oplus} U) \leftrightarrow (T \subset T \underset{˙}{\oplus} U \land \forall r \in S ((T \subseteq r \land r \subseteq T \underset{˙}{\oplus} U) \to (r = T \lor r = T \underset{˙}{\oplus} U))))$
39	4	adantr	$⊢ (φ \land s \in S) \to W \in LMod$
40		simpr	$⊢ (φ \land s \in S) \to s \in S$
41	5	adantr	$⊢ (φ \land s \in S) \to T \in S$
42	1 2	lsmcl	$⊢ (W \in LMod \land s \in S \land T \in S) \to s \underset{˙}{\oplus} T \in S$
43	39 40 41 42	syl3anc	$⊢ (φ \land s \in S) \to s \underset{˙}{\oplus} T \in S$
44		sseq2	$⊢ r = s \underset{˙}{\oplus} T \to (T \subseteq r \leftrightarrow T \subseteq s \underset{˙}{\oplus} T)$
45		sseq1	$⊢ r = s \underset{˙}{\oplus} T \to (r \subseteq T \underset{˙}{\oplus} U \leftrightarrow s \underset{˙}{\oplus} T \subseteq T \underset{˙}{\oplus} U)$
46	44 45	anbi12d	$⊢ r = s \underset{˙}{\oplus} T \to ((T \subseteq r \land r \subseteq T \underset{˙}{\oplus} U) \leftrightarrow (T \subseteq s \underset{˙}{\oplus} T \land s \underset{˙}{\oplus} T \subseteq T \underset{˙}{\oplus} U))$
47		eqeq1	$⊢ r = s \underset{˙}{\oplus} T \to (r = T \leftrightarrow s \underset{˙}{\oplus} T = T)$
48		eqeq1	$⊢ r = s \underset{˙}{\oplus} T \to (r = T \underset{˙}{\oplus} U \leftrightarrow s \underset{˙}{\oplus} T = T \underset{˙}{\oplus} U)$
49	47 48	orbi12d	$⊢ r = s \underset{˙}{\oplus} T \to ((r = T \lor r = T \underset{˙}{\oplus} U) \leftrightarrow (s \underset{˙}{\oplus} T = T \lor s \underset{˙}{\oplus} T = T \underset{˙}{\oplus} U))$
50	46 49	imbi12d	$⊢ r = s \underset{˙}{\oplus} T \to (((T \subseteq r \land r \subseteq T \underset{˙}{\oplus} U) \to (r = T \lor r = T \underset{˙}{\oplus} U)) \leftrightarrow ((T \subseteq s \underset{˙}{\oplus} T \land s \underset{˙}{\oplus} T \subseteq T \underset{˙}{\oplus} U) \to (s \underset{˙}{\oplus} T = T \lor s \underset{˙}{\oplus} T = T \underset{˙}{\oplus} U)))$
51	50	rspcv	$⊢ s \underset{˙}{\oplus} T \in S \to (\forall r \in S ((T \subseteq r \land r \subseteq T \underset{˙}{\oplus} U) \to (r = T \lor r = T \underset{˙}{\oplus} U)) \to ((T \subseteq s \underset{˙}{\oplus} T \land s \underset{˙}{\oplus} T \subseteq T \underset{˙}{\oplus} U) \to (s \underset{˙}{\oplus} T = T \lor s \underset{˙}{\oplus} T = T \underset{˙}{\oplus} U)))$
52	43 51	syl	$⊢ (φ \land s \in S) \to (\forall r \in S ((T \subseteq r \land r \subseteq T \underset{˙}{\oplus} U) \to (r = T \lor r = T \underset{˙}{\oplus} U)) \to ((T \subseteq s \underset{˙}{\oplus} T \land s \underset{˙}{\oplus} T \subseteq T \underset{˙}{\oplus} U) \to (s \underset{˙}{\oplus} T = T \lor s \underset{˙}{\oplus} T = T \underset{˙}{\oplus} U)))$
53	52	adantld	$⊢ (φ \land s \in S) \to ((T \subset T \underset{˙}{\oplus} U \land \forall r \in S ((T \subseteq r \land r \subseteq T \underset{˙}{\oplus} U) \to (r = T \lor r = T \underset{˙}{\oplus} U))) \to ((T \subseteq s \underset{˙}{\oplus} T \land s \underset{˙}{\oplus} T \subseteq T \underset{˙}{\oplus} U) \to (s \underset{˙}{\oplus} T = T \lor s \underset{˙}{\oplus} T = T \underset{˙}{\oplus} U)))$
54	38 53	sylbid	$⊢ (φ \land s \in S) \to (T C (T \underset{˙}{\oplus} U) \to ((T \subseteq s \underset{˙}{\oplus} T \land s \underset{˙}{\oplus} T \subseteq T \underset{˙}{\oplus} U) \to (s \underset{˙}{\oplus} T = T \lor s \underset{˙}{\oplus} T = T \underset{˙}{\oplus} U)))$
55	54	3adant3	$⊢ (φ \land s \in S \land (T \cap U \subseteq s \land s \subseteq U)) \to (T C (T \underset{˙}{\oplus} U) \to ((T \subseteq s \underset{˙}{\oplus} T \land s \underset{˙}{\oplus} T \subseteq T \underset{˙}{\oplus} U) \to (s \underset{˙}{\oplus} T = T \lor s \underset{˙}{\oplus} T = T \underset{˙}{\oplus} U)))$
56	36 55	mpd	$⊢ (φ \land s \in S \land (T \cap U \subseteq s \land s \subseteq U)) \to ((T \subseteq s \underset{˙}{\oplus} T \land s \underset{˙}{\oplus} T \subseteq T \underset{˙}{\oplus} U) \to (s \underset{˙}{\oplus} T = T \lor s \underset{˙}{\oplus} T = T \underset{˙}{\oplus} U))$
57	21 35 56	mp2and	$⊢ (φ \land s \in S \land (T \cap U \subseteq s \land s \subseteq U)) \to (s \underset{˙}{\oplus} T = T \lor s \underset{˙}{\oplus} T = T \underset{˙}{\oplus} U)$
58		ineq1	$⊢ s \underset{˙}{\oplus} T = T \to (s \underset{˙}{\oplus} T) \cap U = T \cap U$
59		simp3l	$⊢ (φ \land s \in S \land (T \cap U \subseteq s \land s \subseteq U)) \to T \cap U \subseteq s$
60	1 2 3 13 18 22 16 59 24	lcvexchlem2	$⊢ (φ \land s \in S \land (T \cap U \subseteq s \land s \subseteq U)) \to (s \underset{˙}{\oplus} T) \cap U = s$
61	60	eqeq1d	$⊢ (φ \land s \in S \land (T \cap U \subseteq s \land s \subseteq U)) \to ((s \underset{˙}{\oplus} T) \cap U = T \cap U \leftrightarrow s = T \cap U)$
62	58 61	syl5ib	$⊢ (φ \land s \in S \land (T \cap U \subseteq s \land s \subseteq U)) \to (s \underset{˙}{\oplus} T = T \to s = T \cap U)$
63		ineq1	$⊢ s \underset{˙}{\oplus} T = T \underset{˙}{\oplus} U \to (s \underset{˙}{\oplus} T) \cap U = (T \underset{˙}{\oplus} U) \cap U$
64	2	lsmub2	$⊢ (T \in SubGrp (W) \land U \in SubGrp (W)) \to U \subseteq T \underset{˙}{\oplus} U$
65	19 23 64	syl2anc	$⊢ (φ \land s \in S \land (T \cap U \subseteq s \land s \subseteq U)) \to U \subseteq T \underset{˙}{\oplus} U$
66		sseqin2	$⊢ U \subseteq T \underset{˙}{\oplus} U \leftrightarrow (T \underset{˙}{\oplus} U) \cap U = U$
67	65 66	sylib	$⊢ (φ \land s \in S \land (T \cap U \subseteq s \land s \subseteq U)) \to (T \underset{˙}{\oplus} U) \cap U = U$
68	60 67	eqeq12d	$⊢ (φ \land s \in S \land (T \cap U \subseteq s \land s \subseteq U)) \to ((s \underset{˙}{\oplus} T) \cap U = (T \underset{˙}{\oplus} U) \cap U \leftrightarrow s = U)$
69	63 68	syl5ib	$⊢ (φ \land s \in S \land (T \cap U \subseteq s \land s \subseteq U)) \to (s \underset{˙}{\oplus} T = T \underset{˙}{\oplus} U \to s = U)$
70	62 69	orim12d	$⊢ (φ \land s \in S \land (T \cap U \subseteq s \land s \subseteq U)) \to ((s \underset{˙}{\oplus} T = T \lor s \underset{˙}{\oplus} T = T \underset{˙}{\oplus} U) \to (s = T \cap U \lor s = U))$
71	57 70	mpd	$⊢ (φ \land s \in S \land (T \cap U \subseteq s \land s \subseteq U)) \to (s = T \cap U \lor s = U)$
72	71	3exp	$⊢ φ \to (s \in S \to ((T \cap U \subseteq s \land s \subseteq U) \to (s = T \cap U \lor s = U)))$
73	72	ralrimiv	$⊢ φ \to \forall s \in S ((T \cap U \subseteq s \land s \subseteq U) \to (s = T \cap U \lor s = U))$
74	1	lssincl	$⊢ (W \in LMod \land T \in S \land U \in S) \to T \cap U \in S$
75	4 5 6 74	syl3anc	$⊢ φ \to T \cap U \in S$
76	1 3 4 75 6	lcvbr3	$⊢ φ \to ((T \cap U) C U \leftrightarrow (T \cap U \subset U \land \forall s \in S ((T \cap U \subseteq s \land s \subseteq U) \to (s = T \cap U \lor s = U))))$
77	12 73 76	mpbir2and	$⊢ φ \to (T \cap U) C U$

Metamath Proof Explorer

Theorem lcvexchlem4

Proof