Theorem frlmvscavalb

Description: Scalar multiplication in a free module at the coordinates. (Contributed by AV, 16-Jan-2023)

	Ref	Expression
Hypotheses	frlmplusgvalb.f	$$⊢F=R\mathrm{freeLMod}I$$
	frlmplusgvalb.b	$$⊢B={\mathrm{Base}}_F$$
	frlmplusgvalb.i	$$⊢\phi \to I\in W$$
	frlmplusgvalb.x	$$⊢\phi \to X\in B$$
	frlmplusgvalb.z	$$⊢\phi \to Z\in B$$
	frlmplusgvalb.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	frlmvscavalb.k	$$⊢K={\mathrm{Base}}_R$$
	frlmvscavalb.a	$$⊢\phi \to A\in K$$
	frlmvscavalb.v	$$⊢\underset{\dot{}}{\bullet }={\cdot }_F$$
	frlmvscavalb.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
Assertion	frlmvscavalb	$$⊢\phi \to \left(Z=A\underset{\dot{}}{\bullet }X\leftrightarrow \forall i\in IZ\left(i\right)=A\underset{\dot{}}{·}X\left(i\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		frlmplusgvalb.f	$$⊢F=R\mathrm{freeLMod}I$$
2		frlmplusgvalb.b	$$⊢B={\mathrm{Base}}_F$$
3		frlmplusgvalb.i	$$⊢\phi \to I\in W$$
4		frlmplusgvalb.x	$$⊢\phi \to X\in B$$
5		frlmplusgvalb.z	$$⊢\phi \to Z\in B$$
6		frlmplusgvalb.r	$$⊢\phi \to R\in \mathrm{Ring}$$
7		frlmvscavalb.k	$$⊢K={\mathrm{Base}}_R$$
8		frlmvscavalb.a	$$⊢\phi \to A\in K$$
9		frlmvscavalb.v	$$⊢\underset{\dot{}}{\bullet }={\cdot }_F$$
10		frlmvscavalb.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
11	1 7 2	frlmbasmap	$$⊢\left(I\in W\wedge Z\in B\right)\to Z\in \left(K^I\right)$$
12	3 5 11	syl2anc	$$⊢\phi \to Z\in \left(K^I\right)$$
13	7	fvexi	$$⊢K\in \mathrm{V}$$
14	13	a1i	$$⊢\phi \to K\in \mathrm{V}$$
15	14 3	elmapd	$$⊢\phi \to \left(Z\in \left(K^I\right)\leftrightarrow Z:I⟶K\right)$$
16	12 15	mpbid	$$⊢\phi \to Z:I⟶K$$
17	16	ffnd	$$⊢\phi \to ZFnI$$
18	1	frlmlmod	$$⊢\left(R\in \mathrm{Ring}\wedge I\in W\right)\to F\in \mathrm{LMod}$$
19	6 3 18	syl2anc	$$⊢\phi \to F\in \mathrm{LMod}$$
20	8 7	eleqtrdi	$$⊢\phi \to A\in {\mathrm{Base}}_R$$
21	1	frlmsca	$$⊢\left(R\in \mathrm{Ring}\wedge I\in W\right)\to R=\mathrm{Scalar}\left(F\right)$$
22	6 3 21	syl2anc	$$⊢\phi \to R=\mathrm{Scalar}\left(F\right)$$
23	22	fveq2d	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{Scalar}\left(F\right)}$$
24	20 23	eleqtrd	$$⊢\phi \to A\in {\mathrm{Base}}_{\mathrm{Scalar}\left(F\right)}$$
25		eqid	$$⊢\mathrm{Scalar}\left(F\right)=\mathrm{Scalar}\left(F\right)$$
26		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(F\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(F\right)}$$
27	2 25 9 26	lmodvscl	$$⊢\left(F\in \mathrm{LMod}\wedge A\in {\mathrm{Base}}_{\mathrm{Scalar}\left(F\right)}\wedge X\in B\right)\to A\underset{\dot{}}{\bullet }X\in B$$
28	19 24 4 27	syl3anc	$$⊢\phi \to A\underset{\dot{}}{\bullet }X\in B$$
29	1 7 2	frlmbasmap	$$⊢\left(I\in W\wedge A\underset{\dot{}}{\bullet }X\in B\right)\to A\underset{\dot{}}{\bullet }X\in \left(K^I\right)$$
30	3 28 29	syl2anc	$$⊢\phi \to A\underset{\dot{}}{\bullet }X\in \left(K^I\right)$$
31	14 3	elmapd	$$⊢\phi \to \left(A\underset{\dot{}}{\bullet }X\in \left(K^I\right)\leftrightarrow \left(A\underset{\dot{}}{\bullet }X\right):I⟶K\right)$$
32	30 31	mpbid	$$⊢\phi \to \left(A\underset{\dot{}}{\bullet }X\right):I⟶K$$
33	32	ffnd	$$⊢\phi \to \left(A\underset{\dot{}}{\bullet }X\right)FnI$$
34		eqfnfv	$$⊢\left(ZFnI\wedge \left(A\underset{\dot{}}{\bullet }X\right)FnI\right)\to \left(Z=A\underset{\dot{}}{\bullet }X\leftrightarrow \forall i\in IZ\left(i\right)=\left(A\underset{\dot{}}{\bullet }X\right)\left(i\right)\right)$$
35	17 33 34	syl2anc	$$⊢\phi \to \left(Z=A\underset{\dot{}}{\bullet }X\leftrightarrow \forall i\in IZ\left(i\right)=\left(A\underset{\dot{}}{\bullet }X\right)\left(i\right)\right)$$
36	3	adantr	$$⊢\left(\phi \wedge i\in I\right)\to I\in W$$
37	8	adantr	$$⊢\left(\phi \wedge i\in I\right)\to A\in K$$
38	4	adantr	$$⊢\left(\phi \wedge i\in I\right)\to X\in B$$
39		simpr	$$⊢\left(\phi \wedge i\in I\right)\to i\in I$$
40	1 2 7 36 37 38 39 9 10	frlmvscaval	$$⊢\left(\phi \wedge i\in I\right)\to \left(A\underset{\dot{}}{\bullet }X\right)\left(i\right)=A\underset{\dot{}}{·}X\left(i\right)$$
41	40	eqeq2d	$$⊢\left(\phi \wedge i\in I\right)\to \left(Z\left(i\right)=\left(A\underset{\dot{}}{\bullet }X\right)\left(i\right)\leftrightarrow Z\left(i\right)=A\underset{\dot{}}{·}X\left(i\right)\right)$$
42	41	ralbidva	$$⊢\phi \to \left(\forall i\in IZ\left(i\right)=\left(A\underset{\dot{}}{\bullet }X\right)\left(i\right)\leftrightarrow \forall i\in IZ\left(i\right)=A\underset{\dot{}}{·}X\left(i\right)\right)$$
43	35 42	bitrd	$$⊢\phi \to \left(Z=A\underset{\dot{}}{\bullet }X\leftrightarrow \forall i\in IZ\left(i\right)=A\underset{\dot{}}{·}X\left(i\right)\right)$$