lcvexchlem2

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.r	$⊢ φ \to R \in S$
8		lcvexch.a	$⊢ φ \to T \cap U \subseteq R$
9		lcvexch.b	$⊢ φ \to R \subseteq 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 5	sseldd	$⊢ φ \to T \in SubGrp (W)$
14	11 6	sseldd	$⊢ φ \to U \in SubGrp (W)$
15	2	lsmmod	$⊢ ((R \in SubGrp (W) \land T \in SubGrp (W) \land U \in SubGrp (W)) \land R \subseteq U) \to R \underset{˙}{\oplus} (T \cap U) = (R \underset{˙}{\oplus} T) \cap U$
16	12 13 14 9 15	syl31anc	$⊢ φ \to R \underset{˙}{\oplus} (T \cap U) = (R \underset{˙}{\oplus} T) \cap U$
17	1	lssincl	$⊢ (W \in LMod \land T \in S \land U \in S) \to T \cap U \in S$
18	4 5 6 17	syl3anc	$⊢ φ \to T \cap U \in S$
19	11 18	sseldd	$⊢ φ \to T \cap U \in SubGrp (W)$
20	2	lsmss2	$⊢ (R \in SubGrp (W) \land T \cap U \in SubGrp (W) \land T \cap U \subseteq R) \to R \underset{˙}{\oplus} (T \cap U) = R$
21	12 19 8 20	syl3anc	$⊢ φ \to R \underset{˙}{\oplus} (T \cap U) = R$
22	16 21	eqtr3d	$⊢ φ \to (R \underset{˙}{\oplus} T) \cap U = R$

Metamath Proof Explorer