Step |
Hyp |
Ref |
Expression |
1 |
|
ply1scl.p |
⊢ 𝑃 = ( Poly1 ‘ 𝑅 ) |
2 |
|
ply1scl.a |
⊢ 𝐴 = ( algSc ‘ 𝑃 ) |
3 |
|
ply1sclid.k |
⊢ 𝐾 = ( Base ‘ 𝑅 ) |
4 |
|
ply1sclf1.b |
⊢ 𝐵 = ( Base ‘ 𝑃 ) |
5 |
1 2 3 4
|
ply1sclf |
⊢ ( 𝑅 ∈ Ring → 𝐴 : 𝐾 ⟶ 𝐵 ) |
6 |
|
fveq2 |
⊢ ( ( 𝐴 ‘ 𝑥 ) = ( 𝐴 ‘ 𝑦 ) → ( coe1 ‘ ( 𝐴 ‘ 𝑥 ) ) = ( coe1 ‘ ( 𝐴 ‘ 𝑦 ) ) ) |
7 |
6
|
fveq1d |
⊢ ( ( 𝐴 ‘ 𝑥 ) = ( 𝐴 ‘ 𝑦 ) → ( ( coe1 ‘ ( 𝐴 ‘ 𝑥 ) ) ‘ 0 ) = ( ( coe1 ‘ ( 𝐴 ‘ 𝑦 ) ) ‘ 0 ) ) |
8 |
1 2 3
|
ply1sclid |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐾 ) → 𝑥 = ( ( coe1 ‘ ( 𝐴 ‘ 𝑥 ) ) ‘ 0 ) ) |
9 |
8
|
adantrr |
⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → 𝑥 = ( ( coe1 ‘ ( 𝐴 ‘ 𝑥 ) ) ‘ 0 ) ) |
10 |
1 2 3
|
ply1sclid |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐾 ) → 𝑦 = ( ( coe1 ‘ ( 𝐴 ‘ 𝑦 ) ) ‘ 0 ) ) |
11 |
10
|
adantrl |
⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → 𝑦 = ( ( coe1 ‘ ( 𝐴 ‘ 𝑦 ) ) ‘ 0 ) ) |
12 |
9 11
|
eqeq12d |
⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝑥 = 𝑦 ↔ ( ( coe1 ‘ ( 𝐴 ‘ 𝑥 ) ) ‘ 0 ) = ( ( coe1 ‘ ( 𝐴 ‘ 𝑦 ) ) ‘ 0 ) ) ) |
13 |
7 12
|
syl5ibr |
⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( ( 𝐴 ‘ 𝑥 ) = ( 𝐴 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) |
14 |
13
|
ralrimivva |
⊢ ( 𝑅 ∈ Ring → ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ( ( 𝐴 ‘ 𝑥 ) = ( 𝐴 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) |
15 |
|
dff13 |
⊢ ( 𝐴 : 𝐾 –1-1→ 𝐵 ↔ ( 𝐴 : 𝐾 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ( ( 𝐴 ‘ 𝑥 ) = ( 𝐴 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) ) |
16 |
5 14 15
|
sylanbrc |
⊢ ( 𝑅 ∈ Ring → 𝐴 : 𝐾 –1-1→ 𝐵 ) |