lmisfree

Description: A module has a basis iff it is isomorphic to a free module. In settings where isomorphic objects are not distinguished, it is common to define "free module" as any module with a basis; thus for instance lbsex might be described as "every vector space is free". (Contributed by Stefan O'Rear, 26-Feb-2015)

	Ref	Expression
Hypotheses	lmisfree.j	$⊢ J = LBasis (W)$
	lmisfree.f	$⊢ F = Scalar (W)$
Assertion	lmisfree	$⊢ W \in LMod \to (J \neq \emptyset \leftrightarrow \exists k W ≃_{𝑚} (F freeLMod k))$

Proof

Step	Hyp	Ref	Expression
1		lmisfree.j	$⊢ J = LBasis (W)$
2		lmisfree.f	$⊢ F = Scalar (W)$
3		n0	$⊢ J \neq \emptyset \leftrightarrow \exists j j \in J$
4		vex	$⊢ j \in V$
5	4	enref	$⊢ j \approx j$
6	2 1	lbslcic	$⊢ (W \in LMod \land j \in J \land j \approx j) \to W ≃_{𝑚} (F freeLMod j)$
7	5 6	mp3an3	$⊢ (W \in LMod \land j \in J) \to W ≃_{𝑚} (F freeLMod j)$
8		oveq2	$⊢ k = j \to F freeLMod k = F freeLMod j$
9	8	breq2d	$⊢ k = j \to (W ≃_{𝑚} (F freeLMod k) \leftrightarrow W ≃_{𝑚} (F freeLMod j))$
10	4 9	spcev	$⊢ W ≃_{𝑚} (F freeLMod j) \to \exists k W ≃_{𝑚} (F freeLMod k)$
11	7 10	syl	$⊢ (W \in LMod \land j \in J) \to \exists k W ≃_{𝑚} (F freeLMod k)$
12	11	ex	$⊢ W \in LMod \to (j \in J \to \exists k W ≃_{𝑚} (F freeLMod k))$
13	12	exlimdv	$⊢ W \in LMod \to (\exists j j \in J \to \exists k W ≃_{𝑚} (F freeLMod k))$
14	3 13	biimtrid	$⊢ W \in LMod \to (J \neq \emptyset \to \exists k W ≃_{𝑚} (F freeLMod k))$
15		lmicsym	$⊢ W ≃_{𝑚} (F freeLMod k) \to (F freeLMod k) ≃_{𝑚} W$
16		lmiclcl	$⊢ W ≃_{𝑚} (F freeLMod k) \to W \in LMod$
17	2	lmodring	$⊢ W \in LMod \to F \in Ring$
18		vex	$⊢ k \in V$
19		eqid	$⊢ F freeLMod k = F freeLMod k$
20		eqid	$⊢ F unitVec k = F unitVec k$
21		eqid	$⊢ LBasis (F freeLMod k) = LBasis (F freeLMod k)$
22	19 20 21	frlmlbs	$⊢ (F \in Ring \land k \in V) \to ran (F unitVec k) \in LBasis (F freeLMod k)$
23	17 18 22	sylancl	$⊢ W \in LMod \to ran (F unitVec k) \in LBasis (F freeLMod k)$
24	23	ne0d	$⊢ W \in LMod \to LBasis (F freeLMod k) \neq \emptyset$
25	16 24	syl	$⊢ W ≃_{𝑚} (F freeLMod k) \to LBasis (F freeLMod k) \neq \emptyset$
26	21 1	lmiclbs	$⊢ (F freeLMod k) ≃_{𝑚} W \to (LBasis (F freeLMod k) \neq \emptyset \to J \neq \emptyset)$
27	15 25 26	sylc	$⊢ W ≃_{𝑚} (F freeLMod k) \to J \neq \emptyset$
28	27	exlimiv	$⊢ \exists k W ≃_{𝑚} (F freeLMod k) \to J \neq \emptyset$
29	14 28	impbid1	$⊢ W \in LMod \to (J \neq \emptyset \leftrightarrow \exists k W ≃_{𝑚} (F freeLMod k))$

Metamath Proof Explorer

Theorem lmisfree

Proof