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 df-ss ( 𝑅 ⊆ ( 𝑈 𝑇 ) ↔ ( 𝑅 ∩ ( 𝑈 𝑇 ) ) = 𝑅 )
23 21 22 sylib ( 𝜑 → ( 𝑅 ∩ ( 𝑈 𝑇 ) ) = 𝑅 )
24 16 23 eqtr3d ( 𝜑 → ( ( 𝑅𝑈 ) 𝑇 ) = 𝑅 )