frlmipval

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

	Ref	Expression
Hypotheses	frlmphl.y	$⊢ Y = R freeLMod I$
	frlmphl.b	$⊢ B = {Base}_{R}$
	frlmphl.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	frlmphl.v	$⊢ V = {Base}_{Y}$
	frlmphl.j	$⊢ \underset{˙}{,} = \cdot_{𝑖} (Y)$
Assertion	frlmipval	$⊢ ((I \in W \land R \in X) \land (F \in V \land G \in V)) \to F \underset{˙}{,} G = \sum_{R} (F {\underset{˙}{\cdot}}_{f} G)$

Proof

Step	Hyp	Ref	Expression
1		frlmphl.y	$⊢ Y = R freeLMod I$
2		frlmphl.b	$⊢ B = {Base}_{R}$
3		frlmphl.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		frlmphl.v	$⊢ V = {Base}_{Y}$
5		frlmphl.j	$⊢ \underset{˙}{,} = \cdot_{𝑖} (Y)$
6	1 2 4	frlmbasmap	$⊢ (I \in W \land F \in V) \to F \in (B^{I})$
7	6	ad2ant2r	$⊢ ((I \in W \land R \in X) \land (F \in V \land G \in V)) \to F \in (B^{I})$
8		elmapi	$⊢ F \in (B^{I}) \to F : I ⟶ B$
9		ffn	$⊢ F : I ⟶ B \to F Fn I$
10	7 8 9	3syl	$⊢ ((I \in W \land R \in X) \land (F \in V \land G \in V)) \to F Fn I$
11	1 2 4	frlmbasmap	$⊢ (I \in W \land G \in V) \to G \in (B^{I})$
12	11	ad2ant2rl	$⊢ ((I \in W \land R \in X) \land (F \in V \land G \in V)) \to G \in (B^{I})$
13		elmapi	$⊢ G \in (B^{I}) \to G : I ⟶ B$
14		ffn	$⊢ G : I ⟶ B \to G Fn I$
15	12 13 14	3syl	$⊢ ((I \in W \land R \in X) \land (F \in V \land G \in V)) \to G Fn I$
16		simpll	$⊢ ((I \in W \land R \in X) \land (F \in V \land G \in V)) \to I \in W$
17		inidm	$⊢ I \cap I = I$
18		eqidd	$⊢ (((I \in W \land R \in X) \land (F \in V \land G \in V)) \land x \in I) \to F (x) = F (x)$
19		eqidd	$⊢ (((I \in W \land R \in X) \land (F \in V \land G \in V)) \land x \in I) \to G (x) = G (x)$
20	10 15 16 16 17 18 19	offval	$⊢ ((I \in W \land R \in X) \land (F \in V \land G \in V)) \to F {\underset{˙}{\cdot}}_{f} G = (x \in I ⟼ F (x) \underset{˙}{\cdot} G (x))$
21	20	oveq2d	$⊢ ((I \in W \land R \in X) \land (F \in V \land G \in V)) \to \sum_{R} (F {\underset{˙}{\cdot}}_{f} G) = \underset{x \in I}{\sum_{R}} (F (x) \underset{˙}{\cdot} G (x))$
22		ovexd	$⊢ ((I \in W \land R \in X) \land (F \in V \land G \in V)) \to \underset{x \in I}{\sum_{R}} (F (x) \underset{˙}{\cdot} G (x)) \in V$
23		fveq1	$⊢ f = F \to f (x) = F (x)$
24	23	oveq1d	$⊢ f = F \to f (x) \underset{˙}{\cdot} g (x) = F (x) \underset{˙}{\cdot} g (x)$
25	24	mpteq2dv	$⊢ f = F \to (x \in I ⟼ f (x) \underset{˙}{\cdot} g (x)) = (x \in I ⟼ F (x) \underset{˙}{\cdot} g (x))$
26	25	oveq2d	$⊢ f = F \to \underset{x \in I}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (x)) = \underset{x \in I}{\sum_{R}} (F (x) \underset{˙}{\cdot} g (x))$
27		fveq1	$⊢ g = G \to g (x) = G (x)$
28	27	oveq2d	$⊢ g = G \to F (x) \underset{˙}{\cdot} g (x) = F (x) \underset{˙}{\cdot} G (x)$
29	28	mpteq2dv	$⊢ g = G \to (x \in I ⟼ F (x) \underset{˙}{\cdot} g (x)) = (x \in I ⟼ F (x) \underset{˙}{\cdot} G (x))$
30	29	oveq2d	$⊢ g = G \to \underset{x \in I}{\sum_{R}} (F (x) \underset{˙}{\cdot} g (x)) = \underset{x \in I}{\sum_{R}} (F (x) \underset{˙}{\cdot} G (x))$
31		eqid	$⊢ (f \in (B^{I}), g \in (B^{I}) ⟼ \underset{x \in I}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (x))) = (f \in (B^{I}), g \in (B^{I}) ⟼ \underset{x \in I}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (x)))$
32	26 30 31	ovmpog	$⊢ (F \in (B^{I}) \land G \in (B^{I}) \land \underset{x \in I}{\sum_{R}} (F (x) \underset{˙}{\cdot} G (x)) \in V) \to F (f \in (B^{I}), g \in (B^{I}) ⟼ \underset{x \in I}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (x))) G = \underset{x \in I}{\sum_{R}} (F (x) \underset{˙}{\cdot} G (x))$
33	7 12 22 32	syl3anc	$⊢ ((I \in W \land R \in X) \land (F \in V \land G \in V)) \to F (f \in (B^{I}), g \in (B^{I}) ⟼ \underset{x \in I}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (x))) G = \underset{x \in I}{\sum_{R}} (F (x) \underset{˙}{\cdot} G (x))$
34	1 2 3	frlmip	$⊢ (I \in W \land R \in X) \to (f \in (B^{I}), g \in (B^{I}) ⟼ \underset{x \in I}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (x))) = \cdot_{𝑖} (Y)$
35	34	adantr	$⊢ ((I \in W \land R \in X) \land (F \in V \land G \in V)) \to (f \in (B^{I}), g \in (B^{I}) ⟼ \underset{x \in I}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (x))) = \cdot_{𝑖} (Y)$
36	35 5	eqtr4di	$⊢ ((I \in W \land R \in X) \land (F \in V \land G \in V)) \to (f \in (B^{I}), g \in (B^{I}) ⟼ \underset{x \in I}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (x))) = \underset{˙}{,}$
37	36	oveqd	$⊢ ((I \in W \land R \in X) \land (F \in V \land G \in V)) \to F (f \in (B^{I}), g \in (B^{I}) ⟼ \underset{x \in I}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (x))) G = F \underset{˙}{,} G$
38	21 33 37	3eqtr2rd	$⊢ ((I \in W \land R \in X) \land (F \in V \land G \in V)) \to F \underset{˙}{,} G = \sum_{R} (F {\underset{˙}{\cdot}}_{f} G)$

Metamath Proof Explorer

Theorem frlmipval

Proof