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

Metamath Proof Explorer

Theorem frlmfzowrdb

Proof