Description: The image structure's ring multiplication is closed in the base set. (Contributed by Mario Carneiro, 23-Feb-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | imasaddf.f | ⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 ) | |
| imasaddf.e | ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 · 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ) | ||
| imasaddf.u | ⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) ) | ||
| imasaddf.v | ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) ) | ||
| imasaddf.r | ⊢ ( 𝜑 → 𝑅 ∈ 𝑍 ) | ||
| imasmulf.p | ⊢ · = ( .r ‘ 𝑅 ) | ||
| imasmulf.a | ⊢ ∙ = ( .r ‘ 𝑈 ) | ||
| imasmulf.c | ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( 𝑝 · 𝑞 ) ∈ 𝑉 ) | ||
| Assertion | imasmulf | ⊢ ( 𝜑 → ∙ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imasaddf.f | ⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 ) | |
| 2 | imasaddf.e | ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 · 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ) ) | |
| 3 | imasaddf.u | ⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) ) | |
| 4 | imasaddf.v | ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) ) | |
| 5 | imasaddf.r | ⊢ ( 𝜑 → 𝑅 ∈ 𝑍 ) | |
| 6 | imasmulf.p | ⊢ · = ( .r ‘ 𝑅 ) | |
| 7 | imasmulf.a | ⊢ ∙ = ( .r ‘ 𝑈 ) | |
| 8 | imasmulf.c | ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( 𝑝 · 𝑞 ) ∈ 𝑉 ) | |
| 9 | 3 4 1 5 6 7 | imasmulr | ⊢ ( 𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { ⟨ ⟨ ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) ⟩ , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) ⟩ } ) |
| 10 | 1 2 9 8 | imasaddflem | ⊢ ( 𝜑 → ∙ : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ) |