Metamath Proof Explorer


Theorem frlmfzowrdb

Description: The vectors of a module with indices 0 to N - 1 are the length- N words over the scalars of the module. (Contributed by SN, 1-Sep-2023)

Ref Expression
Hypotheses frlmfzowrd.w W = K freeLMod 0 ..^ N
frlmfzowrd.b B = Base W
frlmfzowrd.s S = Base K
Assertion frlmfzowrdb K V N 0 X B X Word S X = N

Proof

Step Hyp Ref Expression
1 frlmfzowrd.w W = K freeLMod 0 ..^ N
2 frlmfzowrd.b B = Base W
3 frlmfzowrd.s S = Base K
4 1 2 3 frlmfzowrd X B X Word S
5 4 a1i K V N 0 X B X Word S
6 1 2 3 frlmfzolen N 0 X B X = N
7 6 ex N 0 X B X = N
8 7 adantl K V N 0 X B X = N
9 5 8 jcad K V N 0 X B X Word S X = N
10 simp3l K V N 0 X Word S X = N X Word S
11 wrdf X Word S X : 0 ..^ X S
12 10 11 syl K V N 0 X Word S X = N X : 0 ..^ X S
13 simp3r K V N 0 X Word S X = N X = N
14 13 oveq2d K V N 0 X Word S X = N 0 ..^ X = 0 ..^ N
15 14 feq2d K V N 0 X Word S X = N X : 0 ..^ X S X : 0 ..^ N S
16 12 15 mpbid K V N 0 X Word S X = N X : 0 ..^ N S
17 simp1 K V N 0 X Word S X = N K V
18 fzofi 0 ..^ N Fin
19 1 3 2 frlmfielbas K V 0 ..^ N Fin X B X : 0 ..^ N S
20 17 18 19 sylancl K V N 0 X Word S X = N X B X : 0 ..^ N S
21 16 20 mpbird K V N 0 X Word S X = N X B
22 21 3expia K V N 0 X Word S X = N X B
23 9 22 impbid K V N 0 X B X Word S X = N