This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑈 ‘ 𝑌 ) ) = ( 𝐴 ‘ 𝑌 ) )