Theorem lcvexchlem2

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 )
	lcvexch.r	|- ( ph -> R e. S )
	lcvexch.a	|- ( ph -> ( T i^i U ) C_ R )
	lcvexch.b	|- ( ph -> R C_ U )
Assertion	lcvexchlem2	|- ( ph -> ( ( R .(+) T ) i^i U ) = R )

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		lcvexch.r	|- ( ph -> R e. S )
8		lcvexch.a	|- ( ph -> ( T i^i U ) C_ R )
9		lcvexch.b	|- ( ph -> R C_ U )
10	1	lsssssubg	|- ( W e. LMod -> S C_ ( SubGrp ` W ) )
11	4 10	syl	|- ( ph -> S C_ ( SubGrp ` W ) )
12	11 7	sseldd	|- ( ph -> R e. ( SubGrp ` W ) )
13	11 5	sseldd	|- ( ph -> T e. ( SubGrp ` W ) )
14	11 6	sseldd	|- ( ph -> U e. ( SubGrp ` W ) )
15	2	lsmmod	|- ( ( ( R e. ( SubGrp ` W ) /\ T e. ( SubGrp ` W ) /\ U e. ( SubGrp ` W ) ) /\ R C_ U ) -> ( R .(+) ( T i^i U ) ) = ( ( R .(+) T ) i^i U ) )
16	12 13 14 9 15	syl31anc	|- ( ph -> ( R .(+) ( T i^i U ) ) = ( ( R .(+) T ) i^i U ) )
17	1	lssincl	|- ( ( W e. LMod /\ T e. S /\ U e. S ) -> ( T i^i U ) e. S )
18	4 5 6 17	syl3anc	|- ( ph -> ( T i^i U ) e. S )
19	11 18	sseldd	|- ( ph -> ( T i^i U ) e. ( SubGrp ` W ) )
20	2	lsmss2	|- ( ( R e. ( SubGrp ` W ) /\ ( T i^i U ) e. ( SubGrp ` W ) /\ ( T i^i U ) C_ R ) -> ( R .(+) ( T i^i U ) ) = R )
21	12 19 8 20	syl3anc	|- ( ph -> ( R .(+) ( T i^i U ) ) = R )
22	16 21	eqtr3d	|- ( ph -> ( ( R .(+) T ) i^i U ) = R )