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 · 𝐺 ) ) )