This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lcvexchlem3

Description: Lemma for lcvexch . (Contributed by NM, 10-Jan-2015)

Ref Expression
Hypotheses lcvexch.s ⊢ S = LSubSp ⁡ W
lcvexch.p ⊢ ⊕ ˙ = LSSum ⁡ W
lcvexch.c ⊢ C = ⋖ L ⁡ W
lcvexch.w ⊢ φ → W ∈ LMod
lcvexch.t ⊢ φ → T ∈ S
lcvexch.u ⊢ φ → U ∈ S
lcvexch.q ⊢ φ → R ∈ S
lcvexch.d ⊢ φ → T ⊆ R
lcvexch.e ⊢ φ → R ⊆ T ⊕ ˙ U
Assertion lcvexchlem3 ⊢ φ → R ∩ U ⊕ ˙ T = R

Proof

Step Hyp Ref Expression
1 lcvexch.s ⊢ S = LSubSp ⁡ W
2 lcvexch.p ⊢ ⊕ ˙ = LSSum ⁡ W
3 lcvexch.c ⊢ C = ⋖ L ⁡ W
4 lcvexch.w ⊢ φ → W ∈ LMod
5 lcvexch.t ⊢ φ → T ∈ S
6 lcvexch.u ⊢ φ → U ∈ S
7 lcvexch.q ⊢ φ → R ∈ S
8 lcvexch.d ⊢ φ → T ⊆ R
9 lcvexch.e ⊢ φ → R ⊆ T ⊕ ˙ U
10 1 lsssssubg ⊢ W ∈ LMod → S ⊆ SubGrp ⁡ W
11 4 10 syl ⊢ φ → S ⊆ SubGrp ⁡ W
12 11 7 sseldd ⊢ φ → R ∈ SubGrp ⁡ W
13 11 6 sseldd ⊢ φ → U ∈ SubGrp ⁡ W
14 11 5 sseldd ⊢ φ → T ∈ SubGrp ⁡ W
15 2 lsmmod2 ⊢ R ∈ SubGrp ⁡ W ∧ U ∈ SubGrp ⁡ W ∧ T ∈ SubGrp ⁡ W ∧ T ⊆ R → R ∩ U ⊕ ˙ T = R ∩ U ⊕ ˙ T
16 12 13 14 8 15 syl31anc ⊢ φ → R ∩ U ⊕ ˙ T = R ∩ U ⊕ ˙ T
17 lmodabl ⊢ W ∈ LMod → W ∈ Abel
18 4 17 syl ⊢ φ → W ∈ Abel
19 2 lsmcom ⊢ W ∈ Abel ∧ T ∈ SubGrp ⁡ W ∧ U ∈ SubGrp ⁡ W → T ⊕ ˙ U = U ⊕ ˙ T
20 18 14 13 19 syl3anc ⊢ φ → T ⊕ ˙ U = U ⊕ ˙ T
21 9 20 sseqtrd ⊢ φ → R ⊆ U ⊕ ˙ T
22 dfss2 ⊢ R ⊆ U ⊕ ˙ T ↔ R ∩ U ⊕ ˙ T = R
23 21 22 sylib ⊢ φ → R ∩ U ⊕ ˙ T = R
24 16 23 eqtr3d ⊢ φ → R ∩ U ⊕ ˙ T = R