Theorem lcvexchlem1

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

	Ref	Expression
Hypotheses	lcvexch.s	|- S = ( LSubSp ` W )
	lcvexch.p	|- .(+) = ( LSSum ` W )
	lcvexch.c	|- C = (
	lcvexch.w	|- ( ph -> W e. LMod )
	lcvexch.t	|- ( ph -> T e. S )
	lcvexch.u	|- ( ph -> U e. S )
Assertion	lcvexchlem1	|- ( ph -> ( T C. ( T .(+) U ) <-> ( T i^i U ) C. U ) )

Proof

Step	Hyp	Ref	Expression
1		lcvexch.s	|- S = ( LSubSp ` W )
2		lcvexch.p	|- .(+) = ( LSSum ` W )
3		lcvexch.c	|- C = (
4		lcvexch.w	|- ( ph -> W e. LMod )
5		lcvexch.t	|- ( ph -> T e. S )
6		lcvexch.u	|- ( ph -> U e. S )
7	1	lsssssubg	|- ( W e. LMod -> S C_ ( SubGrp ` W ) )
8	4 7	syl	|- ( ph -> S C_ ( SubGrp ` W ) )
9	8 5	sseldd	|- ( ph -> T e. ( SubGrp ` W ) )
10	8 6	sseldd	|- ( ph -> U e. ( SubGrp ` W ) )
11	2	lsmub1	|- ( ( T e. ( SubGrp ` W ) /\ U e. ( SubGrp ` W ) ) -> T C_ ( T .(+) U ) )
12	9 10 11	syl2anc	|- ( ph -> T C_ ( T .(+) U ) )
13		inss2	|- ( T i^i U ) C_ U
14	13	a1i	|- ( ph -> ( T i^i U ) C_ U )
15	12 14	2thd	|- ( ph -> ( T C_ ( T .(+) U ) <-> ( T i^i U ) C_ U ) )
16	2	lsmss2b	|- ( ( T e. ( SubGrp ` W ) /\ U e. ( SubGrp ` W ) ) -> ( U C_ T <-> ( T .(+) U ) = T ) )
17	9 10 16	syl2anc	|- ( ph -> ( U C_ T <-> ( T .(+) U ) = T ) )
18		eqcom	|- ( ( T .(+) U ) = T <-> T = ( T .(+) U ) )
19	17 18	bitrdi	|- ( ph -> ( U C_ T <-> T = ( T .(+) U ) ) )
20		sseqin2	|- ( U C_ T <-> ( T i^i U ) = U )
21	19 20	bitr3di	|- ( ph -> ( T = ( T .(+) U ) <-> ( T i^i U ) = U ) )
22	21	necon3bid	|- ( ph -> ( T =/= ( T .(+) U ) <-> ( T i^i U ) =/= U ) )
23	15 22	anbi12d	|- ( ph -> ( ( T C_ ( T .(+) U ) /\ T =/= ( T .(+) U ) ) <-> ( ( T i^i U ) C_ U /\ ( T i^i U ) =/= U ) ) )
24		df-pss	|- ( T C. ( T .(+) U ) <-> ( T C_ ( T .(+) U ) /\ T =/= ( T .(+) U ) ) )
25		df-pss	|- ( ( T i^i U ) C. U <-> ( ( T i^i U ) C_ U /\ ( T i^i U ) =/= U ) )
26	23 24 25	3bitr4g	|- ( ph -> ( T C. ( T .(+) U ) <-> ( T i^i U ) C. U ) )