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

Metamath Proof Explorer

Theorem mvrvalind

Description: Value of the generating elements of the power series structure, expressed using the indicator function. (Contributed by Thierry Arnoux, 25-Jan-2026)

Ref Expression
Hypotheses mvrvalind.1 ⊢ V = I mVar R
mvrvalind.2 ⊢ D = h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
mvrvalind.3 ⊢ 0 ˙ = 0 R
mvrvalind.4 ⊢ 1 ˙ = 1 R
mvrvalind.5 ⊢ φ → I ∈ W
mvrvalind.6 ⊢ φ → R ∈ Y
mvrvalind.7 ⊢ φ → X ∈ I
mvrvalind.8 ⊢ φ → F ∈ D
mvrvalind.9 ⊢ A = 𝟙 I ⁡ X
Assertion mvrvalind ⊢ φ → V ⁡ X ⁡ F = if F = A 1 ˙ 0 ˙

Proof

Step Hyp Ref Expression
1 mvrvalind.1 ⊢ V = I mVar R
2 mvrvalind.2 ⊢ D = h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
3 mvrvalind.3 ⊢ 0 ˙ = 0 R
4 mvrvalind.4 ⊢ 1 ˙ = 1 R
5 mvrvalind.5 ⊢ φ → I ∈ W
6 mvrvalind.6 ⊢ φ → R ∈ Y
7 mvrvalind.7 ⊢ φ → X ∈ I
8 mvrvalind.8 ⊢ φ → F ∈ D
9 mvrvalind.9 ⊢ A = 𝟙 I ⁡ X
10 1 2 3 4 5 6 7 8 mvrval2 ⊢ φ → V ⁡ X ⁡ F = if F = y ∈ I ⟼ if y = X 1 0 1 ˙ 0 ˙
11 9 a1i ⊢ φ → A = 𝟙 I ⁡ X
12 7 snssd ⊢ φ → X ⊆ I
13 indval ⊢ I ∈ W ∧ X ⊆ I → 𝟙 I ⁡ X = y ∈ I ⟼ if y ∈ X 1 0
14 5 12 13 syl2anc ⊢ φ → 𝟙 I ⁡ X = y ∈ I ⟼ if y ∈ X 1 0
15 velsn ⊢ y ∈ X ↔ y = X
16 15 a1i ⊢ φ → y ∈ X ↔ y = X
17 16 ifbid ⊢ φ → if y ∈ X 1 0 = if y = X 1 0
18 17 mpteq2dv ⊢ φ → y ∈ I ⟼ if y ∈ X 1 0 = y ∈ I ⟼ if y = X 1 0
19 11 14 18 3eqtrd ⊢ φ → A = y ∈ I ⟼ if y = X 1 0
20 19 eqeq2d ⊢ φ → F = A ↔ F = y ∈ I ⟼ if y = X 1 0
21 20 ifbid ⊢ φ → if F = A 1 ˙ 0 ˙ = if F = y ∈ I ⟼ if y = X 1 0 1 ˙ 0 ˙
22 10 21 eqtr4d ⊢ φ → V ⁡ X ⁡ F = if F = A 1 ˙ 0 ˙