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

Metamath Proof Explorer

Theorem frlmvscaval

Description: Coordinates of a scalar multiple with respect to a basis in a free module. (Contributed by Stefan O'Rear, 3-Feb-2015)

Ref Expression
Hypotheses frlmvscaval.y ⊢ Y = R freeLMod I
frlmvscaval.b ⊢ B = Base Y
frlmvscaval.k ⊢ K = Base R
frlmvscaval.i ⊢ φ → I ∈ W
frlmvscaval.a ⊢ φ → A ∈ K
frlmvscaval.x ⊢ φ → X ∈ B
frlmvscaval.j ⊢ φ → J ∈ I
frlmvscaval.v ⊢ ∙ ˙ = ⋅ Y
frlmvscaval.t ⊢ · ˙ = ⋅ R
Assertion frlmvscaval ⊢ φ → A ∙ ˙ X ⁡ J = A · ˙ X ⁡ J

Proof

Step Hyp Ref Expression
1 frlmvscaval.y ⊢ Y = R freeLMod I
2 frlmvscaval.b ⊢ B = Base Y
3 frlmvscaval.k ⊢ K = Base R
4 frlmvscaval.i ⊢ φ → I ∈ W
5 frlmvscaval.a ⊢ φ → A ∈ K
6 frlmvscaval.x ⊢ φ → X ∈ B
7 frlmvscaval.j ⊢ φ → J ∈ I
8 frlmvscaval.v ⊢ ∙ ˙ = ⋅ Y
9 frlmvscaval.t ⊢ · ˙ = ⋅ R
10 1 2 3 4 5 6 8 9 frlmvscafval ⊢ φ → A ∙ ˙ X = I × A · ˙ f X
11 10 fveq1d ⊢ φ → A ∙ ˙ X ⁡ J = I × A · ˙ f X ⁡ J
12 fnconstg ⊢ A ∈ K → I × A Fn I
13 5 12 syl ⊢ φ → I × A Fn I
14 1 3 2 frlmbasf ⊢ I ∈ W ∧ X ∈ B → X : I ⟶ K
15 4 6 14 syl2anc ⊢ φ → X : I ⟶ K
16 15 ffnd ⊢ φ → X Fn I
17 fnfvof ⊢ I × A Fn I ∧ X Fn I ∧ I ∈ W ∧ J ∈ I → I × A · ˙ f X ⁡ J = I × A ⁡ J · ˙ X ⁡ J
18 13 16 4 7 17 syl22anc ⊢ φ → I × A · ˙ f X ⁡ J = I × A ⁡ J · ˙ X ⁡ J
19 fvconst2g ⊢ A ∈ K ∧ J ∈ I → I × A ⁡ J = A
20 5 7 19 syl2anc ⊢ φ → I × A ⁡ J = A
21 20 oveq1d ⊢ φ → I × A ⁡ J · ˙ X ⁡ J = A · ˙ X ⁡ J
22 11 18 21 3eqtrd ⊢ φ → A ∙ ˙ X ⁡ J = A · ˙ X ⁡ J