frlmplusgvalb

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

	Ref	Expression
Hypotheses	frlmplusgvalb.f	$⊢ F = R freeLMod I$
	frlmplusgvalb.b	$⊢ B = {Base}_{F}$
	frlmplusgvalb.i	$⊢ φ \to I \in W$
	frlmplusgvalb.x	$⊢ φ \to X \in B$
	frlmplusgvalb.z	$⊢ φ \to Z \in B$
	frlmplusgvalb.r	$⊢ φ \to R \in Ring$
	frlmplusgvalb.y	$⊢ φ \to Y \in B$
	frlmplusgvalb.a	$⊢ \underset{˙}{+} = +_{R}$
	frlmplusgvalb.p	$⊢ \underset{˙}{✚} = +_{F}$
Assertion	frlmplusgvalb	$⊢ φ \to (Z = X \underset{˙}{✚} Y \leftrightarrow \forall i \in I Z (i) = X (i) \underset{˙}{+} Y (i))$

Proof

Step	Hyp	Ref	Expression
1		frlmplusgvalb.f	$⊢ F = R freeLMod I$
2		frlmplusgvalb.b	$⊢ B = {Base}_{F}$
3		frlmplusgvalb.i	$⊢ φ \to I \in W$
4		frlmplusgvalb.x	$⊢ φ \to X \in B$
5		frlmplusgvalb.z	$⊢ φ \to Z \in B$
6		frlmplusgvalb.r	$⊢ φ \to R \in Ring$
7		frlmplusgvalb.y	$⊢ φ \to Y \in B$
8		frlmplusgvalb.a	$⊢ \underset{˙}{+} = +_{R}$
9		frlmplusgvalb.p	$⊢ \underset{˙}{✚} = +_{F}$
10		eqid	$⊢ {Base}_{R} = {Base}_{R}$
11	1 10 2	frlmbasmap	$⊢ (I \in W \land Z \in B) \to Z \in ({Base}_{R}^{I})$
12	3 5 11	syl2anc	$⊢ φ \to Z \in ({Base}_{R}^{I})$
13		fvexd	$⊢ φ \to {Base}_{R} \in V$
14	13 3	elmapd	$⊢ φ \to (Z \in ({Base}_{R}^{I}) \leftrightarrow Z : I ⟶ {Base}_{R})$
15	12 14	mpbid	$⊢ φ \to Z : I ⟶ {Base}_{R}$
16	15	ffnd	$⊢ φ \to Z Fn I$
17	1	frlmlmod	$⊢ (R \in Ring \land I \in W) \to F \in LMod$
18	6 3 17	syl2anc	$⊢ φ \to F \in LMod$
19		lmodgrp	$⊢ F \in LMod \to F \in Grp$
20	18 19	syl	$⊢ φ \to F \in Grp$
21	2 9	grpcl	$⊢ (F \in Grp \land X \in B \land Y \in B) \to X \underset{˙}{✚} Y \in B$
22	20 4 7 21	syl3anc	$⊢ φ \to X \underset{˙}{✚} Y \in B$
23	1 10 2	frlmbasmap	$⊢ (I \in W \land X \underset{˙}{✚} Y \in B) \to X \underset{˙}{✚} Y \in ({Base}_{R}^{I})$
24	3 22 23	syl2anc	$⊢ φ \to X \underset{˙}{✚} Y \in ({Base}_{R}^{I})$
25	13 3	elmapd	$⊢ φ \to (X \underset{˙}{✚} Y \in ({Base}_{R}^{I}) \leftrightarrow (X \underset{˙}{✚} Y) : I ⟶ {Base}_{R})$
26	24 25	mpbid	$⊢ φ \to (X \underset{˙}{✚} Y) : I ⟶ {Base}_{R}$
27	26	ffnd	$⊢ φ \to (X \underset{˙}{✚} Y) Fn I$
28		eqfnfv	$⊢ (Z Fn I \land (X \underset{˙}{✚} Y) Fn I) \to (Z = X \underset{˙}{✚} Y \leftrightarrow \forall i \in I Z (i) = (X \underset{˙}{✚} Y) (i))$
29	16 27 28	syl2anc	$⊢ φ \to (Z = X \underset{˙}{✚} Y \leftrightarrow \forall i \in I Z (i) = (X \underset{˙}{✚} Y) (i))$
30	6	adantr	$⊢ (φ \land i \in I) \to R \in Ring$
31	3	adantr	$⊢ (φ \land i \in I) \to I \in W$
32	4	adantr	$⊢ (φ \land i \in I) \to X \in B$
33	7	adantr	$⊢ (φ \land i \in I) \to Y \in B$
34		simpr	$⊢ (φ \land i \in I) \to i \in I$
35	1 2 30 31 32 33 34 8 9	frlmvplusgvalc	$⊢ (φ \land i \in I) \to (X \underset{˙}{✚} Y) (i) = X (i) \underset{˙}{+} Y (i)$
36	35	eqeq2d	$⊢ (φ \land i \in I) \to (Z (i) = (X \underset{˙}{✚} Y) (i) \leftrightarrow Z (i) = X (i) \underset{˙}{+} Y (i))$
37	36	ralbidva	$⊢ φ \to (\forall i \in I Z (i) = (X \underset{˙}{✚} Y) (i) \leftrightarrow \forall i \in I Z (i) = X (i) \underset{˙}{+} Y (i))$
38	29 37	bitrd	$⊢ φ \to (Z = X \underset{˙}{✚} Y \leftrightarrow \forall i \in I Z (i) = X (i) \underset{˙}{+} Y (i))$

Metamath Proof Explorer

Theorem frlmplusgvalb

Proof