Theorem lcvexchlem3

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.q	|- ( ph -> R e. S )
	lcvexch.d	|- ( ph -> T C_ R )
	lcvexch.e	|- ( ph -> R C_ ( T .(+) U ) )
Assertion	lcvexchlem3	|- ( ph -> ( ( R i^i U ) .(+) T ) = 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.q	|- ( ph -> R e. S )
8		lcvexch.d	|- ( ph -> T C_ R )
9		lcvexch.e	|- ( ph -> R C_ ( T .(+) 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 6	sseldd	|- ( ph -> U e. ( SubGrp ` W ) )
14	11 5	sseldd	|- ( ph -> T e. ( SubGrp ` W ) )
15	2	lsmmod2	|- ( ( ( R e. ( SubGrp ` W ) /\ U e. ( SubGrp ` W ) /\ T e. ( SubGrp ` W ) ) /\ T C_ R ) -> ( R i^i ( U .(+) T ) ) = ( ( R i^i U ) .(+) T ) )
16	12 13 14 8 15	syl31anc	|- ( ph -> ( R i^i ( U .(+) T ) ) = ( ( R i^i U ) .(+) T ) )
17		lmodabl	|- ( W e. LMod -> W e. Abel )
18	4 17	syl	|- ( ph -> W e. Abel )
19	2	lsmcom	|- ( ( W e. Abel /\ T e. ( SubGrp ` W ) /\ U e. ( SubGrp ` W ) ) -> ( T .(+) U ) = ( U .(+) T ) )
20	18 14 13 19	syl3anc	|- ( ph -> ( T .(+) U ) = ( U .(+) T ) )
21	9 20	sseqtrd	|- ( ph -> R C_ ( U .(+) T ) )
22		df-ss	|- ( R C_ ( U .(+) T ) <-> ( R i^i ( U .(+) T ) ) = R )
23	21 22	sylib	|- ( ph -> ( R i^i ( U .(+) T ) ) = R )
24	16 23	eqtr3d	|- ( ph -> ( ( R i^i U ) .(+) T ) = R )