Metamath Proof Explorer

Theorem subrgmvr

Description: The variables in a subring polynomial algebra are the same as the original ring. (Contributed by Mario Carneiro, 4-Jul-2015)

Ref Expression
Hypotheses subrgmvr.v ⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
subrgmvr.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
subrgmvr.r ⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
subrgmvr.h ⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
Assertion subrgmvr ( 𝜑 → 𝑉 = ( 𝐼 mVar 𝐻 ) )

Proof

Step Hyp Ref Expression
1 subrgmvr.v ⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
2 subrgmvr.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
3 subrgmvr.r ⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
4 subrgmvr.h ⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
5 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
6 4 5 subrg1 ⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝐻 ) )
7 3 6 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝐻 ) )
8 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
9 4 8 subrg0 ⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝐻 ) )
10 3 9 syl ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝐻 ) )
11 7 10 ifeq12d ⊢ ( 𝜑 → if ( 𝑦 = ( 𝑧 ∈ 𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = if ( 𝑦 = ( 𝑧 ∈ 𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝐻 ) , ( 0g ‘ 𝐻 ) ) )
12 11 mpteq2dv ⊢ ( 𝜑 → ( 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = ( 𝑧 ∈ 𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = ( 𝑧 ∈ 𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝐻 ) , ( 0g ‘ 𝐻 ) ) ) )
13 12 mpteq2dv ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = ( 𝑧 ∈ 𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = ( 𝑧 ∈ 𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝐻 ) , ( 0g ‘ 𝐻 ) ) ) ) )
14 eqid ⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
15 subrgrcl ⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝑅 ∈ Ring )
16 3 15 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
17 1 14 8 5 2 16 mvrfval ⊢ ( 𝜑 → 𝑉 = ( 𝑥 ∈ 𝐼 ↦ ( 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = ( 𝑧 ∈ 𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) )
18 eqid ⊢ ( 𝐼 mVar 𝐻 ) = ( 𝐼 mVar 𝐻 )
19 eqid ⊢ ( 0g ‘ 𝐻 ) = ( 0g ‘ 𝐻 )
20 eqid ⊢ ( 1r ‘ 𝐻 ) = ( 1r ‘ 𝐻 )
21 4 ovexi ⊢ 𝐻 ∈ V
22 21 a1i ⊢ ( 𝜑 → 𝐻 ∈ V )
23 18 14 19 20 2 22 mvrfval ⊢ ( 𝜑 → ( 𝐼 mVar 𝐻 ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = ( 𝑧 ∈ 𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝐻 ) , ( 0g ‘ 𝐻 ) ) ) ) )
24 13 17 23 3eqtr4d ⊢ ( 𝜑 → 𝑉 = ( 𝐼 mVar 𝐻 ) )