frlmip

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

	Ref	Expression
Hypotheses	frlmphl.y	$⊢ Y = R freeLMod I$
	frlmphl.b	$⊢ B = {Base}_{R}$
	frlmphl.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	frlmip	$⊢ (I \in W \land R \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)$

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		eqid	$⊢ R freeLMod I = R freeLMod I$
5		eqid	$⊢ {Base}_{(R freeLMod I)} = {Base}_{(R freeLMod I)}$
6	4 5	frlmpws	$⊢ (R \in V \land I \in W) \to R freeLMod I = (ringLMod (R) ↑_{𝑠} I) ↾_{𝑠} {Base}_{(R freeLMod I)}$
7	6	ancoms	$⊢ (I \in W \land R \in V) \to R freeLMod I = (ringLMod (R) ↑_{𝑠} I) ↾_{𝑠} {Base}_{(R freeLMod I)}$
8	2	ressid	$⊢ R \in V \to R ↾_{𝑠} B = R$
9		eqidd	$⊢ R \in V \to subringAlg (R) (B) = subringAlg (R) (B)$
10	2	eqimssi	$⊢ B \subseteq {Base}_{R}$
11	10	a1i	$⊢ R \in V \to B \subseteq {Base}_{R}$
12	9 11	srasca	$⊢ R \in V \to R ↾_{𝑠} B = Scalar (subringAlg (R) (B))$
13	8 12	eqtr3d	$⊢ R \in V \to R = Scalar (subringAlg (R) (B))$
14	13	oveq1d	$⊢ R \in V \to R ⨉_{𝑠} (I \times \{subringAlg (R) (B)\}) = Scalar (subringAlg (R) (B)) ⨉_{𝑠} (I \times \{subringAlg (R) (B)\})$
15	14	adantl	$⊢ (I \in W \land R \in V) \to R ⨉_{𝑠} (I \times \{subringAlg (R) (B)\}) = Scalar (subringAlg (R) (B)) ⨉_{𝑠} (I \times \{subringAlg (R) (B)\})$
16		fvex	$⊢ subringAlg (R) (B) \in V$
17		rlmval	$⊢ ringLMod (R) = subringAlg (R) ({Base}_{R})$
18	2	fveq2i	$⊢ subringAlg (R) (B) = subringAlg (R) ({Base}_{R})$
19	17 18	eqtr4i	$⊢ ringLMod (R) = subringAlg (R) (B)$
20	19	oveq1i	$⊢ ringLMod (R) ↑_{𝑠} I = subringAlg (R) (B) ↑_{𝑠} I$
21		eqid	$⊢ Scalar (subringAlg (R) (B)) = Scalar (subringAlg (R) (B))$
22	20 21	pwsval	$⊢ (subringAlg (R) (B) \in V \land I \in W) \to ringLMod (R) ↑_{𝑠} I = Scalar (subringAlg (R) (B)) ⨉_{𝑠} (I \times \{subringAlg (R) (B)\})$
23	16 22	mpan	$⊢ I \in W \to ringLMod (R) ↑_{𝑠} I = Scalar (subringAlg (R) (B)) ⨉_{𝑠} (I \times \{subringAlg (R) (B)\})$
24	23	adantr	$⊢ (I \in W \land R \in V) \to ringLMod (R) ↑_{𝑠} I = Scalar (subringAlg (R) (B)) ⨉_{𝑠} (I \times \{subringAlg (R) (B)\})$
25	15 24	eqtr4d	$⊢ (I \in W \land R \in V) \to R ⨉_{𝑠} (I \times \{subringAlg (R) (B)\}) = ringLMod (R) ↑_{𝑠} I$
26	1	fveq2i	$⊢ {Base}_{Y} = {Base}_{(R freeLMod I)}$
27	26	a1i	$⊢ (I \in W \land R \in V) \to {Base}_{Y} = {Base}_{(R freeLMod I)}$
28	25 27	oveq12d	$⊢ (I \in W \land R \in V) \to (R ⨉_{𝑠} (I \times \{subringAlg (R) (B)\})) ↾_{𝑠} {Base}_{Y} = (ringLMod (R) ↑_{𝑠} I) ↾_{𝑠} {Base}_{(R freeLMod I)}$
29	7 28	eqtr4d	$⊢ (I \in W \land R \in V) \to R freeLMod I = (R ⨉_{𝑠} (I \times \{subringAlg (R) (B)\})) ↾_{𝑠} {Base}_{Y}$
30	1 29	syl5eq	$⊢ (I \in W \land R \in V) \to Y = (R ⨉_{𝑠} (I \times \{subringAlg (R) (B)\})) ↾_{𝑠} {Base}_{Y}$
31	30	fveq2d	$⊢ (I \in W \land R \in V) \to \cdot_{𝑖} (Y) = \cdot_{𝑖} ((R ⨉_{𝑠} (I \times \{subringAlg (R) (B)\})) ↾_{𝑠} {Base}_{Y})$
32		fvex	$⊢ {Base}_{Y} \in V$
33		eqid	$⊢ (R ⨉_{𝑠} (I \times \{subringAlg (R) (B)\})) ↾_{𝑠} {Base}_{Y} = (R ⨉_{𝑠} (I \times \{subringAlg (R) (B)\})) ↾_{𝑠} {Base}_{Y}$
34		eqid	$⊢ \cdot_{𝑖} (R ⨉_{𝑠} (I \times \{subringAlg (R) (B)\})) = \cdot_{𝑖} (R ⨉_{𝑠} (I \times \{subringAlg (R) (B)\}))$
35	33 34	ressip	$⊢ {Base}_{Y} \in V \to \cdot_{𝑖} (R ⨉_{𝑠} (I \times \{subringAlg (R) (B)\})) = \cdot_{𝑖} ((R ⨉_{𝑠} (I \times \{subringAlg (R) (B)\})) ↾_{𝑠} {Base}_{Y})$
36	32 35	ax-mp	$⊢ \cdot_{𝑖} (R ⨉_{𝑠} (I \times \{subringAlg (R) (B)\})) = \cdot_{𝑖} ((R ⨉_{𝑠} (I \times \{subringAlg (R) (B)\})) ↾_{𝑠} {Base}_{Y})$
37		eqid	$⊢ R ⨉_{𝑠} (I \times \{subringAlg (R) (B)\}) = R ⨉_{𝑠} (I \times \{subringAlg (R) (B)\})$
38		simpr	$⊢ (I \in W \land R \in V) \to R \in V$
39		snex	$⊢ \{subringAlg (R) (B)\} \in V$
40		xpexg	$⊢ (I \in W \land \{subringAlg (R) (B)\} \in V) \to I \times \{subringAlg (R) (B)\} \in V$
41	39 40	mpan2	$⊢ I \in W \to I \times \{subringAlg (R) (B)\} \in V$
42	41	adantr	$⊢ (I \in W \land R \in V) \to I \times \{subringAlg (R) (B)\} \in V$
43		eqid	$⊢ {Base}_{(R ⨉_{𝑠} (I \times \{subringAlg (R) (B)\}))} = {Base}_{(R ⨉_{𝑠} (I \times \{subringAlg (R) (B)\}))}$
44	16	snnz	$⊢ \{subringAlg (R) (B)\} \neq \emptyset$
45		dmxp	$⊢ \{subringAlg (R) (B)\} \neq \emptyset \to dom (I \times \{subringAlg (R) (B)\}) = I$
46	44 45	mp1i	$⊢ (I \in W \land R \in V) \to dom (I \times \{subringAlg (R) (B)\}) = I$
47	37 38 42 43 46 34	prdsip	$⊢ (I \in W \land R \in V) \to \cdot_{𝑖} (R ⨉_{𝑠} (I \times \{subringAlg (R) (B)\})) = (f \in {Base}_{(R ⨉_{𝑠} (I \times \{subringAlg (R) (B)\}))}, g \in {Base}_{(R ⨉_{𝑠} (I \times \{subringAlg (R) (B)\}))} ⟼ \underset{x \in I}{\sum_{R}} (f (x) \cdot_{𝑖} ((I \times \{subringAlg (R) (B)\}) (x)) g (x)))$
48	37 38 42 43 46	prdsbas	$⊢ (I \in W \land R \in V) \to {Base}_{(R ⨉_{𝑠} (I \times \{subringAlg (R) (B)\}))} = \underset{x \in I}{⨉} {Base}_{(I \times \{subringAlg (R) (B)\}) (x)}$
49		eqidd	$⊢ x \in I \to subringAlg (R) (B) = subringAlg (R) (B)$
50	10	a1i	$⊢ x \in I \to B \subseteq {Base}_{R}$
51	49 50	srabase	$⊢ x \in I \to {Base}_{R} = {Base}_{subringAlg (R) (B)}$
52	2	a1i	$⊢ x \in I \to B = {Base}_{R}$
53	16	fvconst2	$⊢ x \in I \to (I \times \{subringAlg (R) (B)\}) (x) = subringAlg (R) (B)$
54	53	fveq2d	$⊢ x \in I \to {Base}_{(I \times \{subringAlg (R) (B)\}) (x)} = {Base}_{subringAlg (R) (B)}$
55	51 52 54	3eqtr4rd	$⊢ x \in I \to {Base}_{(I \times \{subringAlg (R) (B)\}) (x)} = B$
56	55	adantl	$⊢ ((I \in W \land R \in V) \land x \in I) \to {Base}_{(I \times \{subringAlg (R) (B)\}) (x)} = B$
57	56	ixpeq2dva	$⊢ (I \in W \land R \in V) \to \underset{x \in I}{⨉} {Base}_{(I \times \{subringAlg (R) (B)\}) (x)} = \underset{x \in I}{⨉} B$
58	2	fvexi	$⊢ B \in V$
59		ixpconstg	$⊢ (I \in W \land B \in V) \to \underset{x \in I}{⨉} B = B^{I}$
60	58 59	mpan2	$⊢ I \in W \to \underset{x \in I}{⨉} B = B^{I}$
61	60	adantr	$⊢ (I \in W \land R \in V) \to \underset{x \in I}{⨉} B = B^{I}$
62	48 57 61	3eqtrd	$⊢ (I \in W \land R \in V) \to {Base}_{(R ⨉_{𝑠} (I \times \{subringAlg (R) (B)\}))} = B^{I}$
63	53 50	sraip	$⊢ x \in I \to \cdot_{R} = \cdot_{𝑖} ((I \times \{subringAlg (R) (B)\}) (x))$
64	3 63	syl5req	$⊢ x \in I \to \cdot_{𝑖} ((I \times \{subringAlg (R) (B)\}) (x)) = \underset{˙}{\cdot}$
65	64	oveqd	$⊢ x \in I \to f (x) \cdot_{𝑖} ((I \times \{subringAlg (R) (B)\}) (x)) g (x) = f (x) \underset{˙}{\cdot} g (x)$
66	65	mpteq2ia	$⊢ (x \in I ⟼ f (x) \cdot_{𝑖} ((I \times \{subringAlg (R) (B)\}) (x)) g (x)) = (x \in I ⟼ f (x) \underset{˙}{\cdot} g (x))$
67	66	oveq2i	$⊢ \underset{x \in I}{\sum_{R}} (f (x) \cdot_{𝑖} ((I \times \{subringAlg (R) (B)\}) (x)) g (x)) = \underset{x \in I}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (x))$
68	67	a1i	$⊢ (I \in W \land R \in V) \to \underset{x \in I}{\sum_{R}} (f (x) \cdot_{𝑖} ((I \times \{subringAlg (R) (B)\}) (x)) g (x)) = \underset{x \in I}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (x))$
69	62 62 68	mpoeq123dv	$⊢ (I \in W \land R \in V) \to (f \in {Base}_{(R ⨉_{𝑠} (I \times \{subringAlg (R) (B)\}))}, g \in {Base}_{(R ⨉_{𝑠} (I \times \{subringAlg (R) (B)\}))} ⟼ \underset{x \in I}{\sum_{R}} (f (x) \cdot_{𝑖} ((I \times \{subringAlg (R) (B)\}) (x)) g (x))) = (f \in (B^{I}), g \in (B^{I}) ⟼ \underset{x \in I}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (x)))$
70	47 69	eqtrd	$⊢ (I \in W \land R \in V) \to \cdot_{𝑖} (R ⨉_{𝑠} (I \times \{subringAlg (R) (B)\})) = (f \in (B^{I}), g \in (B^{I}) ⟼ \underset{x \in I}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (x)))$
71	36 70	syl5eqr	$⊢ (I \in W \land R \in V) \to \cdot_{𝑖} ((R ⨉_{𝑠} (I \times \{subringAlg (R) (B)\})) ↾_{𝑠} {Base}_{Y}) = (f \in (B^{I}), g \in (B^{I}) ⟼ \underset{x \in I}{\sum_{R}} (f (x) \underset{˙}{\cdot} g (x)))$
72	31 71	eqtr2d	$⊢ (I \in W \land R \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)$

Metamath Proof Explorer

Theorem frlmip

Proof