Theorem 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	⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
	frlmup.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
	frlmup.c	⊢ 𝐶 = ( Base ‘ 𝑇 )
	frlmup.v	⊢ · = ( ·𝑠 ‘ 𝑇 )
	frlmup.e	⊢ 𝐸 = ( 𝑥 ∈ 𝐵 ↦ ( 𝑇 Σg ( 𝑥 ∘f · 𝐴 ) ) )
	frlmup.t	⊢ ( 𝜑 → 𝑇 ∈ LMod )
	frlmup.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑋 )
	frlmup.r	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑇 ) )
	frlmup.a	⊢ ( 𝜑 → 𝐴 : 𝐼 ⟶ 𝐶 )
	frlmup.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐼 )
	frlmup.u	⊢ 𝑈 = ( 𝑅 unitVec 𝐼 )
Assertion	frlmup2	⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑈 ‘ 𝑌 ) ) = ( 𝐴 ‘ 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		frlmup.f	⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
2		frlmup.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
3		frlmup.c	⊢ 𝐶 = ( Base ‘ 𝑇 )
4		frlmup.v	⊢ · = ( ·𝑠 ‘ 𝑇 )
5		frlmup.e	⊢ 𝐸 = ( 𝑥 ∈ 𝐵 ↦ ( 𝑇 Σg ( 𝑥 ∘f · 𝐴 ) ) )
6		frlmup.t	⊢ ( 𝜑 → 𝑇 ∈ LMod )
7		frlmup.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑋 )
8		frlmup.r	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑇 ) )
9		frlmup.a	⊢ ( 𝜑 → 𝐴 : 𝐼 ⟶ 𝐶 )
10		frlmup.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐼 )
11		frlmup.u	⊢ 𝑈 = ( 𝑅 unitVec 𝐼 )
12		eqid	⊢ ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑇 )
13	12	lmodring	⊢ ( 𝑇 ∈ LMod → ( Scalar ‘ 𝑇 ) ∈ Ring )
14	6 13	syl	⊢ ( 𝜑 → ( Scalar ‘ 𝑇 ) ∈ Ring )
15	8 14	eqeltrd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
16	11 1 2	uvcff	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑋 ) → 𝑈 : 𝐼 ⟶ 𝐵 )
17	15 7 16	syl2anc	⊢ ( 𝜑 → 𝑈 : 𝐼 ⟶ 𝐵 )
18	17 10	ffvelcdmd	⊢ ( 𝜑 → ( 𝑈 ‘ 𝑌 ) ∈ 𝐵 )
19		oveq1	⊢ ( 𝑥 = ( 𝑈 ‘ 𝑌 ) → ( 𝑥 ∘f · 𝐴 ) = ( ( 𝑈 ‘ 𝑌 ) ∘f · 𝐴 ) )
20	19	oveq2d	⊢ ( 𝑥 = ( 𝑈 ‘ 𝑌 ) → ( 𝑇 Σg ( 𝑥 ∘f · 𝐴 ) ) = ( 𝑇 Σg ( ( 𝑈 ‘ 𝑌 ) ∘f · 𝐴 ) ) )
21		ovex	⊢ ( 𝑇 Σg ( ( 𝑈 ‘ 𝑌 ) ∘f · 𝐴 ) ) ∈ V
22	20 5 21	fvmpt	⊢ ( ( 𝑈 ‘ 𝑌 ) ∈ 𝐵 → ( 𝐸 ‘ ( 𝑈 ‘ 𝑌 ) ) = ( 𝑇 Σg ( ( 𝑈 ‘ 𝑌 ) ∘f · 𝐴 ) ) )
23	18 22	syl	⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑈 ‘ 𝑌 ) ) = ( 𝑇 Σg ( ( 𝑈 ‘ 𝑌 ) ∘f · 𝐴 ) ) )
24		eqid	⊢ ( 0g ‘ 𝑇 ) = ( 0g ‘ 𝑇 )
25		lmodcmn	⊢ ( 𝑇 ∈ LMod → 𝑇 ∈ CMnd )
26		cmnmnd	⊢ ( 𝑇 ∈ CMnd → 𝑇 ∈ Mnd )
27	6 25 26	3syl	⊢ ( 𝜑 → 𝑇 ∈ Mnd )
28		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑇 ) ) = ( Base ‘ ( Scalar ‘ 𝑇 ) )
29		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
30	1 29 2	frlmbasf	⊢ ( ( 𝐼 ∈ 𝑋 ∧ ( 𝑈 ‘ 𝑌 ) ∈ 𝐵 ) → ( 𝑈 ‘ 𝑌 ) : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
31	7 18 30	syl2anc	⊢ ( 𝜑 → ( 𝑈 ‘ 𝑌 ) : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
32	8	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑇 ) ) )
33	32	feq3d	⊢ ( 𝜑 → ( ( 𝑈 ‘ 𝑌 ) : 𝐼 ⟶ ( Base ‘ 𝑅 ) ↔ ( 𝑈 ‘ 𝑌 ) : 𝐼 ⟶ ( Base ‘ ( Scalar ‘ 𝑇 ) ) ) )
34	31 33	mpbid	⊢ ( 𝜑 → ( 𝑈 ‘ 𝑌 ) : 𝐼 ⟶ ( Base ‘ ( Scalar ‘ 𝑇 ) ) )
35	12 28 4 3 6 34 9 7	lcomf	⊢ ( 𝜑 → ( ( 𝑈 ‘ 𝑌 ) ∘f · 𝐴 ) : 𝐼 ⟶ 𝐶 )
36	31	ffnd	⊢ ( 𝜑 → ( 𝑈 ‘ 𝑌 ) Fn 𝐼 )
37	36	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ { 𝑌 } ) ) → ( 𝑈 ‘ 𝑌 ) Fn 𝐼 )
38	9	ffnd	⊢ ( 𝜑 → 𝐴 Fn 𝐼 )
39	38	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ { 𝑌 } ) ) → 𝐴 Fn 𝐼 )
40	7	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ { 𝑌 } ) ) → 𝐼 ∈ 𝑋 )
41		eldifi	⊢ ( 𝑥 ∈ ( 𝐼 ∖ { 𝑌 } ) → 𝑥 ∈ 𝐼 )
42	41	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ { 𝑌 } ) ) → 𝑥 ∈ 𝐼 )
43		fnfvof	⊢ ( ( ( ( 𝑈 ‘ 𝑌 ) Fn 𝐼 ∧ 𝐴 Fn 𝐼 ) ∧ ( 𝐼 ∈ 𝑋 ∧ 𝑥 ∈ 𝐼 ) ) → ( ( ( 𝑈 ‘ 𝑌 ) ∘f · 𝐴 ) ‘ 𝑥 ) = ( ( ( 𝑈 ‘ 𝑌 ) ‘ 𝑥 ) · ( 𝐴 ‘ 𝑥 ) ) )
44	37 39 40 42 43	syl22anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ { 𝑌 } ) ) → ( ( ( 𝑈 ‘ 𝑌 ) ∘f · 𝐴 ) ‘ 𝑥 ) = ( ( ( 𝑈 ‘ 𝑌 ) ‘ 𝑥 ) · ( 𝐴 ‘ 𝑥 ) ) )
45	15	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ { 𝑌 } ) ) → 𝑅 ∈ Ring )
46	10	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ { 𝑌 } ) ) → 𝑌 ∈ 𝐼 )
47		eldifsni	⊢ ( 𝑥 ∈ ( 𝐼 ∖ { 𝑌 } ) → 𝑥 ≠ 𝑌 )
48	47	necomd	⊢ ( 𝑥 ∈ ( 𝐼 ∖ { 𝑌 } ) → 𝑌 ≠ 𝑥 )
49	48	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ { 𝑌 } ) ) → 𝑌 ≠ 𝑥 )
50		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
51	11 45 40 46 42 49 50	uvcvv0	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ { 𝑌 } ) ) → ( ( 𝑈 ‘ 𝑌 ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) )
52	8	fveq2d	⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( Scalar ‘ 𝑇 ) ) )
53	52	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ { 𝑌 } ) ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( Scalar ‘ 𝑇 ) ) )
54	51 53	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ { 𝑌 } ) ) → ( ( 𝑈 ‘ 𝑌 ) ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑇 ) ) )
55	54	oveq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ { 𝑌 } ) ) → ( ( ( 𝑈 ‘ 𝑌 ) ‘ 𝑥 ) · ( 𝐴 ‘ 𝑥 ) ) = ( ( 0g ‘ ( Scalar ‘ 𝑇 ) ) · ( 𝐴 ‘ 𝑥 ) ) )
56	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ { 𝑌 } ) ) → 𝑇 ∈ LMod )
57		ffvelcdm	⊢ ( ( 𝐴 : 𝐼 ⟶ 𝐶 ∧ 𝑥 ∈ 𝐼 ) → ( 𝐴 ‘ 𝑥 ) ∈ 𝐶 )
58	9 41 57	syl2an	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ { 𝑌 } ) ) → ( 𝐴 ‘ 𝑥 ) ∈ 𝐶 )
59		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝑇 ) ) = ( 0g ‘ ( Scalar ‘ 𝑇 ) )
60	3 12 4 59 24	lmod0vs	⊢ ( ( 𝑇 ∈ LMod ∧ ( 𝐴 ‘ 𝑥 ) ∈ 𝐶 ) → ( ( 0g ‘ ( Scalar ‘ 𝑇 ) ) · ( 𝐴 ‘ 𝑥 ) ) = ( 0g ‘ 𝑇 ) )
61	56 58 60	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ { 𝑌 } ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑇 ) ) · ( 𝐴 ‘ 𝑥 ) ) = ( 0g ‘ 𝑇 ) )
62	44 55 61	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ { 𝑌 } ) ) → ( ( ( 𝑈 ‘ 𝑌 ) ∘f · 𝐴 ) ‘ 𝑥 ) = ( 0g ‘ 𝑇 ) )
63	35 62	suppss	⊢ ( 𝜑 → ( ( ( 𝑈 ‘ 𝑌 ) ∘f · 𝐴 ) supp ( 0g ‘ 𝑇 ) ) ⊆ { 𝑌 } )
64	3 24 27 7 10 35 63	gsumpt	⊢ ( 𝜑 → ( 𝑇 Σg ( ( 𝑈 ‘ 𝑌 ) ∘f · 𝐴 ) ) = ( ( ( 𝑈 ‘ 𝑌 ) ∘f · 𝐴 ) ‘ 𝑌 ) )
65		fnfvof	⊢ ( ( ( ( 𝑈 ‘ 𝑌 ) Fn 𝐼 ∧ 𝐴 Fn 𝐼 ) ∧ ( 𝐼 ∈ 𝑋 ∧ 𝑌 ∈ 𝐼 ) ) → ( ( ( 𝑈 ‘ 𝑌 ) ∘f · 𝐴 ) ‘ 𝑌 ) = ( ( ( 𝑈 ‘ 𝑌 ) ‘ 𝑌 ) · ( 𝐴 ‘ 𝑌 ) ) )
66	36 38 7 10 65	syl22anc	⊢ ( 𝜑 → ( ( ( 𝑈 ‘ 𝑌 ) ∘f · 𝐴 ) ‘ 𝑌 ) = ( ( ( 𝑈 ‘ 𝑌 ) ‘ 𝑌 ) · ( 𝐴 ‘ 𝑌 ) ) )
67		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
68	11 15 7 10 67	uvcvv1	⊢ ( 𝜑 → ( ( 𝑈 ‘ 𝑌 ) ‘ 𝑌 ) = ( 1r ‘ 𝑅 ) )
69	8	fveq2d	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) = ( 1r ‘ ( Scalar ‘ 𝑇 ) ) )
70	68 69	eqtrd	⊢ ( 𝜑 → ( ( 𝑈 ‘ 𝑌 ) ‘ 𝑌 ) = ( 1r ‘ ( Scalar ‘ 𝑇 ) ) )
71	70	oveq1d	⊢ ( 𝜑 → ( ( ( 𝑈 ‘ 𝑌 ) ‘ 𝑌 ) · ( 𝐴 ‘ 𝑌 ) ) = ( ( 1r ‘ ( Scalar ‘ 𝑇 ) ) · ( 𝐴 ‘ 𝑌 ) ) )
72	9 10	ffvelcdmd	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑌 ) ∈ 𝐶 )
73		eqid	⊢ ( 1r ‘ ( Scalar ‘ 𝑇 ) ) = ( 1r ‘ ( Scalar ‘ 𝑇 ) )
74	3 12 4 73	lmodvs1	⊢ ( ( 𝑇 ∈ LMod ∧ ( 𝐴 ‘ 𝑌 ) ∈ 𝐶 ) → ( ( 1r ‘ ( Scalar ‘ 𝑇 ) ) · ( 𝐴 ‘ 𝑌 ) ) = ( 𝐴 ‘ 𝑌 ) )
75	6 72 74	syl2anc	⊢ ( 𝜑 → ( ( 1r ‘ ( Scalar ‘ 𝑇 ) ) · ( 𝐴 ‘ 𝑌 ) ) = ( 𝐴 ‘ 𝑌 ) )
76	66 71 75	3eqtrd	⊢ ( 𝜑 → ( ( ( 𝑈 ‘ 𝑌 ) ∘f · 𝐴 ) ‘ 𝑌 ) = ( 𝐴 ‘ 𝑌 ) )
77	23 64 76	3eqtrd	⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑈 ‘ 𝑌 ) ) = ( 𝐴 ‘ 𝑌 ) )