lbslcic

Description: A module with a basis is isomorphic to a free module with the same cardinality. (Contributed by Stefan O'Rear, 26-Feb-2015)

	Ref	Expression
Hypotheses	lbslcic.f	$⊢ F = Scalar (W)$
	lbslcic.j	$⊢ J = LBasis (W)$
Assertion	lbslcic	$⊢ (W \in LMod \land B \in J \land I \approx B) \to W ≃_{𝑚} (F freeLMod I)$

Proof

Step	Hyp	Ref	Expression
1		lbslcic.f	$⊢ F = Scalar (W)$
2		lbslcic.j	$⊢ J = LBasis (W)$
3		simp3	$⊢ (W \in LMod \land B \in J \land I \approx B) \to I \approx B$
4		bren	$⊢ I \approx B \leftrightarrow \exists e e : I \underset{1-1 onto}{⟶} B$
5	3 4	sylib	$⊢ (W \in LMod \land B \in J \land I \approx B) \to \exists e e : I \underset{1-1 onto}{⟶} B$
6		eqid	$⊢ F freeLMod I = F freeLMod I$
7		eqid	$⊢ {Base}_{(F freeLMod I)} = {Base}_{(F freeLMod I)}$
8		eqid	$⊢ {Base}_{W} = {Base}_{W}$
9		eqid	$⊢ \cdot_{W} = \cdot_{W}$
10		eqid	$⊢ LSpan (W) = LSpan (W)$
11		eqid	$⊢ (x \in {Base}_{(F freeLMod I)} ⟼ \sum_{W} (x {\cdot_{W}}_{f} e)) = (x \in {Base}_{(F freeLMod I)} ⟼ \sum_{W} (x {\cdot_{W}}_{f} e))$
12		simpl1	$⊢ ((W \in LMod \land B \in J \land I \approx B) \land e : I \underset{1-1 onto}{⟶} B) \to W \in LMod$
13		relen	$⊢ Rel \approx$
14	13	brrelex1i	$⊢ I \approx B \to I \in V$
15	14	3ad2ant3	$⊢ (W \in LMod \land B \in J \land I \approx B) \to I \in V$
16	15	adantr	$⊢ ((W \in LMod \land B \in J \land I \approx B) \land e : I \underset{1-1 onto}{⟶} B) \to I \in V$
17	1	a1i	$⊢ ((W \in LMod \land B \in J \land I \approx B) \land e : I \underset{1-1 onto}{⟶} B) \to F = Scalar (W)$
18		f1ofo	$⊢ e : I \underset{1-1 onto}{⟶} B \to e : I \underset{onto}{⟶} B$
19	18	adantl	$⊢ ((W \in LMod \land B \in J \land I \approx B) \land e : I \underset{1-1 onto}{⟶} B) \to e : I \underset{onto}{⟶} B$
20	2	lbslinds	$⊢ J \subseteq LIndS (W)$
21	20	sseli	$⊢ B \in J \to B \in LIndS (W)$
22	21	3ad2ant2	$⊢ (W \in LMod \land B \in J \land I \approx B) \to B \in LIndS (W)$
23	22	adantr	$⊢ ((W \in LMod \land B \in J \land I \approx B) \land e : I \underset{1-1 onto}{⟶} B) \to B \in LIndS (W)$
24		f1of1	$⊢ e : I \underset{1-1 onto}{⟶} B \to e : I \underset{1-1}{⟶} B$
25	24	adantl	$⊢ ((W \in LMod \land B \in J \land I \approx B) \land e : I \underset{1-1 onto}{⟶} B) \to e : I \underset{1-1}{⟶} B$
26		f1linds	$⊢ (W \in LMod \land B \in LIndS (W) \land e : I \underset{1-1}{⟶} B) \to e LIndF W$
27	12 23 25 26	syl3anc	$⊢ ((W \in LMod \land B \in J \land I \approx B) \land e : I \underset{1-1 onto}{⟶} B) \to e LIndF W$
28	8 2 10	lbssp	$⊢ B \in J \to LSpan (W) (B) = {Base}_{W}$
29	28	3ad2ant2	$⊢ (W \in LMod \land B \in J \land I \approx B) \to LSpan (W) (B) = {Base}_{W}$
30	29	adantr	$⊢ ((W \in LMod \land B \in J \land I \approx B) \land e : I \underset{1-1 onto}{⟶} B) \to LSpan (W) (B) = {Base}_{W}$
31	6 7 8 9 10 11 12 16 17 19 27 30	indlcim	$⊢ ((W \in LMod \land B \in J \land I \approx B) \land e : I \underset{1-1 onto}{⟶} B) \to (x \in {Base}_{(F freeLMod I)} ⟼ \sum_{W} (x {\cdot_{W}}_{f} e)) \in ((F freeLMod I) LMIso W)$
32		lmimcnv	$⊢ (x \in {Base}_{(F freeLMod I)} ⟼ \sum_{W} (x {\cdot_{W}}_{f} e)) \in ((F freeLMod I) LMIso W) \to {(x \in {Base}_{(F freeLMod I)} ⟼ \sum_{W} (x {\cdot_{W}}_{f} e))}^{-1} \in (W LMIso (F freeLMod I))$
33		brlmici	$⊢ {(x \in {Base}_{(F freeLMod I)} ⟼ \sum_{W} (x {\cdot_{W}}_{f} e))}^{-1} \in (W LMIso (F freeLMod I)) \to W ≃_{𝑚} (F freeLMod I)$
34	31 32 33	3syl	$⊢ ((W \in LMod \land B \in J \land I \approx B) \land e : I \underset{1-1 onto}{⟶} B) \to W ≃_{𝑚} (F freeLMod I)$
35	5 34	exlimddv	$⊢ (W \in LMod \land B \in J \land I \approx B) \to W ≃_{𝑚} (F freeLMod I)$

Metamath Proof Explorer

Theorem lbslcic

Proof