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	⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
7		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
8		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
9	2 6 7 8 4 5	mvrfval	⊢ ( 𝜑 → 𝑉 = ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ 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	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
17	16	fmpttd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
18		fvex	⊢ ( Base ‘ 𝑅 ) ∈ V
19		ovex	⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
20	19	rabex	⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∈ V
21	18 20	elmap	⊢ ( ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ↔ ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
22	17 21	sylibr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) )
23	1 10 6 3 4	psrbas	⊢ ( 𝜑 → 𝐵 = ( ( Base ‘ 𝑅 ) ↑m { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) )
24	23	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐵 = ( ( Base ‘ 𝑅 ) ↑m { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) )
25	22 24	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ∈ 𝐵 )
26	9 25	fmpt3d	⊢ ( 𝜑 → 𝑉 : 𝐼 ⟶ 𝐵 )