Step |
Hyp |
Ref |
Expression |
1 |
|
srngcl.i |
⊢ ∗ = ( *𝑟 ‘ 𝑅 ) |
2 |
|
srngcl.b |
⊢ 𝐵 = ( Base ‘ 𝑅 ) |
3 |
|
eqid |
⊢ ( *rf ‘ 𝑅 ) = ( *rf ‘ 𝑅 ) |
4 |
2 1 3
|
stafval |
⊢ ( 𝑋 ∈ 𝐵 → ( ( *rf ‘ 𝑅 ) ‘ 𝑋 ) = ( ∗ ‘ 𝑋 ) ) |
5 |
4
|
adantl |
⊢ ( ( 𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵 ) → ( ( *rf ‘ 𝑅 ) ‘ 𝑋 ) = ( ∗ ‘ 𝑋 ) ) |
6 |
3 2
|
srngf1o |
⊢ ( 𝑅 ∈ *-Ring → ( *rf ‘ 𝑅 ) : 𝐵 –1-1-onto→ 𝐵 ) |
7 |
|
f1of |
⊢ ( ( *rf ‘ 𝑅 ) : 𝐵 –1-1-onto→ 𝐵 → ( *rf ‘ 𝑅 ) : 𝐵 ⟶ 𝐵 ) |
8 |
6 7
|
syl |
⊢ ( 𝑅 ∈ *-Ring → ( *rf ‘ 𝑅 ) : 𝐵 ⟶ 𝐵 ) |
9 |
8
|
ffvelrnda |
⊢ ( ( 𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵 ) → ( ( *rf ‘ 𝑅 ) ‘ 𝑋 ) ∈ 𝐵 ) |
10 |
5 9
|
eqeltrrd |
⊢ ( ( 𝑅 ∈ *-Ring ∧ 𝑋 ∈ 𝐵 ) → ( ∗ ‘ 𝑋 ) ∈ 𝐵 ) |