# Metamath Proof Explorer

## Theorem lcvexchlem1

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

Ref Expression
Hypotheses lcvexch.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
lcvexch.p
lcvexch.c ${⊢}{C}={⋖}_{L}\left({W}\right)$
lcvexch.w ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
lcvexch.t ${⊢}{\phi }\to {T}\in {S}$
lcvexch.u ${⊢}{\phi }\to {U}\in {S}$
Assertion lcvexchlem1

### Proof

Step Hyp Ref Expression
1 lcvexch.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
2 lcvexch.p
3 lcvexch.c ${⊢}{C}={⋖}_{L}\left({W}\right)$
4 lcvexch.w ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
5 lcvexch.t ${⊢}{\phi }\to {T}\in {S}$
6 lcvexch.u ${⊢}{\phi }\to {U}\in {S}$
7 1 lsssssubg ${⊢}{W}\in \mathrm{LMod}\to {S}\subseteq \mathrm{SubGrp}\left({W}\right)$
8 4 7 syl ${⊢}{\phi }\to {S}\subseteq \mathrm{SubGrp}\left({W}\right)$
9 8 5 sseldd ${⊢}{\phi }\to {T}\in \mathrm{SubGrp}\left({W}\right)$
10 8 6 sseldd ${⊢}{\phi }\to {U}\in \mathrm{SubGrp}\left({W}\right)$
11 2 lsmub1
12 9 10 11 syl2anc
13 inss2 ${⊢}{T}\cap {U}\subseteq {U}$
14 13 a1i ${⊢}{\phi }\to {T}\cap {U}\subseteq {U}$
15 12 14 2thd
16 sseqin2 ${⊢}{U}\subseteq {T}↔{T}\cap {U}={U}$
17 2 lsmss2b
18 9 10 17 syl2anc
19 eqcom
20 18 19 syl6bb
21 16 20 syl5rbbr
22 21 necon3bid
23 15 22 anbi12d
24 df-pss
25 df-pss ${⊢}{T}\cap {U}\subset {U}↔\left({T}\cap {U}\subseteq {U}\wedge {T}\cap {U}\ne {U}\right)$
26 23 24 25 3bitr4g