Theorem lvecdimfi

Description: Finite version of lvecdim which does not require the axiom of choice. The axiom of choice is used in acsmapd , which is required in the infinite case. Suggested by Gérard Lang. (Contributed by Thierry Arnoux, 24-May-2023)

	Ref	Expression
Hypotheses	lvecdimfi.j	$$⊢J=\mathrm{LBasis}\left(W\right)$$
	lvecdimfi.w	$$⊢\phi \to W\in \mathrm{LVec}$$
	lvecdimfi.s	$$⊢\phi \to S\in J$$
	lvecdimfi.t	$$⊢\phi \to T\in J$$
	lvecdimfi.f	$$⊢\phi \to S\in \mathrm{Fin}$$
Assertion	lvecdimfi	$$⊢\phi \to S\approx T$$

Proof

Step	Hyp	Ref	Expression
1		lvecdimfi.j	$$⊢J=\mathrm{LBasis}\left(W\right)$$
2		lvecdimfi.w	$$⊢\phi \to W\in \mathrm{LVec}$$
3		lvecdimfi.s	$$⊢\phi \to S\in J$$
4		lvecdimfi.t	$$⊢\phi \to T\in J$$
5		lvecdimfi.f	$$⊢\phi \to S\in \mathrm{Fin}$$
6		eqid	$$⊢\mathrm{LSubSp}\left(W\right)=\mathrm{LSubSp}\left(W\right)$$
7		eqid	$$⊢\mathrm{mrCls}\left(\mathrm{LSubSp}\left(W\right)\right)=\mathrm{mrCls}\left(\mathrm{LSubSp}\left(W\right)\right)$$
8		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
9	6 7 8	lssacsex	$$⊢W\in \mathrm{LVec}\to \left(\mathrm{LSubSp}\left(W\right)\in \mathrm{ACS}\left({\mathrm{Base}}_W\right)\wedge \forall x\in 𝒫{\mathrm{Base}}_W\forall y\in {\mathrm{Base}}_W\forall z\in \left(\mathrm{mrCls}\left(\mathrm{LSubSp}\left(W\right)\right)\left(x\cup \left\{y\right\}\right)\setminus \mathrm{mrCls}\left(\mathrm{LSubSp}\left(W\right)\right)\left(x\right)\right)y\in \mathrm{mrCls}\left(\mathrm{LSubSp}\left(W\right)\right)\left(x\cup \left\{z\right\}\right)\right)$$
10	2 9	syl	$$⊢\phi \to \left(\mathrm{LSubSp}\left(W\right)\in \mathrm{ACS}\left({\mathrm{Base}}_W\right)\wedge \forall x\in 𝒫{\mathrm{Base}}_W\forall y\in {\mathrm{Base}}_W\forall z\in \left(\mathrm{mrCls}\left(\mathrm{LSubSp}\left(W\right)\right)\left(x\cup \left\{y\right\}\right)\setminus \mathrm{mrCls}\left(\mathrm{LSubSp}\left(W\right)\right)\left(x\right)\right)y\in \mathrm{mrCls}\left(\mathrm{LSubSp}\left(W\right)\right)\left(x\cup \left\{z\right\}\right)\right)$$
11	10	simpld	$$⊢\phi \to \mathrm{LSubSp}\left(W\right)\in \mathrm{ACS}\left({\mathrm{Base}}_W\right)$$
12	11	acsmred	$$⊢\phi \to \mathrm{LSubSp}\left(W\right)\in \mathrm{Moore}\left({\mathrm{Base}}_W\right)$$
13		eqid	$$⊢\mathrm{mrInd}\left(\mathrm{LSubSp}\left(W\right)\right)=\mathrm{mrInd}\left(\mathrm{LSubSp}\left(W\right)\right)$$
14	10	simprd	$$⊢\phi \to \forall x\in 𝒫{\mathrm{Base}}_W\forall y\in {\mathrm{Base}}_W\forall z\in \left(\mathrm{mrCls}\left(\mathrm{LSubSp}\left(W\right)\right)\left(x\cup \left\{y\right\}\right)\setminus \mathrm{mrCls}\left(\mathrm{LSubSp}\left(W\right)\right)\left(x\right)\right)y\in \mathrm{mrCls}\left(\mathrm{LSubSp}\left(W\right)\right)\left(x\cup \left\{z\right\}\right)$$
15	6 7 8 13 1	lbsacsbs	$$⊢W\in \mathrm{LVec}\to \left(S\in J\leftrightarrow \left(S\in \mathrm{mrInd}\left(\mathrm{LSubSp}\left(W\right)\right)\wedge \mathrm{mrCls}\left(\mathrm{LSubSp}\left(W\right)\right)\left(S\right)={\mathrm{Base}}_W\right)\right)$$
16	15	biimpa	$$⊢\left(W\in \mathrm{LVec}\wedge S\in J\right)\to \left(S\in \mathrm{mrInd}\left(\mathrm{LSubSp}\left(W\right)\right)\wedge \mathrm{mrCls}\left(\mathrm{LSubSp}\left(W\right)\right)\left(S\right)={\mathrm{Base}}_W\right)$$
17	2 3 16	syl2anc	$$⊢\phi \to \left(S\in \mathrm{mrInd}\left(\mathrm{LSubSp}\left(W\right)\right)\wedge \mathrm{mrCls}\left(\mathrm{LSubSp}\left(W\right)\right)\left(S\right)={\mathrm{Base}}_W\right)$$
18	17	simpld	$$⊢\phi \to S\in \mathrm{mrInd}\left(\mathrm{LSubSp}\left(W\right)\right)$$
19	6 7 8 13 1	lbsacsbs	$$⊢W\in \mathrm{LVec}\to \left(T\in J\leftrightarrow \left(T\in \mathrm{mrInd}\left(\mathrm{LSubSp}\left(W\right)\right)\wedge \mathrm{mrCls}\left(\mathrm{LSubSp}\left(W\right)\right)\left(T\right)={\mathrm{Base}}_W\right)\right)$$
20	19	biimpa	$$⊢\left(W\in \mathrm{LVec}\wedge T\in J\right)\to \left(T\in \mathrm{mrInd}\left(\mathrm{LSubSp}\left(W\right)\right)\wedge \mathrm{mrCls}\left(\mathrm{LSubSp}\left(W\right)\right)\left(T\right)={\mathrm{Base}}_W\right)$$
21	2 4 20	syl2anc	$$⊢\phi \to \left(T\in \mathrm{mrInd}\left(\mathrm{LSubSp}\left(W\right)\right)\wedge \mathrm{mrCls}\left(\mathrm{LSubSp}\left(W\right)\right)\left(T\right)={\mathrm{Base}}_W\right)$$
22	21	simpld	$$⊢\phi \to T\in \mathrm{mrInd}\left(\mathrm{LSubSp}\left(W\right)\right)$$
23	17	simprd	$$⊢\phi \to \mathrm{mrCls}\left(\mathrm{LSubSp}\left(W\right)\right)\left(S\right)={\mathrm{Base}}_W$$
24	21	simprd	$$⊢\phi \to \mathrm{mrCls}\left(\mathrm{LSubSp}\left(W\right)\right)\left(T\right)={\mathrm{Base}}_W$$
25	23 24	eqtr4d	$$⊢\phi \to \mathrm{mrCls}\left(\mathrm{LSubSp}\left(W\right)\right)\left(S\right)=\mathrm{mrCls}\left(\mathrm{LSubSp}\left(W\right)\right)\left(T\right)$$
26	12 7 13 14 18 22 5 25	mreexfidimd	$$⊢\phi \to S\approx T$$