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	syl5eq	⊢ ( 𝜑 → 𝑉 = ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ∈ 𝐷 ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , 1 , 0 ) ) ) )