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

Metamath Proof Explorer

Theorem frlmipval

Description: The inner product of a free module. (Contributed by Thierry Arnoux, 21-Jun-2019)

Ref Expression
Hypotheses frlmphl.y ⊢ 𝑌 = ( 𝑅 freeLMod 𝐼 )
frlmphl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
frlmphl.t ⊢ · = ( .r ‘ 𝑅 )
frlmphl.v ⊢ 𝑉 = ( Base ‘ 𝑌 )
frlmphl.j ⊢ , = ( ·𝑖 ‘ 𝑌 )
Assertion frlmipval ( ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑋 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) → ( 𝐹 , 𝐺 ) = ( 𝑅 Σg ( 𝐹 ∘f · 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 frlmphl.y ⊢ 𝑌 = ( 𝑅 freeLMod 𝐼 )
2 frlmphl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 frlmphl.t ⊢ · = ( .r ‘ 𝑅 )
4 frlmphl.v ⊢ 𝑉 = ( Base ‘ 𝑌 )
5 frlmphl.j ⊢ , = ( ·𝑖 ‘ 𝑌 )
6 1 2 4 frlmbasmap ⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝐹 ∈ 𝑉 ) → 𝐹 ∈ ( 𝐵 ↑m 𝐼 ) )
7 6 ad2ant2r ⊢ ( ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑋 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) → 𝐹 ∈ ( 𝐵 ↑m 𝐼 ) )
8 elmapi ⊢ ( 𝐹 ∈ ( 𝐵 ↑m 𝐼 ) → 𝐹 : 𝐼 ⟶ 𝐵 )
9 ffn ⊢ ( 𝐹 : 𝐼 ⟶ 𝐵 → 𝐹 Fn 𝐼 )
10 7 8 9 3syl ⊢ ( ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑋 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) → 𝐹 Fn 𝐼 )
11 1 2 4 frlmbasmap ⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝐺 ∈ 𝑉 ) → 𝐺 ∈ ( 𝐵 ↑m 𝐼 ) )
12 11 ad2ant2rl ⊢ ( ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑋 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) → 𝐺 ∈ ( 𝐵 ↑m 𝐼 ) )
13 elmapi ⊢ ( 𝐺 ∈ ( 𝐵 ↑m 𝐼 ) → 𝐺 : 𝐼 ⟶ 𝐵 )
14 ffn ⊢ ( 𝐺 : 𝐼 ⟶ 𝐵 → 𝐺 Fn 𝐼 )
15 12 13 14 3syl ⊢ ( ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑋 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) → 𝐺 Fn 𝐼 )
16 simpll ⊢ ( ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑋 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) → 𝐼 ∈ 𝑊 )
17 inidm ⊢ ( 𝐼 ∩ 𝐼 ) = 𝐼
18 eqidd ⊢ ( ( ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑋 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
19 eqidd ⊢ ( ( ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑋 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
20 10 15 16 16 17 18 19 offval ⊢ ( ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑋 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) → ( 𝐹 ∘f · 𝐺 ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) )
21 20 oveq2d ⊢ ( ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑋 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) → ( 𝑅 Σg ( 𝐹 ∘f · 𝐺 ) ) = ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) ) )
22 ovexd ⊢ ( ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑋 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) → ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ V )
23 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
24 23 oveq1d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) )
25 24 mpteq2dv ⊢ ( 𝑓 = 𝐹 → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) ) )
26 25 oveq2d ⊢ ( 𝑓 = 𝐹 → ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) ) ) = ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) ) ) )
27 fveq1 ⊢ ( 𝑔 = 𝐺 → ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
28 27 oveq2d ⊢ ( 𝑔 = 𝐺 → ( ( 𝐹 ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) )
29 28 mpteq2dv ⊢ ( 𝑔 = 𝐺 → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) )
30 29 oveq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) ) ) = ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) ) )
31 eqid ⊢ ( 𝑓 ∈ ( 𝐵 ↑m 𝐼 ) , 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) ) ) ) = ( 𝑓 ∈ ( 𝐵 ↑m 𝐼 ) , 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) ) ) )
32 26 30 31 ovmpog ⊢ ( ( 𝐹 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝐺 ∈ ( 𝐵 ↑m 𝐼 ) ∧ ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ V ) → ( 𝐹 ( 𝑓 ∈ ( 𝐵 ↑m 𝐼 ) , 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) ) ) ) 𝐺 ) = ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) ) )
33 7 12 22 32 syl3anc ⊢ ( ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑋 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) → ( 𝐹 ( 𝑓 ∈ ( 𝐵 ↑m 𝐼 ) , 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) ) ) ) 𝐺 ) = ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) ) )
34 1 2 3 frlmip ⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑋 ) → ( 𝑓 ∈ ( 𝐵 ↑m 𝐼 ) , 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) ) ) ) = ( ·𝑖 ‘ 𝑌 ) )
35 34 adantr ⊢ ( ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑋 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) → ( 𝑓 ∈ ( 𝐵 ↑m 𝐼 ) , 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) ) ) ) = ( ·𝑖 ‘ 𝑌 ) )
36 35 5 eqtr4di ⊢ ( ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑋 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) → ( 𝑓 ∈ ( 𝐵 ↑m 𝐼 ) , 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) ) ) ) = , )
37 36 oveqd ⊢ ( ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑋 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) → ( 𝐹 ( 𝑓 ∈ ( 𝐵 ↑m 𝐼 ) , 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑅 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ 𝑥 ) ) ) ) ) 𝐺 ) = ( 𝐹 , 𝐺 ) )
38 21 33 37 3eqtr2rd ⊢ ( ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ 𝑋 ) ∧ ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) → ( 𝐹 , 𝐺 ) = ( 𝑅 Σg ( 𝐹 ∘f · 𝐺 ) ) )