Theorem frlmplusgvalb

Description: Addition 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 )
	frlmplusgvalb.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	frlmplusgvalb.a	⊢ + = ( +g ‘ 𝑅 )
	frlmplusgvalb.p	⊢ ✚ = ( +g ‘ 𝐹 )
Assertion	frlmplusgvalb	⊢ ( 𝜑 → ( 𝑍 = ( 𝑋 ✚ 𝑌 ) ↔ ∀ 𝑖 ∈ 𝐼 ( 𝑍 ‘ 𝑖 ) = ( ( 𝑋 ‘ 𝑖 ) + ( 𝑌 ‘ 𝑖 ) ) ) )

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		frlmplusgvalb.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
8		frlmplusgvalb.a	⊢ + = ( +g ‘ 𝑅 )
9		frlmplusgvalb.p	⊢ ✚ = ( +g ‘ 𝐹 )
10		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
11	1 10 2	frlmbasmap	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑍 ∈ 𝐵 ) → 𝑍 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) )
12	3 5 11	syl2anc	⊢ ( 𝜑 → 𝑍 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) )
13		fvexd	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) ∈ V )
14	13 3	elmapd	⊢ ( 𝜑 → ( 𝑍 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ↔ 𝑍 : 𝐼 ⟶ ( Base ‘ 𝑅 ) ) )
15	12 14	mpbid	⊢ ( 𝜑 → 𝑍 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
16	15	ffnd	⊢ ( 𝜑 → 𝑍 Fn 𝐼 )
17	1	frlmlmod	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → 𝐹 ∈ LMod )
18	6 3 17	syl2anc	⊢ ( 𝜑 → 𝐹 ∈ LMod )
19		lmodgrp	⊢ ( 𝐹 ∈ LMod → 𝐹 ∈ Grp )
20	18 19	syl	⊢ ( 𝜑 → 𝐹 ∈ Grp )
21	2 9	grpcl	⊢ ( ( 𝐹 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ✚ 𝑌 ) ∈ 𝐵 )
22	20 4 7 21	syl3anc	⊢ ( 𝜑 → ( 𝑋 ✚ 𝑌 ) ∈ 𝐵 )
23	1 10 2	frlmbasmap	⊢ ( ( 𝐼 ∈ 𝑊 ∧ ( 𝑋 ✚ 𝑌 ) ∈ 𝐵 ) → ( 𝑋 ✚ 𝑌 ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) )
24	3 22 23	syl2anc	⊢ ( 𝜑 → ( 𝑋 ✚ 𝑌 ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) )
25	13 3	elmapd	⊢ ( 𝜑 → ( ( 𝑋 ✚ 𝑌 ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ↔ ( 𝑋 ✚ 𝑌 ) : 𝐼 ⟶ ( Base ‘ 𝑅 ) ) )
26	24 25	mpbid	⊢ ( 𝜑 → ( 𝑋 ✚ 𝑌 ) : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
27	26	ffnd	⊢ ( 𝜑 → ( 𝑋 ✚ 𝑌 ) Fn 𝐼 )
28		eqfnfv	⊢ ( ( 𝑍 Fn 𝐼 ∧ ( 𝑋 ✚ 𝑌 ) Fn 𝐼 ) → ( 𝑍 = ( 𝑋 ✚ 𝑌 ) ↔ ∀ 𝑖 ∈ 𝐼 ( 𝑍 ‘ 𝑖 ) = ( ( 𝑋 ✚ 𝑌 ) ‘ 𝑖 ) ) )
29	16 27 28	syl2anc	⊢ ( 𝜑 → ( 𝑍 = ( 𝑋 ✚ 𝑌 ) ↔ ∀ 𝑖 ∈ 𝐼 ( 𝑍 ‘ 𝑖 ) = ( ( 𝑋 ✚ 𝑌 ) ‘ 𝑖 ) ) )
30	6	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 𝑅 ∈ Ring )
31	3	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 𝐼 ∈ 𝑊 )
32	4	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 𝑋 ∈ 𝐵 )
33	7	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 𝑌 ∈ 𝐵 )
34		simpr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 𝑖 ∈ 𝐼 )
35	1 2 30 31 32 33 34 8 9	frlmvplusgvalc	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑋 ✚ 𝑌 ) ‘ 𝑖 ) = ( ( 𝑋 ‘ 𝑖 ) + ( 𝑌 ‘ 𝑖 ) ) )
36	35	eqeq2d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑍 ‘ 𝑖 ) = ( ( 𝑋 ✚ 𝑌 ) ‘ 𝑖 ) ↔ ( 𝑍 ‘ 𝑖 ) = ( ( 𝑋 ‘ 𝑖 ) + ( 𝑌 ‘ 𝑖 ) ) ) )
37	36	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑖 ∈ 𝐼 ( 𝑍 ‘ 𝑖 ) = ( ( 𝑋 ✚ 𝑌 ) ‘ 𝑖 ) ↔ ∀ 𝑖 ∈ 𝐼 ( 𝑍 ‘ 𝑖 ) = ( ( 𝑋 ‘ 𝑖 ) + ( 𝑌 ‘ 𝑖 ) ) ) )
38	29 37	bitrd	⊢ ( 𝜑 → ( 𝑍 = ( 𝑋 ✚ 𝑌 ) ↔ ∀ 𝑖 ∈ 𝐼 ( 𝑍 ‘ 𝑖 ) = ( ( 𝑋 ‘ 𝑖 ) + ( 𝑌 ‘ 𝑖 ) ) ) )