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

Metamath Proof Explorer

Theorem frlmvplusgvalc

Description: Coordinates of a sum with respect to a basis in a free module. (Contributed by AV, 16-Jan-2023)

Ref Expression
Hypotheses frlmvplusgvalc.f ⊢ F = R freeLMod I
frlmvplusgvalc.b ⊢ B = Base F
frlmvplusgvalc.r ⊢ φ → R ∈ V
frlmvplusgvalc.i ⊢ φ → I ∈ W
frlmvplusgvalc.x ⊢ φ → X ∈ B
frlmvplusgvalc.y ⊢ φ → Y ∈ B
frlmvplusgvalc.j ⊢ φ → J ∈ I
frlmvplusgvalc.a ⊢ + ˙ = + R
frlmvplusgvalc.p ⊢ ✚ ˙ = + F
Assertion frlmvplusgvalc ⊢ φ → X ✚ ˙ Y ⁡ J = X ⁡ J + ˙ Y ⁡ J

Proof

Step Hyp Ref Expression
1 frlmvplusgvalc.f ⊢ F = R freeLMod I
2 frlmvplusgvalc.b ⊢ B = Base F
3 frlmvplusgvalc.r ⊢ φ → R ∈ V
4 frlmvplusgvalc.i ⊢ φ → I ∈ W
5 frlmvplusgvalc.x ⊢ φ → X ∈ B
6 frlmvplusgvalc.y ⊢ φ → Y ∈ B
7 frlmvplusgvalc.j ⊢ φ → J ∈ I
8 frlmvplusgvalc.a ⊢ + ˙ = + R
9 frlmvplusgvalc.p ⊢ ✚ ˙ = + F
10 1 2 3 4 5 6 8 9 frlmplusgval ⊢ φ → X ✚ ˙ Y = X + ˙ f Y
11 10 fveq1d ⊢ φ → X ✚ ˙ Y ⁡ J = X + ˙ f Y ⁡ J
12 eqid ⊢ Base R = Base R
13 1 12 2 frlmbasmap ⊢ I ∈ W ∧ X ∈ B → X ∈ Base R I
14 4 5 13 syl2anc ⊢ φ → X ∈ Base R I
15 fvexd ⊢ φ → Base R ∈ V
16 15 4 elmapd ⊢ φ → X ∈ Base R I ↔ X : I ⟶ Base R
17 14 16 mpbid ⊢ φ → X : I ⟶ Base R
18 17 ffnd ⊢ φ → X Fn I
19 1 12 2 frlmbasmap ⊢ I ∈ W ∧ Y ∈ B → Y ∈ Base R I
20 4 6 19 syl2anc ⊢ φ → Y ∈ Base R I
21 15 4 elmapd ⊢ φ → Y ∈ Base R I ↔ Y : I ⟶ Base R
22 20 21 mpbid ⊢ φ → Y : I ⟶ Base R
23 22 ffnd ⊢ φ → Y Fn I
24 fnfvof ⊢ X Fn I ∧ Y Fn I ∧ I ∈ W ∧ J ∈ I → X + ˙ f Y ⁡ J = X ⁡ J + ˙ Y ⁡ J
25 18 23 4 7 24 syl22anc ⊢ φ → X + ˙ f Y ⁡ J = X ⁡ J + ˙ Y ⁡ J
26 11 25 eqtrd ⊢ φ → X ✚ ˙ Y ⁡ J = X ⁡ J + ˙ Y ⁡ J