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

Metamath Proof Explorer

Theorem mvrfval

Description: Value of the generating elements of the power series structure. (Contributed by Mario Carneiro, 7-Jan-2015)

Ref Expression
Hypotheses mvrfval.v ⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
mvrfval.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
mvrfval.z ⊢ 0 = ( 0g ‘ 𝑅 )
mvrfval.o ⊢ 1 = ( 1r ‘ 𝑅 )
mvrfval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
mvrfval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑌 )
Assertion mvrfval ( 𝜑 → 𝑉 = ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ∈ 𝐷 ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , 1 , 0 ) ) ) )

Proof

Step Hyp Ref Expression
1 mvrfval.v ⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
2 mvrfval.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
3 mvrfval.z ⊢ 0 = ( 0g ‘ 𝑅 )
4 mvrfval.o ⊢ 1 = ( 1r ‘ 𝑅 )
5 mvrfval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
6 mvrfval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑌 )
7 5 elexd ⊢ ( 𝜑 → 𝐼 ∈ V )
8 6 elexd ⊢ ( 𝜑 → 𝑅 ∈ V )
9 5 mptexd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ∈ 𝐷 ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , 1 , 0 ) ) ) ∈ V )
10 simpl ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → 𝑖 = 𝐼 )
11 10 oveq2d ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( ℕ0 ↑m 𝑖 ) = ( ℕ0 ↑m 𝐼 ) )
12 11 rabeqdv ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
13 12 2 eqtr4di ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = 𝐷 )
14 mpteq1 ⊢ ( 𝑖 = 𝐼 → ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) )
15 14 adantr ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) )
16 15 eqeq2d ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑓 = ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) ↔ 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) ) )
17 simpr ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → 𝑟 = 𝑅 )
18 17 fveq2d ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 1r ‘ 𝑟 ) = ( 1r ‘ 𝑅 ) )
19 18 4 eqtr4di ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 1r ‘ 𝑟 ) = 1 )
20 17 fveq2d ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 0g ‘ 𝑟 ) = ( 0g ‘ 𝑅 ) )
21 20 3 eqtr4di ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 0g ‘ 𝑟 ) = 0 )
22 16 19 21 ifbieq12d ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → if ( 𝑓 = ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) = if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , 1 , 0 ) )
23 13 22 mpteq12dv ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) ) = ( 𝑓 ∈ 𝐷 ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , 1 , 0 ) ) )
24 10 23 mpteq12dv ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑥 ∈ 𝑖 ↦ ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ∈ 𝐷 ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , 1 , 0 ) ) ) )
25 df-mvr ⊢ mVar = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑥 ∈ 𝑖 ↦ ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) ) ) )
26 24 25 ovmpoga ⊢ ( ( 𝐼 ∈ V ∧ 𝑅 ∈ V ∧ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ∈ 𝐷 ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , 1 , 0 ) ) ) ∈ V ) → ( 𝐼 mVar 𝑅 ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ∈ 𝐷 ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , 1 , 0 ) ) ) )
27 7 8 9 26 syl3anc ⊢ ( 𝜑 → ( 𝐼 mVar 𝑅 ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ∈ 𝐷 ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , 1 , 0 ) ) ) )
28 1 27 eqtrid ⊢ ( 𝜑 → 𝑉 = ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ∈ 𝐷 ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , 1 , 0 ) ) ) )