Theorem clmneg

Description: Negation in the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypotheses	clm0.f	|- F = ( Scalar ` W )
	clmsub.k	|- K = ( Base ` F )
Assertion	clmneg	|- ( ( W e. CMod /\ A e. K ) -> -u A = ( ( invg ` F ) ` A ) )

Proof

Step	Hyp	Ref	Expression
1		clm0.f	|- F = ( Scalar ` W )
2		clmsub.k	|- K = ( Base ` F )
3	1 2	clmsca	|- ( W e. CMod -> F = ( CCfld |`s K ) )
4	3	fveq2d	|- ( W e. CMod -> ( invg ` F ) = ( invg ` ( CCfld |`s K ) ) )
5	4	adantr	|- ( ( W e. CMod /\ A e. K ) -> ( invg ` F ) = ( invg ` ( CCfld |`s K ) ) )
6	5	fveq1d	|- ( ( W e. CMod /\ A e. K ) -> ( ( invg ` F ) ` A ) = ( ( invg ` ( CCfld |`s K ) ) ` A ) )
7	1 2	clmsubrg	|- ( W e. CMod -> K e. ( SubRing ` CCfld ) )
8		subrgsubg	|- ( K e. ( SubRing ` CCfld ) -> K e. ( SubGrp ` CCfld ) )
9	7 8	syl	|- ( W e. CMod -> K e. ( SubGrp ` CCfld ) )
10		eqid	|- ( CCfld |`s K ) = ( CCfld |`s K )
11		eqid	|- ( invg ` CCfld ) = ( invg ` CCfld )
12		eqid	|- ( invg ` ( CCfld |`s K ) ) = ( invg ` ( CCfld |`s K ) )
13	10 11 12	subginv	|- ( ( K e. ( SubGrp ` CCfld ) /\ A e. K ) -> ( ( invg ` CCfld ) ` A ) = ( ( invg ` ( CCfld |`s K ) ) ` A ) )
14	9 13	sylan	|- ( ( W e. CMod /\ A e. K ) -> ( ( invg ` CCfld ) ` A ) = ( ( invg ` ( CCfld |`s K ) ) ` A ) )
15	1 2	clmsscn	|- ( W e. CMod -> K C_ CC )
16	15	sselda	|- ( ( W e. CMod /\ A e. K ) -> A e. CC )
17		cnfldneg	|- ( A e. CC -> ( ( invg ` CCfld ) ` A ) = -u A )
18	16 17	syl	|- ( ( W e. CMod /\ A e. K ) -> ( ( invg ` CCfld ) ` A ) = -u A )
19	6 14 18	3eqtr2rd	|- ( ( W e. CMod /\ A e. K ) -> -u A = ( ( invg ` F ) ` A ) )