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	⊢ 𝑅 = ( ℤ/nℤ ‘ 2 )
	frlmpwfi.y	⊢ 𝑌 = ( 𝑅 freeLMod 𝐼 )
	frlmpwfi.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
Assertion	frlmpwfi	⊢ ( 𝐼 ∈ 𝑉 → 𝐵 ≈ ( 𝒫 𝐼 ∩ Fin ) )

Proof

Step	Hyp	Ref	Expression
1		frlmpwfi.r	⊢ 𝑅 = ( ℤ/nℤ ‘ 2 )
2		frlmpwfi.y	⊢ 𝑌 = ( 𝑅 freeLMod 𝐼 )
3		frlmpwfi.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
4	1	fvexi	⊢ 𝑅 ∈ V
5		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
7		eqid	⊢ { 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ∣ 𝑥 finSupp ( 0g ‘ 𝑅 ) } = { 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ∣ 𝑥 finSupp ( 0g ‘ 𝑅 ) }
8	2 5 6 7	frlmbas	⊢ ( ( 𝑅 ∈ V ∧ 𝐼 ∈ 𝑉 ) → { 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ∣ 𝑥 finSupp ( 0g ‘ 𝑅 ) } = ( Base ‘ 𝑌 ) )
9	4 8	mpan	⊢ ( 𝐼 ∈ 𝑉 → { 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ∣ 𝑥 finSupp ( 0g ‘ 𝑅 ) } = ( Base ‘ 𝑌 ) )
10	9 3	eqtr4di	⊢ ( 𝐼 ∈ 𝑉 → { 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ∣ 𝑥 finSupp ( 0g ‘ 𝑅 ) } = 𝐵 )
11		eqid	⊢ { 𝑥 ∈ ( 2o ↑m 𝐼 ) ∣ 𝑥 finSupp ∅ } = { 𝑥 ∈ ( 2o ↑m 𝐼 ) ∣ 𝑥 finSupp ∅ }
12		enrefg	⊢ ( 𝐼 ∈ 𝑉 → 𝐼 ≈ 𝐼 )
13		2nn	⊢ 2 ∈ ℕ
14	1 5	znhash	⊢ ( 2 ∈ ℕ → ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 2 )
15	13 14	ax-mp	⊢ ( ♯ ‘ ( Base ‘ 𝑅 ) ) = 2
16		hash2	⊢ ( ♯ ‘ 2o ) = 2
17	15 16	eqtr4i	⊢ ( ♯ ‘ ( Base ‘ 𝑅 ) ) = ( ♯ ‘ 2o )
18		2nn0	⊢ 2 ∈ ℕ0
19	15 18	eqeltri	⊢ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ∈ ℕ0
20		fvex	⊢ ( Base ‘ 𝑅 ) ∈ V
21		hashclb	⊢ ( ( Base ‘ 𝑅 ) ∈ V → ( ( Base ‘ 𝑅 ) ∈ Fin ↔ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ∈ ℕ0 ) )
22	20 21	ax-mp	⊢ ( ( Base ‘ 𝑅 ) ∈ Fin ↔ ( ♯ ‘ ( Base ‘ 𝑅 ) ) ∈ ℕ0 )
23	19 22	mpbir	⊢ ( Base ‘ 𝑅 ) ∈ Fin
24		2onn	⊢ 2o ∈ ω
25		nnfi	⊢ ( 2o ∈ ω → 2o ∈ Fin )
26	24 25	ax-mp	⊢ 2o ∈ Fin
27		hashen	⊢ ( ( ( Base ‘ 𝑅 ) ∈ Fin ∧ 2o ∈ Fin ) → ( ( ♯ ‘ ( Base ‘ 𝑅 ) ) = ( ♯ ‘ 2o ) ↔ ( Base ‘ 𝑅 ) ≈ 2o ) )
28	23 26 27	mp2an	⊢ ( ( ♯ ‘ ( Base ‘ 𝑅 ) ) = ( ♯ ‘ 2o ) ↔ ( Base ‘ 𝑅 ) ≈ 2o )
29	17 28	mpbi	⊢ ( Base ‘ 𝑅 ) ≈ 2o
30	29	a1i	⊢ ( 𝐼 ∈ 𝑉 → ( Base ‘ 𝑅 ) ≈ 2o )
31	1	zncrng	⊢ ( 2 ∈ ℕ0 → 𝑅 ∈ CRing )
32		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
33	18 31 32	mp2b	⊢ 𝑅 ∈ Ring
34	5 6	ring0cl	⊢ ( 𝑅 ∈ Ring → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
35	33 34	mp1i	⊢ ( 𝐼 ∈ 𝑉 → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
36		2on0	⊢ 2o ≠ ∅
37		2on	⊢ 2o ∈ On
38		on0eln0	⊢ ( 2o ∈ On → ( ∅ ∈ 2o ↔ 2o ≠ ∅ ) )
39	37 38	ax-mp	⊢ ( ∅ ∈ 2o ↔ 2o ≠ ∅ )
40	36 39	mpbir	⊢ ∅ ∈ 2o
41	40	a1i	⊢ ( 𝐼 ∈ 𝑉 → ∅ ∈ 2o )
42	7 11 12 30 35 41	mapfien2	⊢ ( 𝐼 ∈ 𝑉 → { 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ∣ 𝑥 finSupp ( 0g ‘ 𝑅 ) } ≈ { 𝑥 ∈ ( 2o ↑m 𝐼 ) ∣ 𝑥 finSupp ∅ } )
43	10 42	eqbrtrrd	⊢ ( 𝐼 ∈ 𝑉 → 𝐵 ≈ { 𝑥 ∈ ( 2o ↑m 𝐼 ) ∣ 𝑥 finSupp ∅ } )
44	11	pwfi2en	⊢ ( 𝐼 ∈ 𝑉 → { 𝑥 ∈ ( 2o ↑m 𝐼 ) ∣ 𝑥 finSupp ∅ } ≈ ( 𝒫 𝐼 ∩ Fin ) )
45		entr	⊢ ( ( 𝐵 ≈ { 𝑥 ∈ ( 2o ↑m 𝐼 ) ∣ 𝑥 finSupp ∅ } ∧ { 𝑥 ∈ ( 2o ↑m 𝐼 ) ∣ 𝑥 finSupp ∅ } ≈ ( 𝒫 𝐼 ∩ Fin ) ) → 𝐵 ≈ ( 𝒫 𝐼 ∩ Fin ) )
46	43 44 45	syl2anc	⊢ ( 𝐼 ∈ 𝑉 → 𝐵 ≈ ( 𝒫 𝐼 ∩ Fin ) )