Metamath Proof Explorer

Theorem lcvexchlem3

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

Ref Expression
Hypotheses lcvexch.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lcvexch.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
lcvexch.c ⊢ 𝐶 = ( ⋖L ‘ 𝑊 )
lcvexch.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
lcvexch.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
lcvexch.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
lcvexch.q ⊢ ( 𝜑 → 𝑅 ∈ 𝑆 )
lcvexch.d ⊢ ( 𝜑 → 𝑇 ⊆ 𝑅 )
lcvexch.e ⊢ ( 𝜑 → 𝑅 ⊆ ( 𝑇 ⊕ 𝑈 ) )
Assertion lcvexchlem3 ( 𝜑 → ( ( 𝑅 ∩ 𝑈 ) ⊕ 𝑇 ) = 𝑅 )

Proof

Step Hyp Ref Expression
1 lcvexch.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
2 lcvexch.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
3 lcvexch.c ⊢ 𝐶 = ( ⋖L ‘ 𝑊 )
4 lcvexch.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
5 lcvexch.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
6 lcvexch.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
7 lcvexch.q ⊢ ( 𝜑 → 𝑅 ∈ 𝑆 )
8 lcvexch.d ⊢ ( 𝜑 → 𝑇 ⊆ 𝑅 )
9 lcvexch.e ⊢ ( 𝜑 → 𝑅 ⊆ ( 𝑇 ⊕ 𝑈 ) )
10 1 lsssssubg ⊢ ( 𝑊 ∈ LMod → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
11 4 10 syl ⊢ ( 𝜑 → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
12 11 7 sseldd ⊢ ( 𝜑 → 𝑅 ∈ ( SubGrp ‘ 𝑊 ) )
13 11 6 sseldd ⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
14 11 5 sseldd ⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝑊 ) )
15 2 lsmmod2 ⊢ ( ( ( 𝑅 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝑊 ) ) ∧ 𝑇 ⊆ 𝑅 ) → ( 𝑅 ∩ ( 𝑈 ⊕ 𝑇 ) ) = ( ( 𝑅 ∩ 𝑈 ) ⊕ 𝑇 ) )
16 12 13 14 8 15 syl31anc ⊢ ( 𝜑 → ( 𝑅 ∩ ( 𝑈 ⊕ 𝑇 ) ) = ( ( 𝑅 ∩ 𝑈 ) ⊕ 𝑇 ) )
17 lmodabl ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
18 4 17 syl ⊢ ( 𝜑 → 𝑊 ∈ Abel )
19 2 lsmcom ⊢ ( ( 𝑊 ∈ Abel ∧ 𝑇 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ) → ( 𝑇 ⊕ 𝑈 ) = ( 𝑈 ⊕ 𝑇 ) )
20 18 14 13 19 syl3anc ⊢ ( 𝜑 → ( 𝑇 ⊕ 𝑈 ) = ( 𝑈 ⊕ 𝑇 ) )
21 9 20 sseqtrd ⊢ ( 𝜑 → 𝑅 ⊆ ( 𝑈 ⊕ 𝑇 ) )
22 dfss2 ⊢ ( 𝑅 ⊆ ( 𝑈 ⊕ 𝑇 ) ↔ ( 𝑅 ∩ ( 𝑈 ⊕ 𝑇 ) ) = 𝑅 )
23 21 22 sylib ⊢ ( 𝜑 → ( 𝑅 ∩ ( 𝑈 ⊕ 𝑇 ) ) = 𝑅 )
24 16 23 eqtr3d ⊢ ( 𝜑 → ( ( 𝑅 ∩ 𝑈 ) ⊕ 𝑇 ) = 𝑅 )