Metamath Proof Explorer

Theorem lcvexchlem2

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.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑆 )
lcvexch.a ⊢ ( 𝜑 → ( 𝑇 ∩ 𝑈 ) ⊆ 𝑅 )
lcvexch.b ⊢ ( 𝜑 → 𝑅 ⊆ 𝑈 )
Assertion lcvexchlem2 ( 𝜑 → ( ( 𝑅 ⊕ 𝑇 ) ∩ 𝑈 ) = 𝑅 )

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.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑆 )
8 lcvexch.a ⊢ ( 𝜑 → ( 𝑇 ∩ 𝑈 ) ⊆ 𝑅 )
9 lcvexch.b ⊢ ( 𝜑 → 𝑅 ⊆ 𝑈 )
10 1 lsssssubg ⊢ ( 𝑊 ∈ LMod → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
11 4 10 syl ⊢ ( 𝜑 → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
12 11 7 sseldd ⊢ ( 𝜑 → 𝑅 ∈ ( SubGrp ‘ 𝑊 ) )
13 11 5 sseldd ⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝑊 ) )
14 11 6 sseldd ⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
15 2 lsmmod ⊢ ( ( ( 𝑅 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ) ∧ 𝑅 ⊆ 𝑈 ) → ( 𝑅 ⊕ ( 𝑇 ∩ 𝑈 ) ) = ( ( 𝑅 ⊕ 𝑇 ) ∩ 𝑈 ) )
16 12 13 14 9 15 syl31anc ⊢ ( 𝜑 → ( 𝑅 ⊕ ( 𝑇 ∩ 𝑈 ) ) = ( ( 𝑅 ⊕ 𝑇 ) ∩ 𝑈 ) )
17 1 lssincl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → ( 𝑇 ∩ 𝑈 ) ∈ 𝑆 )
18 4 5 6 17 syl3anc ⊢ ( 𝜑 → ( 𝑇 ∩ 𝑈 ) ∈ 𝑆 )
19 11 18 sseldd ⊢ ( 𝜑 → ( 𝑇 ∩ 𝑈 ) ∈ ( SubGrp ‘ 𝑊 ) )
20 2 lsmss2 ⊢ ( ( 𝑅 ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑇 ∩ 𝑈 ) ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑇 ∩ 𝑈 ) ⊆ 𝑅 ) → ( 𝑅 ⊕ ( 𝑇 ∩ 𝑈 ) ) = 𝑅 )
21 12 19 8 20 syl3anc ⊢ ( 𝜑 → ( 𝑅 ⊕ ( 𝑇 ∩ 𝑈 ) ) = 𝑅 )
22 16 21 eqtr3d ⊢ ( 𝜑 → ( ( 𝑅 ⊕ 𝑇 ) ∩ 𝑈 ) = 𝑅 )