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 ⊢ V = I mVar R
subrgmvr.i ⊢ φ → I ∈ W
subrgmvr.r ⊢ φ → T ∈ SubRing ⁡ R
subrgmvr.h ⊢ H = R ↾ 𝑠 T
Assertion subrgmvr ⊢ φ → V = I mVar H

Proof

Step Hyp Ref Expression
1 subrgmvr.v ⊢ V = I mVar R
2 subrgmvr.i ⊢ φ → I ∈ W
3 subrgmvr.r ⊢ φ → T ∈ SubRing ⁡ R
4 subrgmvr.h ⊢ H = R ↾ 𝑠 T
5 eqid ⊢ 1 R = 1 R
6 4 5 subrg1 ⊢ T ∈ SubRing ⁡ R → 1 R = 1 H
7 3 6 syl ⊢ φ → 1 R = 1 H
8 eqid ⊢ 0 R = 0 R
9 4 8 subrg0 ⊢ T ∈ SubRing ⁡ R → 0 R = 0 H
10 3 9 syl ⊢ φ → 0 R = 0 H
11 7 10 ifeq12d ⊢ φ → if y = z ∈ I ⟼ if z = x 1 0 1 R 0 R = if y = z ∈ I ⟼ if z = x 1 0 1 H 0 H
12 11 mpteq2dv ⊢ φ → y ∈ f ∈ ℕ 0 I | f -1 ℕ ∈ Fin ⟼ if y = z ∈ I ⟼ if z = x 1 0 1 R 0 R = y ∈ f ∈ ℕ 0 I | f -1 ℕ ∈ Fin ⟼ if y = z ∈ I ⟼ if z = x 1 0 1 H 0 H
13 12 mpteq2dv ⊢ φ → x ∈ I ⟼ y ∈ f ∈ ℕ 0 I | f -1 ℕ ∈ Fin ⟼ if y = z ∈ I ⟼ if z = x 1 0 1 R 0 R = x ∈ I ⟼ y ∈ f ∈ ℕ 0 I | f -1 ℕ ∈ Fin ⟼ if y = z ∈ I ⟼ if z = x 1 0 1 H 0 H
14 eqid ⊢ f ∈ ℕ 0 I | f -1 ℕ ∈ Fin = f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
15 subrgrcl ⊢ T ∈ SubRing ⁡ R → R ∈ Ring
16 3 15 syl ⊢ φ → R ∈ Ring
17 1 14 8 5 2 16 mvrfval ⊢ φ → V = x ∈ I ⟼ y ∈ f ∈ ℕ 0 I | f -1 ℕ ∈ Fin ⟼ if y = z ∈ I ⟼ if z = x 1 0 1 R 0 R
18 eqid ⊢ I mVar H = I mVar H
19 eqid ⊢ 0 H = 0 H
20 eqid ⊢ 1 H = 1 H
21 4 ovexi ⊢ H ∈ V
22 21 a1i ⊢ φ → H ∈ V
23 18 14 19 20 2 22 mvrfval ⊢ φ → I mVar H = x ∈ I ⟼ y ∈ f ∈ ℕ 0 I | f -1 ℕ ∈ Fin ⟼ if y = z ∈ I ⟼ if z = x 1 0 1 H 0 H
24 13 17 23 3eqtr4d ⊢ φ → V = I mVar H