This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝑍 = ( 𝑋 ✚ 𝑌 ) ↔ ∀ 𝑖 ∈ 𝐼 ( 𝑍 ‘ 𝑖 ) = ( ( 𝑋 ‘ 𝑖 ) + ( 𝑌 ‘ 𝑖 ) ) ) )