lcvexchlem3

	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.q	$⊢ φ \to R \in S$
	lcvexch.d	$⊢ φ \to T \subseteq R$
	lcvexch.e	$⊢ φ \to R \subseteq T \underset{˙}{\oplus} U$
Assertion	lcvexchlem3	$⊢ φ \to (R \cap U) \underset{˙}{\oplus} T = R$

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.q	$⊢ φ \to R \in S$
8		lcvexch.d	$⊢ φ \to T \subseteq R$
9		lcvexch.e	$⊢ φ \to R \subseteq T \underset{˙}{\oplus} U$
10	1	lsssssubg	$⊢ W \in LMod \to S \subseteq SubGrp (W)$
11	4 10	syl	$⊢ φ \to S \subseteq SubGrp (W)$
12	11 7	sseldd	$⊢ φ \to R \in SubGrp (W)$
13	11 6	sseldd	$⊢ φ \to U \in SubGrp (W)$
14	11 5	sseldd	$⊢ φ \to T \in SubGrp (W)$
15	2	lsmmod2	$⊢ ((R \in SubGrp (W) \land U \in SubGrp (W) \land T \in SubGrp (W)) \land T \subseteq R) \to R \cap (U \underset{˙}{\oplus} T) = (R \cap U) \underset{˙}{\oplus} T$
16	12 13 14 8 15	syl31anc	$⊢ φ \to R \cap (U \underset{˙}{\oplus} T) = (R \cap U) \underset{˙}{\oplus} T$
17		lmodabl	$⊢ W \in LMod \to W \in Abel$
18	4 17	syl	$⊢ φ \to W \in Abel$
19	2	lsmcom	$⊢ (W \in Abel \land T \in SubGrp (W) \land U \in SubGrp (W)) \to T \underset{˙}{\oplus} U = U \underset{˙}{\oplus} T$
20	18 14 13 19	syl3anc	$⊢ φ \to T \underset{˙}{\oplus} U = U \underset{˙}{\oplus} T$
21	9 20	sseqtrd	$⊢ φ \to R \subseteq U \underset{˙}{\oplus} T$
22		df-ss	$⊢ R \subseteq U \underset{˙}{\oplus} T \leftrightarrow R \cap (U \underset{˙}{\oplus} T) = R$
23	21 22	sylib	$⊢ φ \to R \cap (U \underset{˙}{\oplus} T) = R$
24	16 23	eqtr3d	$⊢ φ \to (R \cap U) \underset{˙}{\oplus} T = R$

Metamath Proof Explorer