Metamath Proof Explorer


Theorem lcvexchlem1

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 ( 𝜑𝑈𝑆 )
Assertion lcvexchlem1 ( 𝜑 → ( 𝑇 ⊊ ( 𝑇 𝑈 ) ↔ ( 𝑇𝑈 ) ⊊ 𝑈 ) )

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 1 lsssssubg ( 𝑊 ∈ LMod → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
8 4 7 syl ( 𝜑𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
9 8 5 sseldd ( 𝜑𝑇 ∈ ( SubGrp ‘ 𝑊 ) )
10 8 6 sseldd ( 𝜑𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
11 2 lsmub1 ( ( 𝑇 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ) → 𝑇 ⊆ ( 𝑇 𝑈 ) )
12 9 10 11 syl2anc ( 𝜑𝑇 ⊆ ( 𝑇 𝑈 ) )
13 inss2 ( 𝑇𝑈 ) ⊆ 𝑈
14 13 a1i ( 𝜑 → ( 𝑇𝑈 ) ⊆ 𝑈 )
15 12 14 2thd ( 𝜑 → ( 𝑇 ⊆ ( 𝑇 𝑈 ) ↔ ( 𝑇𝑈 ) ⊆ 𝑈 ) )
16 2 lsmss2b ( ( 𝑇 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ) → ( 𝑈𝑇 ↔ ( 𝑇 𝑈 ) = 𝑇 ) )
17 9 10 16 syl2anc ( 𝜑 → ( 𝑈𝑇 ↔ ( 𝑇 𝑈 ) = 𝑇 ) )
18 eqcom ( ( 𝑇 𝑈 ) = 𝑇𝑇 = ( 𝑇 𝑈 ) )
19 17 18 bitrdi ( 𝜑 → ( 𝑈𝑇𝑇 = ( 𝑇 𝑈 ) ) )
20 sseqin2 ( 𝑈𝑇 ↔ ( 𝑇𝑈 ) = 𝑈 )
21 19 20 bitr3di ( 𝜑 → ( 𝑇 = ( 𝑇 𝑈 ) ↔ ( 𝑇𝑈 ) = 𝑈 ) )
22 21 necon3bid ( 𝜑 → ( 𝑇 ≠ ( 𝑇 𝑈 ) ↔ ( 𝑇𝑈 ) ≠ 𝑈 ) )
23 15 22 anbi12d ( 𝜑 → ( ( 𝑇 ⊆ ( 𝑇 𝑈 ) ∧ 𝑇 ≠ ( 𝑇 𝑈 ) ) ↔ ( ( 𝑇𝑈 ) ⊆ 𝑈 ∧ ( 𝑇𝑈 ) ≠ 𝑈 ) ) )
24 df-pss ( 𝑇 ⊊ ( 𝑇 𝑈 ) ↔ ( 𝑇 ⊆ ( 𝑇 𝑈 ) ∧ 𝑇 ≠ ( 𝑇 𝑈 ) ) )
25 df-pss ( ( 𝑇𝑈 ) ⊊ 𝑈 ↔ ( ( 𝑇𝑈 ) ⊆ 𝑈 ∧ ( 𝑇𝑈 ) ≠ 𝑈 ) )
26 23 24 25 3bitr4g ( 𝜑 → ( 𝑇 ⊊ ( 𝑇 𝑈 ) ↔ ( 𝑇𝑈 ) ⊊ 𝑈 ) )