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