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 e. V /\ N e. NN0 ) -> ( X e. B <-> ( X e. 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 e. B -> X e. Word S )
5 4 a1i 
 |-  ( ( K e. V /\ N e. NN0 ) -> ( X e. B -> X e. Word S ) )
6 1 2 3 frlmfzolen 
 |-  ( ( N e. NN0 /\ X e. B ) -> ( # ` X ) = N )
7 6 ex 
 |-  ( N e. NN0 -> ( X e. B -> ( # ` X ) = N ) )
8 7 adantl 
 |-  ( ( K e. V /\ N e. NN0 ) -> ( X e. B -> ( # ` X ) = N ) )
9 5 8 jcad 
 |-  ( ( K e. V /\ N e. NN0 ) -> ( X e. B -> ( X e. Word S /\ ( # ` X ) = N ) ) )
10 simp3l 
 |-  ( ( K e. V /\ N e. NN0 /\ ( X e. Word S /\ ( # ` X ) = N ) ) -> X e. Word S )
11 wrdf 
 |-  ( X e. Word S -> X : ( 0 ..^ ( # ` X ) ) --> S )
12 10 11 syl 
 |-  ( ( K e. V /\ N e. NN0 /\ ( X e. Word S /\ ( # ` X ) = N ) ) -> X : ( 0 ..^ ( # ` X ) ) --> S )
13 simp3r 
 |-  ( ( K e. V /\ N e. NN0 /\ ( X e. Word S /\ ( # ` X ) = N ) ) -> ( # ` X ) = N )
14 13 oveq2d 
 |-  ( ( K e. V /\ N e. NN0 /\ ( X e. Word S /\ ( # ` X ) = N ) ) -> ( 0 ..^ ( # ` X ) ) = ( 0 ..^ N ) )
15 14 feq2d 
 |-  ( ( K e. V /\ N e. NN0 /\ ( X e. Word S /\ ( # ` X ) = N ) ) -> ( X : ( 0 ..^ ( # ` X ) ) --> S <-> X : ( 0 ..^ N ) --> S ) )
16 12 15 mpbid 
 |-  ( ( K e. V /\ N e. NN0 /\ ( X e. Word S /\ ( # ` X ) = N ) ) -> X : ( 0 ..^ N ) --> S )
17 simp1 
 |-  ( ( K e. V /\ N e. NN0 /\ ( X e. Word S /\ ( # ` X ) = N ) ) -> K e. V )
18 fzofi 
 |-  ( 0 ..^ N ) e. Fin
19 1 3 2 frlmfielbas 
 |-  ( ( K e. V /\ ( 0 ..^ N ) e. Fin ) -> ( X e. B <-> X : ( 0 ..^ N ) --> S ) )
20 17 18 19 sylancl 
 |-  ( ( K e. V /\ N e. NN0 /\ ( X e. Word S /\ ( # ` X ) = N ) ) -> ( X e. B <-> X : ( 0 ..^ N ) --> S ) )
21 16 20 mpbird 
 |-  ( ( K e. V /\ N e. NN0 /\ ( X e. Word S /\ ( # ` X ) = N ) ) -> X e. B )
22 21 3expia 
 |-  ( ( K e. V /\ N e. NN0 ) -> ( ( X e. Word S /\ ( # ` X ) = N ) -> X e. B ) )
23 9 22 impbid 
 |-  ( ( K e. V /\ N e. NN0 ) -> ( X e. B <-> ( X e. Word S /\ ( # ` X ) = N ) ) )