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

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 ⊢ 𝑊 = ( 𝐾 freeLMod ( 0 ..^ 𝑁 ) )
frlmfzowrd.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
frlmfzowrd.s ⊢ 𝑆 = ( Base ‘ 𝐾 )
Assertion frlmfzowrdb ( ( 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑋 ∈ 𝐵 ↔ ( 𝑋 ∈ Word 𝑆 ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 frlmfzowrd.w ⊢ 𝑊 = ( 𝐾 freeLMod ( 0 ..^ 𝑁 ) )
2 frlmfzowrd.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
3 frlmfzowrd.s ⊢ 𝑆 = ( Base ‘ 𝐾 )
4 1 2 3 frlmfzowrd ⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ Word 𝑆 )
5 4 a1i ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑋 ∈ 𝐵 → 𝑋 ∈ Word 𝑆 ) )
6 1 2 3 frlmfzolen ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( ♯ ‘ 𝑋 ) = 𝑁 )
7 6 ex ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑋 ∈ 𝐵 → ( ♯ ‘ 𝑋 ) = 𝑁 ) )
8 7 adantl ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑋 ∈ 𝐵 → ( ♯ ‘ 𝑋 ) = 𝑁 ) )
9 5 8 jcad ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑋 ∈ 𝐵 → ( 𝑋 ∈ Word 𝑆 ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ) )
10 simp3l ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑋 ∈ Word 𝑆 ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ) → 𝑋 ∈ Word 𝑆 )
11 wrdf ⊢ ( 𝑋 ∈ Word 𝑆 → 𝑋 : ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ⟶ 𝑆 )
12 10 11 syl ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑋 ∈ Word 𝑆 ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ) → 𝑋 : ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ⟶ 𝑆 )
13 simp3r ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑋 ∈ Word 𝑆 ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ) → ( ♯ ‘ 𝑋 ) = 𝑁 )
14 13 oveq2d ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑋 ∈ Word 𝑆 ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ) → ( 0 ..^ ( ♯ ‘ 𝑋 ) ) = ( 0 ..^ 𝑁 ) )
15 14 feq2d ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑋 ∈ Word 𝑆 ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ) → ( 𝑋 : ( 0 ..^ ( ♯ ‘ 𝑋 ) ) ⟶ 𝑆 ↔ 𝑋 : ( 0 ..^ 𝑁 ) ⟶ 𝑆 ) )
16 12 15 mpbid ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑋 ∈ Word 𝑆 ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ) → 𝑋 : ( 0 ..^ 𝑁 ) ⟶ 𝑆 )
17 simp1 ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑋 ∈ Word 𝑆 ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ) → 𝐾 ∈ 𝑉 )
18 fzofi ⊢ ( 0 ..^ 𝑁 ) ∈ Fin
19 1 3 2 frlmfielbas ⊢ ( ( 𝐾 ∈ 𝑉 ∧ ( 0 ..^ 𝑁 ) ∈ Fin ) → ( 𝑋 ∈ 𝐵 ↔ 𝑋 : ( 0 ..^ 𝑁 ) ⟶ 𝑆 ) )
20 17 18 19 sylancl ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑋 ∈ Word 𝑆 ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ) → ( 𝑋 ∈ 𝐵 ↔ 𝑋 : ( 0 ..^ 𝑁 ) ⟶ 𝑆 ) )
21 16 20 mpbird ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑋 ∈ Word 𝑆 ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ) → 𝑋 ∈ 𝐵 )
22 21 3expia ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑋 ∈ Word 𝑆 ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) → 𝑋 ∈ 𝐵 ) )
23 9 22 impbid ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑋 ∈ 𝐵 ↔ ( 𝑋 ∈ Word 𝑆 ∧ ( ♯ ‘ 𝑋 ) = 𝑁 ) ) )