frlmssuvc2

Description: A nonzero scalar multiple of a unit vector not included in a support-restriction subspace is not included in the subspace. (Contributed by Stefan O'Rear, 5-Feb-2015) (Revised by AV, 24-Jun-2019)

	Ref	Expression
Hypotheses	frlmssuvc1.f	\|- F = ( R freeLMod I )
	frlmssuvc1.u	\|- U = ( R unitVec I )
	frlmssuvc1.b	\|- B = ( Base ` F )
	frlmssuvc1.k	\|- K = ( Base ` R )
	frlmssuvc1.t	\|- .x. = ( .s ` F )
	frlmssuvc1.z	\|- .0. = ( 0g ` R )
	frlmssuvc1.c	\|- C = { x e. B \| ( x supp .0. ) C_ J }
	frlmssuvc1.r	\|- ( ph -> R e. Ring )
	frlmssuvc1.i	\|- ( ph -> I e. V )
	frlmssuvc1.j	\|- ( ph -> J C_ I )
	frlmssuvc2.l	\|- ( ph -> L e. ( I \ J ) )
	frlmssuvc2.x	\|- ( ph -> X e. ( K \ { .0. } ) )
Assertion	frlmssuvc2	\|- ( ph -> -. ( X .x. ( U ` L ) ) e. C )

Proof

Step	Hyp	Ref	Expression
1		frlmssuvc1.f	\|- F = ( R freeLMod I )
2		frlmssuvc1.u	\|- U = ( R unitVec I )
3		frlmssuvc1.b	\|- B = ( Base ` F )
4		frlmssuvc1.k	\|- K = ( Base ` R )
5		frlmssuvc1.t	\|- .x. = ( .s ` F )
6		frlmssuvc1.z	\|- .0. = ( 0g ` R )
7		frlmssuvc1.c	\|- C = { x e. B \| ( x supp .0. ) C_ J }
8		frlmssuvc1.r	\|- ( ph -> R e. Ring )
9		frlmssuvc1.i	\|- ( ph -> I e. V )
10		frlmssuvc1.j	\|- ( ph -> J C_ I )
11		frlmssuvc2.l	\|- ( ph -> L e. ( I \ J ) )
12		frlmssuvc2.x	\|- ( ph -> X e. ( K \ { .0. } ) )
13		fveq2	\|- ( x = L -> ( ( X .x. ( U ` L ) ) ` x ) = ( ( X .x. ( U ` L ) ) ` L ) )
14	13	neeq1d	\|- ( x = L -> ( ( ( X .x. ( U ` L ) ) ` x ) =/= .0. <-> ( ( X .x. ( U ` L ) ) ` L ) =/= .0. ) )
15	11	eldifad	\|- ( ph -> L e. I )
16	12	eldifad	\|- ( ph -> X e. K )
17	2 1 3	uvcff	\|- ( ( R e. Ring /\ I e. V ) -> U : I --> B )
18	8 9 17	syl2anc	\|- ( ph -> U : I --> B )
19	18 15	ffvelcdmd	\|- ( ph -> ( U ` L ) e. B )
20		eqid	\|- ( .r ` R ) = ( .r ` R )
21	1 3 4 9 16 19 15 5 20	frlmvscaval	\|- ( ph -> ( ( X .x. ( U ` L ) ) ` L ) = ( X ( .r ` R ) ( ( U ` L ) ` L ) ) )
22		eqid	\|- ( 1r ` R ) = ( 1r ` R )
23	2 8 9 15 22	uvcvv1	\|- ( ph -> ( ( U ` L ) ` L ) = ( 1r ` R ) )
24	23	oveq2d	\|- ( ph -> ( X ( .r ` R ) ( ( U ` L ) ` L ) ) = ( X ( .r ` R ) ( 1r ` R ) ) )
25	4 20 22	ringridm	\|- ( ( R e. Ring /\ X e. K ) -> ( X ( .r ` R ) ( 1r ` R ) ) = X )
26	8 16 25	syl2anc	\|- ( ph -> ( X ( .r ` R ) ( 1r ` R ) ) = X )
27	21 24 26	3eqtrd	\|- ( ph -> ( ( X .x. ( U ` L ) ) ` L ) = X )
28		eldifsni	\|- ( X e. ( K \ { .0. } ) -> X =/= .0. )
29	12 28	syl	\|- ( ph -> X =/= .0. )
30	27 29	eqnetrd	\|- ( ph -> ( ( X .x. ( U ` L ) ) ` L ) =/= .0. )
31	14 15 30	elrabd	\|- ( ph -> L e. { x e. I \| ( ( X .x. ( U ` L ) ) ` x ) =/= .0. } )
32	11	eldifbd	\|- ( ph -> -. L e. J )
33		nelss	\|- ( ( L e. { x e. I \| ( ( X .x. ( U ` L ) ) ` x ) =/= .0. } /\ -. L e. J ) -> -. { x e. I \| ( ( X .x. ( U ` L ) ) ` x ) =/= .0. } C_ J )
34	31 32 33	syl2anc	\|- ( ph -> -. { x e. I \| ( ( X .x. ( U ` L ) ) ` x ) =/= .0. } C_ J )
35	1	frlmlmod	\|- ( ( R e. Ring /\ I e. V ) -> F e. LMod )
36	8 9 35	syl2anc	\|- ( ph -> F e. LMod )
37	1	frlmsca	\|- ( ( R e. Ring /\ I e. V ) -> R = ( Scalar ` F ) )
38	8 9 37	syl2anc	\|- ( ph -> R = ( Scalar ` F ) )
39	38	fveq2d	\|- ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` F ) ) )
40	4 39	eqtrid	\|- ( ph -> K = ( Base ` ( Scalar ` F ) ) )
41	16 40	eleqtrd	\|- ( ph -> X e. ( Base ` ( Scalar ` F ) ) )
42		eqid	\|- ( Scalar ` F ) = ( Scalar ` F )
43		eqid	\|- ( Base ` ( Scalar ` F ) ) = ( Base ` ( Scalar ` F ) )
44	3 42 5 43	lmodvscl	\|- ( ( F e. LMod /\ X e. ( Base ` ( Scalar ` F ) ) /\ ( U ` L ) e. B ) -> ( X .x. ( U ` L ) ) e. B )
45	36 41 19 44	syl3anc	\|- ( ph -> ( X .x. ( U ` L ) ) e. B )
46	1 4 3	frlmbasf	\|- ( ( I e. V /\ ( X .x. ( U ` L ) ) e. B ) -> ( X .x. ( U ` L ) ) : I --> K )
47	9 45 46	syl2anc	\|- ( ph -> ( X .x. ( U ` L ) ) : I --> K )
48	47	ffnd	\|- ( ph -> ( X .x. ( U ` L ) ) Fn I )
49	6	fvexi	\|- .0. e. _V
50	49	a1i	\|- ( ph -> .0. e. _V )
51		suppvalfn	\|- ( ( ( X .x. ( U ` L ) ) Fn I /\ I e. V /\ .0. e. _V ) -> ( ( X .x. ( U ` L ) ) supp .0. ) = { x e. I \| ( ( X .x. ( U ` L ) ) ` x ) =/= .0. } )
52	48 9 50 51	syl3anc	\|- ( ph -> ( ( X .x. ( U ` L ) ) supp .0. ) = { x e. I \| ( ( X .x. ( U ` L ) ) ` x ) =/= .0. } )
53	52	sseq1d	\|- ( ph -> ( ( ( X .x. ( U ` L ) ) supp .0. ) C_ J <-> { x e. I \| ( ( X .x. ( U ` L ) ) ` x ) =/= .0. } C_ J ) )
54	34 53	mtbird	\|- ( ph -> -. ( ( X .x. ( U ` L ) ) supp .0. ) C_ J )
55	54	intnand	\|- ( ph -> -. ( ( X .x. ( U ` L ) ) e. B /\ ( ( X .x. ( U ` L ) ) supp .0. ) C_ J ) )
56		oveq1	\|- ( x = ( X .x. ( U ` L ) ) -> ( x supp .0. ) = ( ( X .x. ( U ` L ) ) supp .0. ) )
57	56	sseq1d	\|- ( x = ( X .x. ( U ` L ) ) -> ( ( x supp .0. ) C_ J <-> ( ( X .x. ( U ` L ) ) supp .0. ) C_ J ) )
58	57 7	elrab2	\|- ( ( X .x. ( U ` L ) ) e. C <-> ( ( X .x. ( U ` L ) ) e. B /\ ( ( X .x. ( U ` L ) ) supp .0. ) C_ J ) )
59	55 58	sylnibr	\|- ( ph -> -. ( X .x. ( U ` L ) ) e. C )

Metamath Proof Explorer

Theorem frlmssuvc2

Proof