Metamath Proof Explorer


Theorem mvrf

Description: The power series variable function is a function from the index set to elements of the power series structure representing X i for each i . (Contributed by Mario Carneiro, 29-Dec-2014)

Ref Expression
Hypotheses mvrf.s 𝑆 = ( 𝐼 mPwSer 𝑅 )
mvrf.v 𝑉 = ( 𝐼 mVar 𝑅 )
mvrf.b 𝐵 = ( Base ‘ 𝑆 )
mvrf.i ( 𝜑𝐼𝑊 )
mvrf.r ( 𝜑𝑅 ∈ Ring )
Assertion mvrf ( 𝜑𝑉 : 𝐼𝐵 )

Proof

Step Hyp Ref Expression
1 mvrf.s 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 mvrf.v 𝑉 = ( 𝐼 mVar 𝑅 )
3 mvrf.b 𝐵 = ( Base ‘ 𝑆 )
4 mvrf.i ( 𝜑𝐼𝑊 )
5 mvrf.r ( 𝜑𝑅 ∈ Ring )
6 eqid { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } = { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin }
7 eqid ( 0g𝑅 ) = ( 0g𝑅 )
8 eqid ( 1r𝑅 ) = ( 1r𝑅 )
9 2 6 7 8 4 5 mvrfval ( 𝜑𝑉 = ( 𝑥𝐼 ↦ ( 𝑓 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r𝑅 ) , ( 0g𝑅 ) ) ) ) )
10 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
11 10 8 ringidcl ( 𝑅 ∈ Ring → ( 1r𝑅 ) ∈ ( Base ‘ 𝑅 ) )
12 5 11 syl ( 𝜑 → ( 1r𝑅 ) ∈ ( Base ‘ 𝑅 ) )
13 10 7 ring0cl ( 𝑅 ∈ Ring → ( 0g𝑅 ) ∈ ( Base ‘ 𝑅 ) )
14 5 13 syl ( 𝜑 → ( 0g𝑅 ) ∈ ( Base ‘ 𝑅 ) )
15 12 14 ifcld ( 𝜑 → if ( 𝑓 = ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r𝑅 ) , ( 0g𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
16 15 ad2antrr ( ( ( 𝜑𝑥𝐼 ) ∧ 𝑓 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) → if ( 𝑓 = ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r𝑅 ) , ( 0g𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
17 16 fmpttd ( ( 𝜑𝑥𝐼 ) → ( 𝑓 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r𝑅 ) , ( 0g𝑅 ) ) ) : { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
18 fvex ( Base ‘ 𝑅 ) ∈ V
19 ovex ( ℕ0m 𝐼 ) ∈ V
20 19 rabex { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ∈ V
21 18 20 elmap ( ( 𝑓 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r𝑅 ) , ( 0g𝑅 ) ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) ↔ ( 𝑓 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r𝑅 ) , ( 0g𝑅 ) ) ) : { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
22 17 21 sylibr ( ( 𝜑𝑥𝐼 ) → ( 𝑓 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r𝑅 ) , ( 0g𝑅 ) ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) )
23 1 10 6 3 4 psrbas ( 𝜑𝐵 = ( ( Base ‘ 𝑅 ) ↑m { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) )
24 23 adantr ( ( 𝜑𝑥𝐼 ) → 𝐵 = ( ( Base ‘ 𝑅 ) ↑m { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) )
25 22 24 eleqtrrd ( ( 𝜑𝑥𝐼 ) → ( 𝑓 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r𝑅 ) , ( 0g𝑅 ) ) ) ∈ 𝐵 )
26 9 25 fmpt3d ( 𝜑𝑉 : 𝐼𝐵 )