| Step | Hyp | Ref
| Expression |
| 1 | | mvrf.s |
. . 3
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
| 2 | | mvrf.v |
. . 3
⊢ 𝑉 = (𝐼 mVar 𝑅) |
| 3 | | mvrf.b |
. . 3
⊢ 𝐵 = (Base‘𝑆) |
| 4 | | mvrf.i |
. . 3
⊢ (𝜑 → 𝐼 ∈ 𝑊) |
| 5 | | mvrf.r |
. . 3
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 6 | 1, 2, 3, 4, 5 | mvrf 22005 |
. 2
⊢ (𝜑 → 𝑉:𝐼⟶𝐵) |
| 7 | | mvrf1.n |
. . . . . 6
⊢ (𝜑 → 1 ≠ 0 ) |
| 8 | 7 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼) ∧ (𝑉‘𝑥) = (𝑉‘𝑦))) → 1 ≠ 0 ) |
| 9 | | simp2r 1201 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼) ∧ (𝑉‘𝑥) = (𝑉‘𝑦)) ∧ ¬ 𝑥 = 𝑦) → (𝑉‘𝑥) = (𝑉‘𝑦)) |
| 10 | 9 | fveq1d 6908 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼) ∧ (𝑉‘𝑥) = (𝑉‘𝑦)) ∧ ¬ 𝑥 = 𝑦) → ((𝑉‘𝑥)‘(𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0))) = ((𝑉‘𝑦)‘(𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)))) |
| 11 | | eqid 2737 |
. . . . . . . . . 10
⊢ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} = {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} |
| 12 | | mvrf1.z |
. . . . . . . . . 10
⊢ 0 =
(0g‘𝑅) |
| 13 | | mvrf1.o |
. . . . . . . . . 10
⊢ 1 =
(1r‘𝑅) |
| 14 | 4 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼) ∧ (𝑉‘𝑥) = (𝑉‘𝑦)) ∧ ¬ 𝑥 = 𝑦) → 𝐼 ∈ 𝑊) |
| 15 | 5 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼) ∧ (𝑉‘𝑥) = (𝑉‘𝑦)) ∧ ¬ 𝑥 = 𝑦) → 𝑅 ∈ Ring) |
| 16 | | simp2ll 1241 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼) ∧ (𝑉‘𝑥) = (𝑉‘𝑦)) ∧ ¬ 𝑥 = 𝑦) → 𝑥 ∈ 𝐼) |
| 17 | 2, 11, 12, 13, 14, 15, 16 | mvrid 22004 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼) ∧ (𝑉‘𝑥) = (𝑉‘𝑦)) ∧ ¬ 𝑥 = 𝑦) → ((𝑉‘𝑥)‘(𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0))) = 1 ) |
| 18 | | simp2lr 1242 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼) ∧ (𝑉‘𝑥) = (𝑉‘𝑦)) ∧ ¬ 𝑥 = 𝑦) → 𝑦 ∈ 𝐼) |
| 19 | | 1nn0 12542 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ0 |
| 20 | 11 | snifpsrbag 21940 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑊 ∧ 1 ∈ ℕ0) →
(𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
| 21 | 14, 19, 20 | sylancl 586 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼) ∧ (𝑉‘𝑥) = (𝑉‘𝑦)) ∧ ¬ 𝑥 = 𝑦) → (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
| 22 | 2, 11, 12, 13, 14, 15, 18, 21 | mvrval2 22003 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼) ∧ (𝑉‘𝑥) = (𝑉‘𝑦)) ∧ ¬ 𝑥 = 𝑦) → ((𝑉‘𝑦)‘(𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0))) = if((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑦, 1, 0)), 1 , 0 )) |
| 23 | 10, 17, 22 | 3eqtr3d 2785 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼) ∧ (𝑉‘𝑥) = (𝑉‘𝑦)) ∧ ¬ 𝑥 = 𝑦) → 1 = if((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑦, 1, 0)), 1 , 0 )) |
| 24 | | simp3 1139 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼) ∧ (𝑉‘𝑥) = (𝑉‘𝑦)) ∧ ¬ 𝑥 = 𝑦) → ¬ 𝑥 = 𝑦) |
| 25 | | mpteqb 7035 |
. . . . . . . . . . . . . 14
⊢
(∀𝑧 ∈
𝐼 if(𝑧 = 𝑥, 1, 0) ∈ ℕ0 →
((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑦, 1, 0)) ↔ ∀𝑧 ∈ 𝐼 if(𝑧 = 𝑥, 1, 0) = if(𝑧 = 𝑦, 1, 0))) |
| 26 | | 0nn0 12541 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℕ0 |
| 27 | 19, 26 | ifcli 4573 |
. . . . . . . . . . . . . . 15
⊢ if(𝑧 = 𝑥, 1, 0) ∈
ℕ0 |
| 28 | 27 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ 𝐼 → if(𝑧 = 𝑥, 1, 0) ∈
ℕ0) |
| 29 | 25, 28 | mprg 3067 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑦, 1, 0)) ↔ ∀𝑧 ∈ 𝐼 if(𝑧 = 𝑥, 1, 0) = if(𝑧 = 𝑦, 1, 0)) |
| 30 | | iftrue 4531 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑥 → if(𝑧 = 𝑥, 1, 0) = 1) |
| 31 | | eqeq1 2741 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑥 → (𝑧 = 𝑦 ↔ 𝑥 = 𝑦)) |
| 32 | 31 | ifbid 4549 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑥 → if(𝑧 = 𝑦, 1, 0) = if(𝑥 = 𝑦, 1, 0)) |
| 33 | 30, 32 | eqeq12d 2753 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑥 → (if(𝑧 = 𝑥, 1, 0) = if(𝑧 = 𝑦, 1, 0) ↔ 1 = if(𝑥 = 𝑦, 1, 0))) |
| 34 | 33 | rspcv 3618 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐼 → (∀𝑧 ∈ 𝐼 if(𝑧 = 𝑥, 1, 0) = if(𝑧 = 𝑦, 1, 0) → 1 = if(𝑥 = 𝑦, 1, 0))) |
| 35 | 29, 34 | biimtrid 242 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐼 → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑦, 1, 0)) → 1 = if(𝑥 = 𝑦, 1, 0))) |
| 36 | 16, 35 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼) ∧ (𝑉‘𝑥) = (𝑉‘𝑦)) ∧ ¬ 𝑥 = 𝑦) → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑦, 1, 0)) → 1 = if(𝑥 = 𝑦, 1, 0))) |
| 37 | | ax-1ne0 11224 |
. . . . . . . . . . . . 13
⊢ 1 ≠
0 |
| 38 | | eqeq1 2741 |
. . . . . . . . . . . . . 14
⊢ (1 =
if(𝑥 = 𝑦, 1, 0) → (1 = 0 ↔ if(𝑥 = 𝑦, 1, 0) = 0)) |
| 39 | 38 | necon3abid 2977 |
. . . . . . . . . . . . 13
⊢ (1 =
if(𝑥 = 𝑦, 1, 0) → (1 ≠ 0 ↔ ¬
if(𝑥 = 𝑦, 1, 0) = 0)) |
| 40 | 37, 39 | mpbii 233 |
. . . . . . . . . . . 12
⊢ (1 =
if(𝑥 = 𝑦, 1, 0) → ¬ if(𝑥 = 𝑦, 1, 0) = 0) |
| 41 | | iffalse 4534 |
. . . . . . . . . . . 12
⊢ (¬
𝑥 = 𝑦 → if(𝑥 = 𝑦, 1, 0) = 0) |
| 42 | 40, 41 | nsyl2 141 |
. . . . . . . . . . 11
⊢ (1 =
if(𝑥 = 𝑦, 1, 0) → 𝑥 = 𝑦) |
| 43 | 36, 42 | syl6 35 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼) ∧ (𝑉‘𝑥) = (𝑉‘𝑦)) ∧ ¬ 𝑥 = 𝑦) → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑦, 1, 0)) → 𝑥 = 𝑦)) |
| 44 | 24, 43 | mtod 198 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼) ∧ (𝑉‘𝑥) = (𝑉‘𝑦)) ∧ ¬ 𝑥 = 𝑦) → ¬ (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑦, 1, 0))) |
| 45 | | iffalse 4534 |
. . . . . . . . 9
⊢ (¬
(𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑦, 1, 0)) → if((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑦, 1, 0)), 1 , 0 ) = 0 ) |
| 46 | 44, 45 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼) ∧ (𝑉‘𝑥) = (𝑉‘𝑦)) ∧ ¬ 𝑥 = 𝑦) → if((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑦, 1, 0)), 1 , 0 ) = 0 ) |
| 47 | 23, 46 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼) ∧ (𝑉‘𝑥) = (𝑉‘𝑦)) ∧ ¬ 𝑥 = 𝑦) → 1 = 0 ) |
| 48 | 47 | 3expia 1122 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼) ∧ (𝑉‘𝑥) = (𝑉‘𝑦))) → (¬ 𝑥 = 𝑦 → 1 = 0 )) |
| 49 | 48 | necon1ad 2957 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼) ∧ (𝑉‘𝑥) = (𝑉‘𝑦))) → ( 1 ≠ 0 → 𝑥 = 𝑦)) |
| 50 | 8, 49 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼) ∧ (𝑉‘𝑥) = (𝑉‘𝑦))) → 𝑥 = 𝑦) |
| 51 | 50 | expr 456 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼)) → ((𝑉‘𝑥) = (𝑉‘𝑦) → 𝑥 = 𝑦)) |
| 52 | 51 | ralrimivva 3202 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝐼 ∀𝑦 ∈ 𝐼 ((𝑉‘𝑥) = (𝑉‘𝑦) → 𝑥 = 𝑦)) |
| 53 | | dff13 7275 |
. 2
⊢ (𝑉:𝐼–1-1→𝐵 ↔ (𝑉:𝐼⟶𝐵 ∧ ∀𝑥 ∈ 𝐼 ∀𝑦 ∈ 𝐼 ((𝑉‘𝑥) = (𝑉‘𝑦) → 𝑥 = 𝑦))) |
| 54 | 6, 52, 53 | sylanbrc 583 |
1
⊢ (𝜑 → 𝑉:𝐼–1-1→𝐵) |