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 ⊢ ( 𝜑 → ( 𝑇 ⊊ ( 𝑇 ⊕ 𝑈 ) ↔ ( 𝑇 ∩ 𝑈 ) ⊊ 𝑈 ) )