Theorem frlmpwfi

Description: Formal linear combinations over Z/2Z are equivalent to finite subsets. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015) (Proof shortened by AV, 14-Jun-2020)

	Ref	Expression
Hypotheses	frlmpwfi.r	$$⊢R=\mathbb{Z}/2\mathbb{Z}$$
	frlmpwfi.y	$$⊢Y=R\mathrm{freeLMod}I$$
	frlmpwfi.b	$$⊢B={\mathrm{Base}}_Y$$
Assertion	frlmpwfi	$$⊢I\in V\to B\approx \left(𝒫I\cap \mathrm{Fin}\right)$$

Proof

Step	Hyp	Ref	Expression
1		frlmpwfi.r	$$⊢R=\mathbb{Z}/2\mathbb{Z}$$
2		frlmpwfi.y	$$⊢Y=R\mathrm{freeLMod}I$$
3		frlmpwfi.b	$$⊢B={\mathrm{Base}}_Y$$
4	1	fvexi	$$⊢R\in \mathrm{V}$$
5		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
6		eqid	$$⊢0_R=0_R$$
7		eqid	$$⊢\left\{x\in \left({{\mathrm{Base}}_R}^I\right)|{finSupp}_{0_R}\left(x\right)\right\}=\left\{x\in \left({{\mathrm{Base}}_R}^I\right)|{finSupp}_{0_R}\left(x\right)\right\}$$
8	2 5 6 7	frlmbas	$$⊢\left(R\in \mathrm{V}\wedge I\in V\right)\to \left\{x\in \left({{\mathrm{Base}}_R}^I\right)|{finSupp}_{0_R}\left(x\right)\right\}={\mathrm{Base}}_Y$$
9	4 8	mpan	$$⊢I\in V\to \left\{x\in \left({{\mathrm{Base}}_R}^I\right)|{finSupp}_{0_R}\left(x\right)\right\}={\mathrm{Base}}_Y$$
10	9 3	eqtr4di	$$⊢I\in V\to \left\{x\in \left({{\mathrm{Base}}_R}^I\right)|{finSupp}_{0_R}\left(x\right)\right\}=B$$
11		eqid	$$⊢\left\{x\in \left({2_{𝑜}}^I\right)|{finSupp}_{\varnothing }\left(x\right)\right\}=\left\{x\in \left({2_{𝑜}}^I\right)|{finSupp}_{\varnothing }\left(x\right)\right\}$$
12		enrefg	$$⊢I\in V\to I\approx I$$
13		2nn	$$⊢2\in \mathbb{N}$$
14	1 5	znhash	$$⊢2\in \mathbb{N}\to \left|{\mathrm{Base}}_R\right|=2$$
15	13 14	ax-mp	$$⊢\left|{\mathrm{Base}}_R\right|=2$$
16		hash2	$$⊢\left|2_{𝑜}\right|=2$$
17	15 16	eqtr4i	$$⊢\left|{\mathrm{Base}}_R\right|=\left|2_{𝑜}\right|$$
18		2nn0	$$⊢2\in {\mathbb{N}}_0$$
19	15 18	eqeltri	$$⊢\left|{\mathrm{Base}}_R\right|\in {\mathbb{N}}_0$$
20		fvex	$$⊢{\mathrm{Base}}_R\in \mathrm{V}$$
21		hashclb	$$⊢{\mathrm{Base}}_R\in \mathrm{V}\to \left({\mathrm{Base}}_R\in \mathrm{Fin}\leftrightarrow \left|{\mathrm{Base}}_R\right|\in {\mathbb{N}}_0\right)$$
22	20 21	ax-mp	$$⊢{\mathrm{Base}}_R\in \mathrm{Fin}\leftrightarrow \left|{\mathrm{Base}}_R\right|\in {\mathbb{N}}_0$$
23	19 22	mpbir	$$⊢{\mathrm{Base}}_R\in \mathrm{Fin}$$
24		2onn	$$⊢2_{𝑜}\in \mathrm{\omega }$$
25		nnfi	$$⊢2_{𝑜}\in \mathrm{\omega }\to 2_{𝑜}\in \mathrm{Fin}$$
26	24 25	ax-mp	$$⊢2_{𝑜}\in \mathrm{Fin}$$
27		hashen	$$⊢\left({\mathrm{Base}}_R\in \mathrm{Fin}\wedge 2_{𝑜}\in \mathrm{Fin}\right)\to \left(\left|{\mathrm{Base}}_R\right|=\left|2_{𝑜}\right|\leftrightarrow {\mathrm{Base}}_R\approx 2_{𝑜}\right)$$
28	23 26 27	mp2an	$$⊢\left|{\mathrm{Base}}_R\right|=\left|2_{𝑜}\right|\leftrightarrow {\mathrm{Base}}_R\approx 2_{𝑜}$$
29	17 28	mpbi	$$⊢{\mathrm{Base}}_R\approx 2_{𝑜}$$
30	29	a1i	$$⊢I\in V\to {\mathrm{Base}}_R\approx 2_{𝑜}$$
31	1	zncrng	$$⊢2\in {\mathbb{N}}_0\to R\in \mathrm{CRing}$$
32		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
33	18 31 32	mp2b	$$⊢R\in \mathrm{Ring}$$
34	5 6	ring0cl	$$⊢R\in \mathrm{Ring}\to 0_R\in {\mathrm{Base}}_R$$
35	33 34	mp1i	$$⊢I\in V\to 0_R\in {\mathrm{Base}}_R$$
36		2on0	$$⊢2_{𝑜}\ne \varnothing$$
37		2on	$$⊢2_{𝑜}\in \mathrm{On}$$
38		on0eln0	$$⊢2_{𝑜}\in \mathrm{On}\to \left(\varnothing \in 2_{𝑜}\leftrightarrow 2_{𝑜}\ne \varnothing \right)$$
39	37 38	ax-mp	$$⊢\varnothing \in 2_{𝑜}\leftrightarrow 2_{𝑜}\ne \varnothing$$
40	36 39	mpbir	$$⊢\varnothing \in 2_{𝑜}$$
41	40	a1i	$$⊢I\in V\to \varnothing \in 2_{𝑜}$$
42	7 11 12 30 35 41	mapfien2	$$⊢I\in V\to \left\{x\in \left({{\mathrm{Base}}_R}^I\right)|{finSupp}_{0_R}\left(x\right)\right\}\approx \left\{x\in \left({2_{𝑜}}^I\right)|{finSupp}_{\varnothing }\left(x\right)\right\}$$
43	10 42	eqbrtrrd	$$⊢I\in V\to B\approx \left\{x\in \left({2_{𝑜}}^I\right)|{finSupp}_{\varnothing }\left(x\right)\right\}$$
44	11	pwfi2en	$$⊢I\in V\to \left\{x\in \left({2_{𝑜}}^I\right)|{finSupp}_{\varnothing }\left(x\right)\right\}\approx \left(𝒫I\cap \mathrm{Fin}\right)$$
45		entr	$$⊢\left(B\approx \left\{x\in \left({2_{𝑜}}^I\right)|{finSupp}_{\varnothing }\left(x\right)\right\}\wedge \left\{x\in \left({2_{𝑜}}^I\right)|{finSupp}_{\varnothing }\left(x\right)\right\}\approx \left(𝒫I\cap \mathrm{Fin}\right)\right)\to B\approx \left(𝒫I\cap \mathrm{Fin}\right)$$
46	43 44 45	syl2anc	$$⊢I\in V\to B\approx \left(𝒫I\cap \mathrm{Fin}\right)$$