This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem frlmfibas

Description: The base set of the finite free module as a set exponential. (Contributed by AV, 6-Dec-2018)

Ref Expression
Hypotheses frlmfibas.f ⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
frlmfibas.n ⊢ 𝑁 = ( Base ‘ 𝑅 )
Assertion frlmfibas ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ Fin ) → ( 𝑁 ↑m 𝐼 ) = ( Base ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 frlmfibas.f ⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
2 frlmfibas.n ⊢ 𝑁 = ( Base ‘ 𝑅 )
3 elmapi ⊢ ( 𝑎 ∈ ( 𝑁 ↑m 𝐼 ) → 𝑎 : 𝐼 ⟶ 𝑁 )
4 3 adantl ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑎 ∈ ( 𝑁 ↑m 𝐼 ) ) → 𝑎 : 𝐼 ⟶ 𝑁 )
5 simpl ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑎 ∈ ( 𝑁 ↑m 𝐼 ) ) → 𝐼 ∈ Fin )
6 fvexd ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑎 ∈ ( 𝑁 ↑m 𝐼 ) ) → ( 0g ‘ 𝑅 ) ∈ V )
7 4 5 6 fdmfifsupp ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑎 ∈ ( 𝑁 ↑m 𝐼 ) ) → 𝑎 finSupp ( 0g ‘ 𝑅 ) )
8 7 ralrimiva ⊢ ( 𝐼 ∈ Fin → ∀ 𝑎 ∈ ( 𝑁 ↑m 𝐼 ) 𝑎 finSupp ( 0g ‘ 𝑅 ) )
9 8 adantl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ Fin ) → ∀ 𝑎 ∈ ( 𝑁 ↑m 𝐼 ) 𝑎 finSupp ( 0g ‘ 𝑅 ) )
10 rabid2 ⊢ ( ( 𝑁 ↑m 𝐼 ) = { 𝑎 ∈ ( 𝑁 ↑m 𝐼 ) ∣ 𝑎 finSupp ( 0g ‘ 𝑅 ) } ↔ ∀ 𝑎 ∈ ( 𝑁 ↑m 𝐼 ) 𝑎 finSupp ( 0g ‘ 𝑅 ) )
11 9 10 sylibr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ Fin ) → ( 𝑁 ↑m 𝐼 ) = { 𝑎 ∈ ( 𝑁 ↑m 𝐼 ) ∣ 𝑎 finSupp ( 0g ‘ 𝑅 ) } )
12 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
13 eqid ⊢ { 𝑎 ∈ ( 𝑁 ↑m 𝐼 ) ∣ 𝑎 finSupp ( 0g ‘ 𝑅 ) } = { 𝑎 ∈ ( 𝑁 ↑m 𝐼 ) ∣ 𝑎 finSupp ( 0g ‘ 𝑅 ) }
14 1 2 12 13 frlmbas ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ Fin ) → { 𝑎 ∈ ( 𝑁 ↑m 𝐼 ) ∣ 𝑎 finSupp ( 0g ‘ 𝑅 ) } = ( Base ‘ 𝐹 ) )
15 11 14 eqtrd ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ Fin ) → ( 𝑁 ↑m 𝐼 ) = ( Base ‘ 𝐹 ) )