frlmup2

Description: The evaluation map has the intended behavior on the unit vectors. (Contributed by Stefan O'Rear, 7-Feb-2015) (Proof shortened by AV, 21-Jul-2019)

	Ref	Expression
Hypotheses	frlmup.f	\|- F = ( R freeLMod I )
	frlmup.b	\|- B = ( Base ` F )
	frlmup.c	\|- C = ( Base ` T )
	frlmup.v	\|- .x. = ( .s ` T )
	frlmup.e	\|- E = ( x e. B \|-> ( T gsum ( x oF .x. A ) ) )
	frlmup.t	\|- ( ph -> T e. LMod )
	frlmup.i	\|- ( ph -> I e. X )
	frlmup.r	\|- ( ph -> R = ( Scalar ` T ) )
	frlmup.a	\|- ( ph -> A : I --> C )
	frlmup.y	\|- ( ph -> Y e. I )
	frlmup.u	\|- U = ( R unitVec I )
Assertion	frlmup2	\|- ( ph -> ( E ` ( U ` Y ) ) = ( A ` Y ) )

Proof

Step	Hyp	Ref	Expression
1		frlmup.f	\|- F = ( R freeLMod I )
2		frlmup.b	\|- B = ( Base ` F )
3		frlmup.c	\|- C = ( Base ` T )
4		frlmup.v	\|- .x. = ( .s ` T )
5		frlmup.e	\|- E = ( x e. B \|-> ( T gsum ( x oF .x. A ) ) )
6		frlmup.t	\|- ( ph -> T e. LMod )
7		frlmup.i	\|- ( ph -> I e. X )
8		frlmup.r	\|- ( ph -> R = ( Scalar ` T ) )
9		frlmup.a	\|- ( ph -> A : I --> C )
10		frlmup.y	\|- ( ph -> Y e. I )
11		frlmup.u	\|- U = ( R unitVec I )
12		eqid	\|- ( Scalar ` T ) = ( Scalar ` T )
13	12	lmodring	\|- ( T e. LMod -> ( Scalar ` T ) e. Ring )
14	6 13	syl	\|- ( ph -> ( Scalar ` T ) e. Ring )
15	8 14	eqeltrd	\|- ( ph -> R e. Ring )
16	11 1 2	uvcff	\|- ( ( R e. Ring /\ I e. X ) -> U : I --> B )
17	15 7 16	syl2anc	\|- ( ph -> U : I --> B )
18	17 10	ffvelcdmd	\|- ( ph -> ( U ` Y ) e. B )
19		oveq1	\|- ( x = ( U ` Y ) -> ( x oF .x. A ) = ( ( U ` Y ) oF .x. A ) )
20	19	oveq2d	\|- ( x = ( U ` Y ) -> ( T gsum ( x oF .x. A ) ) = ( T gsum ( ( U ` Y ) oF .x. A ) ) )
21		ovex	\|- ( T gsum ( ( U ` Y ) oF .x. A ) ) e. _V
22	20 5 21	fvmpt	\|- ( ( U ` Y ) e. B -> ( E ` ( U ` Y ) ) = ( T gsum ( ( U ` Y ) oF .x. A ) ) )
23	18 22	syl	\|- ( ph -> ( E ` ( U ` Y ) ) = ( T gsum ( ( U ` Y ) oF .x. A ) ) )
24		eqid	\|- ( 0g ` T ) = ( 0g ` T )
25		lmodcmn	\|- ( T e. LMod -> T e. CMnd )
26		cmnmnd	\|- ( T e. CMnd -> T e. Mnd )
27	6 25 26	3syl	\|- ( ph -> T e. Mnd )
28		eqid	\|- ( Base ` ( Scalar ` T ) ) = ( Base ` ( Scalar ` T ) )
29		eqid	\|- ( Base ` R ) = ( Base ` R )
30	1 29 2	frlmbasf	\|- ( ( I e. X /\ ( U ` Y ) e. B ) -> ( U ` Y ) : I --> ( Base ` R ) )
31	7 18 30	syl2anc	\|- ( ph -> ( U ` Y ) : I --> ( Base ` R ) )
32	8	fveq2d	\|- ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` T ) ) )
33	32	feq3d	\|- ( ph -> ( ( U ` Y ) : I --> ( Base ` R ) <-> ( U ` Y ) : I --> ( Base ` ( Scalar ` T ) ) ) )
34	31 33	mpbid	\|- ( ph -> ( U ` Y ) : I --> ( Base ` ( Scalar ` T ) ) )
35	12 28 4 3 6 34 9 7	lcomf	\|- ( ph -> ( ( U ` Y ) oF .x. A ) : I --> C )
36	31	ffnd	\|- ( ph -> ( U ` Y ) Fn I )
37	36	adantr	\|- ( ( ph /\ x e. ( I \ { Y } ) ) -> ( U ` Y ) Fn I )
38	9	ffnd	\|- ( ph -> A Fn I )
39	38	adantr	\|- ( ( ph /\ x e. ( I \ { Y } ) ) -> A Fn I )
40	7	adantr	\|- ( ( ph /\ x e. ( I \ { Y } ) ) -> I e. X )
41		eldifi	\|- ( x e. ( I \ { Y } ) -> x e. I )
42	41	adantl	\|- ( ( ph /\ x e. ( I \ { Y } ) ) -> x e. I )
43		fnfvof	\|- ( ( ( ( U ` Y ) Fn I /\ A Fn I ) /\ ( I e. X /\ x e. I ) ) -> ( ( ( U ` Y ) oF .x. A ) ` x ) = ( ( ( U ` Y ) ` x ) .x. ( A ` x ) ) )
44	37 39 40 42 43	syl22anc	\|- ( ( ph /\ x e. ( I \ { Y } ) ) -> ( ( ( U ` Y ) oF .x. A ) ` x ) = ( ( ( U ` Y ) ` x ) .x. ( A ` x ) ) )
45	15	adantr	\|- ( ( ph /\ x e. ( I \ { Y } ) ) -> R e. Ring )
46	10	adantr	\|- ( ( ph /\ x e. ( I \ { Y } ) ) -> Y e. I )
47		eldifsni	\|- ( x e. ( I \ { Y } ) -> x =/= Y )
48	47	necomd	\|- ( x e. ( I \ { Y } ) -> Y =/= x )
49	48	adantl	\|- ( ( ph /\ x e. ( I \ { Y } ) ) -> Y =/= x )
50		eqid	\|- ( 0g ` R ) = ( 0g ` R )
51	11 45 40 46 42 49 50	uvcvv0	\|- ( ( ph /\ x e. ( I \ { Y } ) ) -> ( ( U ` Y ) ` x ) = ( 0g ` R ) )
52	8	fveq2d	\|- ( ph -> ( 0g ` R ) = ( 0g ` ( Scalar ` T ) ) )
53	52	adantr	\|- ( ( ph /\ x e. ( I \ { Y } ) ) -> ( 0g ` R ) = ( 0g ` ( Scalar ` T ) ) )
54	51 53	eqtrd	\|- ( ( ph /\ x e. ( I \ { Y } ) ) -> ( ( U ` Y ) ` x ) = ( 0g ` ( Scalar ` T ) ) )
55	54	oveq1d	\|- ( ( ph /\ x e. ( I \ { Y } ) ) -> ( ( ( U ` Y ) ` x ) .x. ( A ` x ) ) = ( ( 0g ` ( Scalar ` T ) ) .x. ( A ` x ) ) )
56	6	adantr	\|- ( ( ph /\ x e. ( I \ { Y } ) ) -> T e. LMod )
57		ffvelcdm	\|- ( ( A : I --> C /\ x e. I ) -> ( A ` x ) e. C )
58	9 41 57	syl2an	\|- ( ( ph /\ x e. ( I \ { Y } ) ) -> ( A ` x ) e. C )
59		eqid	\|- ( 0g ` ( Scalar ` T ) ) = ( 0g ` ( Scalar ` T ) )
60	3 12 4 59 24	lmod0vs	\|- ( ( T e. LMod /\ ( A ` x ) e. C ) -> ( ( 0g ` ( Scalar ` T ) ) .x. ( A ` x ) ) = ( 0g ` T ) )
61	56 58 60	syl2anc	\|- ( ( ph /\ x e. ( I \ { Y } ) ) -> ( ( 0g ` ( Scalar ` T ) ) .x. ( A ` x ) ) = ( 0g ` T ) )
62	44 55 61	3eqtrd	\|- ( ( ph /\ x e. ( I \ { Y } ) ) -> ( ( ( U ` Y ) oF .x. A ) ` x ) = ( 0g ` T ) )
63	35 62	suppss	\|- ( ph -> ( ( ( U ` Y ) oF .x. A ) supp ( 0g ` T ) ) C_ { Y } )
64	3 24 27 7 10 35 63	gsumpt	\|- ( ph -> ( T gsum ( ( U ` Y ) oF .x. A ) ) = ( ( ( U ` Y ) oF .x. A ) ` Y ) )
65		fnfvof	\|- ( ( ( ( U ` Y ) Fn I /\ A Fn I ) /\ ( I e. X /\ Y e. I ) ) -> ( ( ( U ` Y ) oF .x. A ) ` Y ) = ( ( ( U ` Y ) ` Y ) .x. ( A ` Y ) ) )
66	36 38 7 10 65	syl22anc	\|- ( ph -> ( ( ( U ` Y ) oF .x. A ) ` Y ) = ( ( ( U ` Y ) ` Y ) .x. ( A ` Y ) ) )
67		eqid	\|- ( 1r ` R ) = ( 1r ` R )
68	11 15 7 10 67	uvcvv1	\|- ( ph -> ( ( U ` Y ) ` Y ) = ( 1r ` R ) )
69	8	fveq2d	\|- ( ph -> ( 1r ` R ) = ( 1r ` ( Scalar ` T ) ) )
70	68 69	eqtrd	\|- ( ph -> ( ( U ` Y ) ` Y ) = ( 1r ` ( Scalar ` T ) ) )
71	70	oveq1d	\|- ( ph -> ( ( ( U ` Y ) ` Y ) .x. ( A ` Y ) ) = ( ( 1r ` ( Scalar ` T ) ) .x. ( A ` Y ) ) )
72	9 10	ffvelcdmd	\|- ( ph -> ( A ` Y ) e. C )
73		eqid	\|- ( 1r ` ( Scalar ` T ) ) = ( 1r ` ( Scalar ` T ) )
74	3 12 4 73	lmodvs1	\|- ( ( T e. LMod /\ ( A ` Y ) e. C ) -> ( ( 1r ` ( Scalar ` T ) ) .x. ( A ` Y ) ) = ( A ` Y ) )
75	6 72 74	syl2anc	\|- ( ph -> ( ( 1r ` ( Scalar ` T ) ) .x. ( A ` Y ) ) = ( A ` Y ) )
76	66 71 75	3eqtrd	\|- ( ph -> ( ( ( U ` Y ) oF .x. A ) ` Y ) = ( A ` Y ) )
77	23 64 76	3eqtrd	\|- ( ph -> ( E ` ( U ` Y ) ) = ( A ` Y ) )

Metamath Proof Explorer

Theorem frlmup2

Proof