Metamath Proof Explorer

Theorem mvrf1

Description: The power series variable function is injective if the base ring is nonzero. (Contributed by Mario Carneiro, 29-Dec-2014)

Ref Expression
Hypotheses mvrf.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
mvrf.v ⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
mvrf.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
mvrf.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
mvrf.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
mvrf1.z ⊢ 0 = ( 0g ‘ 𝑅 )
mvrf1.o ⊢ 1 = ( 1r ‘ 𝑅 )
mvrf1.n ⊢ ( 𝜑 → 1 ≠ 0 )
Assertion mvrf1 ( 𝜑 → 𝑉 : 𝐼 –1-1→ 𝐵 )

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 mvrf1.z ⊢ 0 = ( 0g ‘ 𝑅 )
7 mvrf1.o ⊢ 1 = ( 1r ‘ 𝑅 )
8 mvrf1.n ⊢ ( 𝜑 → 1 ≠ 0 )
9 1 2 3 4 5 mvrf ⊢ ( 𝜑 → 𝑉 : 𝐼 ⟶ 𝐵 )
10 8 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ) ∧ ( 𝑉 ‘ 𝑥 ) = ( 𝑉 ‘ 𝑦 ) ) ) → 1 ≠ 0 )
11 simp2r ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ) ∧ ( 𝑉 ‘ 𝑥 ) = ( 𝑉 ‘ 𝑦 ) ) ∧ ¬ 𝑥 = 𝑦 ) → ( 𝑉 ‘ 𝑥 ) = ( 𝑉 ‘ 𝑦 ) )
12 11 fveq1d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ) ∧ ( 𝑉 ‘ 𝑥 ) = ( 𝑉 ‘ 𝑦 ) ) ∧ ¬ 𝑥 = 𝑦 ) → ( ( 𝑉 ‘ 𝑥 ) ‘ ( 𝑧 ∈ 𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) ) = ( ( 𝑉 ‘ 𝑦 ) ‘ ( 𝑧 ∈ 𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) ) )
13 eqid ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
14 4 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ) ∧ ( 𝑉 ‘ 𝑥 ) = ( 𝑉 ‘ 𝑦 ) ) ∧ ¬ 𝑥 = 𝑦 ) → 𝐼 ∈ 𝑊 )
15 5 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ) ∧ ( 𝑉 ‘ 𝑥 ) = ( 𝑉 ‘ 𝑦 ) ) ∧ ¬ 𝑥 = 𝑦 ) → 𝑅 ∈ Ring )
16 simp2ll ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ) ∧ ( 𝑉 ‘ 𝑥 ) = ( 𝑉 ‘ 𝑦 ) ) ∧ ¬ 𝑥 = 𝑦 ) → 𝑥 ∈ 𝐼 )
17 2 13 6 7 14 15 16 mvrid ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ) ∧ ( 𝑉 ‘ 𝑥 ) = ( 𝑉 ‘ 𝑦 ) ) ∧ ¬ 𝑥 = 𝑦 ) → ( ( 𝑉 ‘ 𝑥 ) ‘ ( 𝑧 ∈ 𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) ) = 1 )
18 simp2lr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ) ∧ ( 𝑉 ‘ 𝑥 ) = ( 𝑉 ‘ 𝑦 ) ) ∧ ¬ 𝑥 = 𝑦 ) → 𝑦 ∈ 𝐼 )
19 1nn0 ⊢ 1 ∈ ℕ0
20 13 snifpsrbag ⊢ ( ( 𝐼 ∈ 𝑊 ∧ 1 ∈ ℕ0 ) → ( 𝑧 ∈ 𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
21 14 19 20 sylancl ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ) ∧ ( 𝑉 ‘ 𝑥 ) = ( 𝑉 ‘ 𝑦 ) ) ∧ ¬ 𝑥 = 𝑦 ) → ( 𝑧 ∈ 𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
22 2 13 6 7 14 15 18 21 mvrval2 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ) ∧ ( 𝑉 ‘ 𝑥 ) = ( 𝑉 ‘ 𝑦 ) ) ∧ ¬ 𝑥 = 𝑦 ) → ( ( 𝑉 ‘ 𝑦 ) ‘ ( 𝑧 ∈ 𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) ) = if ( ( 𝑧 ∈ 𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) = ( 𝑧 ∈ 𝐼 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) , 1 , 0 ) )
23 12 17 22 3eqtr3d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ) ∧ ( 𝑉 ‘ 𝑥 ) = ( 𝑉 ‘ 𝑦 ) ) ∧ ¬ 𝑥 = 𝑦 ) → 1 = if ( ( 𝑧 ∈ 𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) = ( 𝑧 ∈ 𝐼 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) , 1 , 0 ) )
24 simp3 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ) ∧ ( 𝑉 ‘ 𝑥 ) = ( 𝑉 ‘ 𝑦 ) ) ∧ ¬ 𝑥 = 𝑦 ) → ¬ 𝑥 = 𝑦 )
25 mpteqb ⊢ ( ∀ 𝑧 ∈ 𝐼 if ( 𝑧 = 𝑥 , 1 , 0 ) ∈ ℕ0 → ( ( 𝑧 ∈ 𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) = ( 𝑧 ∈ 𝐼 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) ↔ ∀ 𝑧 ∈ 𝐼 if ( 𝑧 = 𝑥 , 1 , 0 ) = if ( 𝑧 = 𝑦 , 1 , 0 ) ) )
26 0nn0 ⊢ 0 ∈ ℕ0
27 19 26 ifcli ⊢ if ( 𝑧 = 𝑥 , 1 , 0 ) ∈ ℕ0
28 27 a1i ⊢ ( 𝑧 ∈ 𝐼 → if ( 𝑧 = 𝑥 , 1 , 0 ) ∈ ℕ0 )
29 25 28 mprg ⊢ ( ( 𝑧 ∈ 𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) = ( 𝑧 ∈ 𝐼 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) ↔ ∀ 𝑧 ∈ 𝐼 if ( 𝑧 = 𝑥 , 1 , 0 ) = if ( 𝑧 = 𝑦 , 1 , 0 ) )
30 iftrue ⊢ ( 𝑧 = 𝑥 → if ( 𝑧 = 𝑥 , 1 , 0 ) = 1 )
31 eqeq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 = 𝑦 ↔ 𝑥 = 𝑦 ) )
32 31 ifbid ⊢ ( 𝑧 = 𝑥 → if ( 𝑧 = 𝑦 , 1 , 0 ) = if ( 𝑥 = 𝑦 , 1 , 0 ) )
33 30 32 eqeq12d ⊢ ( 𝑧 = 𝑥 → ( if ( 𝑧 = 𝑥 , 1 , 0 ) = if ( 𝑧 = 𝑦 , 1 , 0 ) ↔ 1 = if ( 𝑥 = 𝑦 , 1 , 0 ) ) )
34 33 rspcv ⊢ ( 𝑥 ∈ 𝐼 → ( ∀ 𝑧 ∈ 𝐼 if ( 𝑧 = 𝑥 , 1 , 0 ) = if ( 𝑧 = 𝑦 , 1 , 0 ) → 1 = if ( 𝑥 = 𝑦 , 1 , 0 ) ) )
35 29 34 syl5bi ⊢ ( 𝑥 ∈ 𝐼 → ( ( 𝑧 ∈ 𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) = ( 𝑧 ∈ 𝐼 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) → 1 = if ( 𝑥 = 𝑦 , 1 , 0 ) ) )
36 16 35 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ) ∧ ( 𝑉 ‘ 𝑥 ) = ( 𝑉 ‘ 𝑦 ) ) ∧ ¬ 𝑥 = 𝑦 ) → ( ( 𝑧 ∈ 𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) = ( 𝑧 ∈ 𝐼 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) → 1 = if ( 𝑥 = 𝑦 , 1 , 0 ) ) )
37 ax-1ne0 ⊢ 1 ≠ 0
38 eqeq1 ⊢ ( 1 = if ( 𝑥 = 𝑦 , 1 , 0 ) → ( 1 = 0 ↔ if ( 𝑥 = 𝑦 , 1 , 0 ) = 0 ) )
39 38 necon3abid ⊢ ( 1 = if ( 𝑥 = 𝑦 , 1 , 0 ) → ( 1 ≠ 0 ↔ ¬ if ( 𝑥 = 𝑦 , 1 , 0 ) = 0 ) )
40 37 39 mpbii ⊢ ( 1 = if ( 𝑥 = 𝑦 , 1 , 0 ) → ¬ if ( 𝑥 = 𝑦 , 1 , 0 ) = 0 )
41 iffalse ⊢ ( ¬ 𝑥 = 𝑦 → if ( 𝑥 = 𝑦 , 1 , 0 ) = 0 )
42 40 41 nsyl2 ⊢ ( 1 = if ( 𝑥 = 𝑦 , 1 , 0 ) → 𝑥 = 𝑦 )
43 36 42 syl6 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ) ∧ ( 𝑉 ‘ 𝑥 ) = ( 𝑉 ‘ 𝑦 ) ) ∧ ¬ 𝑥 = 𝑦 ) → ( ( 𝑧 ∈ 𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) = ( 𝑧 ∈ 𝐼 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) → 𝑥 = 𝑦 ) )
44 24 43 mtod ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ) ∧ ( 𝑉 ‘ 𝑥 ) = ( 𝑉 ‘ 𝑦 ) ) ∧ ¬ 𝑥 = 𝑦 ) → ¬ ( 𝑧 ∈ 𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) = ( 𝑧 ∈ 𝐼 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) )
45 iffalse ⊢ ( ¬ ( 𝑧 ∈ 𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) = ( 𝑧 ∈ 𝐼 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) → if ( ( 𝑧 ∈ 𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) = ( 𝑧 ∈ 𝐼 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) , 1 , 0 ) = 0 )
46 44 45 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ) ∧ ( 𝑉 ‘ 𝑥 ) = ( 𝑉 ‘ 𝑦 ) ) ∧ ¬ 𝑥 = 𝑦 ) → if ( ( 𝑧 ∈ 𝐼 ↦ if ( 𝑧 = 𝑥 , 1 , 0 ) ) = ( 𝑧 ∈ 𝐼 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) , 1 , 0 ) = 0 )
47 23 46 eqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ) ∧ ( 𝑉 ‘ 𝑥 ) = ( 𝑉 ‘ 𝑦 ) ) ∧ ¬ 𝑥 = 𝑦 ) → 1 = 0 )
48 47 3expia ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ) ∧ ( 𝑉 ‘ 𝑥 ) = ( 𝑉 ‘ 𝑦 ) ) ) → ( ¬ 𝑥 = 𝑦 → 1 = 0 ) )
49 48 necon1ad ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ) ∧ ( 𝑉 ‘ 𝑥 ) = ( 𝑉 ‘ 𝑦 ) ) ) → ( 1 ≠ 0 → 𝑥 = 𝑦 ) )
50 10 49 mpd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ) ∧ ( 𝑉 ‘ 𝑥 ) = ( 𝑉 ‘ 𝑦 ) ) ) → 𝑥 = 𝑦 )
51 50 expr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ) ) → ( ( 𝑉 ‘ 𝑥 ) = ( 𝑉 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
52 51 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝐼 ( ( 𝑉 ‘ 𝑥 ) = ( 𝑉 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
53 dff13 ⊢ ( 𝑉 : 𝐼 –1-1→ 𝐵 ↔ ( 𝑉 : 𝐼 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝐼 ( ( 𝑉 ‘ 𝑥 ) = ( 𝑉 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
54 9 52 53 sylanbrc ⊢ ( 𝜑 → 𝑉 : 𝐼 –1-1→ 𝐵 )