Theorem lincresunitlem1

Description: Lemma 1 for properties of a specially modified restriction of a linear combination containing a unit as scalar. (Contributed by AV, 18-May-2019)

	Ref	Expression
Hypotheses	lincresunit.b	|- B = ( Base ` M )
	lincresunit.r	|- R = ( Scalar ` M )
	lincresunit.e	|- E = ( Base ` R )
	lincresunit.u	|- U = ( Unit ` R )
	lincresunit.0	|- .0. = ( 0g ` R )
	lincresunit.z	|- Z = ( 0g ` M )
	lincresunit.n	|- N = ( invg ` R )
	lincresunit.i	|- I = ( invr ` R )
	lincresunit.t	|- .x. = ( .r ` R )
	lincresunit.g	|- G = ( s e. ( S \ { X } ) |-> ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` s ) ) )
Assertion	lincresunitlem1	|- ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) ) -> ( I ` ( N ` ( F ` X ) ) ) e. E )

Proof

Step	Hyp	Ref	Expression
1		lincresunit.b	|- B = ( Base ` M )
2		lincresunit.r	|- R = ( Scalar ` M )
3		lincresunit.e	|- E = ( Base ` R )
4		lincresunit.u	|- U = ( Unit ` R )
5		lincresunit.0	|- .0. = ( 0g ` R )
6		lincresunit.z	|- Z = ( 0g ` M )
7		lincresunit.n	|- N = ( invg ` R )
8		lincresunit.i	|- I = ( invr ` R )
9		lincresunit.t	|- .x. = ( .r ` R )
10		lincresunit.g	|- G = ( s e. ( S \ { X } ) |-> ( ( I ` ( N ` ( F ` X ) ) ) .x. ( F ` s ) ) )
11	2	lmodring	|- ( M e. LMod -> R e. Ring )
12	11	3ad2ant2	|- ( ( S e. ~P B /\ M e. LMod /\ X e. S ) -> R e. Ring )
13	12	adantr	|- ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) ) -> R e. Ring )
14		simpr	|- ( ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) -> ( F ` X ) e. U )
15	4 7	unitnegcl	|- ( ( R e. Ring /\ ( F ` X ) e. U ) -> ( N ` ( F ` X ) ) e. U )
16	12 14 15	syl2an	|- ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) ) -> ( N ` ( F ` X ) ) e. U )
17	4 8 3	ringinvcl	|- ( ( R e. Ring /\ ( N ` ( F ` X ) ) e. U ) -> ( I ` ( N ` ( F ` X ) ) ) e. E )
18	13 16 17	syl2anc	|- ( ( ( S e. ~P B /\ M e. LMod /\ X e. S ) /\ ( F e. ( E ^m S ) /\ ( F ` X ) e. U ) ) -> ( I ` ( N ` ( F ` X ) ) ) e. E )