Theorem frlmvscavalb

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

	Ref	Expression
Hypotheses	frlmplusgvalb.f	⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
	frlmplusgvalb.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
	frlmplusgvalb.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	frlmplusgvalb.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	frlmplusgvalb.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
	frlmplusgvalb.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	frlmvscavalb.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	frlmvscavalb.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
	frlmvscavalb.v	⊢ ∙ = ( ·𝑠 ‘ 𝐹 )
	frlmvscavalb.t	⊢ · = ( .r ‘ 𝑅 )
Assertion	frlmvscavalb	⊢ ( 𝜑 → ( 𝑍 = ( 𝐴 ∙ 𝑋 ) ↔ ∀ 𝑖 ∈ 𝐼 ( 𝑍 ‘ 𝑖 ) = ( 𝐴 · ( 𝑋 ‘ 𝑖 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		frlmplusgvalb.f	⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
2		frlmplusgvalb.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
3		frlmplusgvalb.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
4		frlmplusgvalb.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		frlmplusgvalb.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
6		frlmplusgvalb.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
7		frlmvscavalb.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
8		frlmvscavalb.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
9		frlmvscavalb.v	⊢ ∙ = ( ·𝑠 ‘ 𝐹 )
10		frlmvscavalb.t	⊢ · = ( .r ‘ 𝑅 )
11	1 7 2	frlmbasmap	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑍 ∈ 𝐵 ) → 𝑍 ∈ ( 𝐾 ↑m 𝐼 ) )
12	3 5 11	syl2anc	⊢ ( 𝜑 → 𝑍 ∈ ( 𝐾 ↑m 𝐼 ) )
13	7	fvexi	⊢ 𝐾 ∈ V
14	13	a1i	⊢ ( 𝜑 → 𝐾 ∈ V )
15	14 3	elmapd	⊢ ( 𝜑 → ( 𝑍 ∈ ( 𝐾 ↑m 𝐼 ) ↔ 𝑍 : 𝐼 ⟶ 𝐾 ) )
16	12 15	mpbid	⊢ ( 𝜑 → 𝑍 : 𝐼 ⟶ 𝐾 )
17	16	ffnd	⊢ ( 𝜑 → 𝑍 Fn 𝐼 )
18	1	frlmlmod	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → 𝐹 ∈ LMod )
19	6 3 18	syl2anc	⊢ ( 𝜑 → 𝐹 ∈ LMod )
20	8 7	eleqtrdi	⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ 𝑅 ) )
21	1	frlmsca	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → 𝑅 = ( Scalar ‘ 𝐹 ) )
22	6 3 21	syl2anc	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝐹 ) )
23	22	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝐹 ) ) )
24	20 23	eleqtrd	⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) )
25		eqid	⊢ ( Scalar ‘ 𝐹 ) = ( Scalar ‘ 𝐹 )
26		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝐹 ) ) = ( Base ‘ ( Scalar ‘ 𝐹 ) )
27	2 25 9 26	lmodvscl	⊢ ( ( 𝐹 ∈ LMod ∧ 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐴 ∙ 𝑋 ) ∈ 𝐵 )
28	19 24 4 27	syl3anc	⊢ ( 𝜑 → ( 𝐴 ∙ 𝑋 ) ∈ 𝐵 )
29	1 7 2	frlmbasmap	⊢ ( ( 𝐼 ∈ 𝑊 ∧ ( 𝐴 ∙ 𝑋 ) ∈ 𝐵 ) → ( 𝐴 ∙ 𝑋 ) ∈ ( 𝐾 ↑m 𝐼 ) )
30	3 28 29	syl2anc	⊢ ( 𝜑 → ( 𝐴 ∙ 𝑋 ) ∈ ( 𝐾 ↑m 𝐼 ) )
31	14 3	elmapd	⊢ ( 𝜑 → ( ( 𝐴 ∙ 𝑋 ) ∈ ( 𝐾 ↑m 𝐼 ) ↔ ( 𝐴 ∙ 𝑋 ) : 𝐼 ⟶ 𝐾 ) )
32	30 31	mpbid	⊢ ( 𝜑 → ( 𝐴 ∙ 𝑋 ) : 𝐼 ⟶ 𝐾 )
33	32	ffnd	⊢ ( 𝜑 → ( 𝐴 ∙ 𝑋 ) Fn 𝐼 )
34		eqfnfv	⊢ ( ( 𝑍 Fn 𝐼 ∧ ( 𝐴 ∙ 𝑋 ) Fn 𝐼 ) → ( 𝑍 = ( 𝐴 ∙ 𝑋 ) ↔ ∀ 𝑖 ∈ 𝐼 ( 𝑍 ‘ 𝑖 ) = ( ( 𝐴 ∙ 𝑋 ) ‘ 𝑖 ) ) )
35	17 33 34	syl2anc	⊢ ( 𝜑 → ( 𝑍 = ( 𝐴 ∙ 𝑋 ) ↔ ∀ 𝑖 ∈ 𝐼 ( 𝑍 ‘ 𝑖 ) = ( ( 𝐴 ∙ 𝑋 ) ‘ 𝑖 ) ) )
36	3	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 𝐼 ∈ 𝑊 )
37	8	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 𝐴 ∈ 𝐾 )
38	4	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 𝑋 ∈ 𝐵 )
39		simpr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 𝑖 ∈ 𝐼 )
40	1 2 7 36 37 38 39 9 10	frlmvscaval	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝐴 ∙ 𝑋 ) ‘ 𝑖 ) = ( 𝐴 · ( 𝑋 ‘ 𝑖 ) ) )
41	40	eqeq2d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑍 ‘ 𝑖 ) = ( ( 𝐴 ∙ 𝑋 ) ‘ 𝑖 ) ↔ ( 𝑍 ‘ 𝑖 ) = ( 𝐴 · ( 𝑋 ‘ 𝑖 ) ) ) )
42	41	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑖 ∈ 𝐼 ( 𝑍 ‘ 𝑖 ) = ( ( 𝐴 ∙ 𝑋 ) ‘ 𝑖 ) ↔ ∀ 𝑖 ∈ 𝐼 ( 𝑍 ‘ 𝑖 ) = ( 𝐴 · ( 𝑋 ‘ 𝑖 ) ) ) )
43	35 42	bitrd	⊢ ( 𝜑 → ( 𝑍 = ( 𝐴 ∙ 𝑋 ) ↔ ∀ 𝑖 ∈ 𝐼 ( 𝑍 ‘ 𝑖 ) = ( 𝐴 · ( 𝑋 ‘ 𝑖 ) ) ) )