Description: The value of an image structure's ring multiplication. (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 ‘ 𝑈 ) | ||
Assertion | imasmulval | ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑋 ) ∙ ( 𝐹 ‘ 𝑌 ) ) = ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) ) |
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 | 3 4 1 5 6 7 | imasmulr | ⊢ ( 𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { 〈 〈 ( 𝐹 ‘ 𝑝 ) , ( 𝐹 ‘ 𝑞 ) 〉 , ( 𝐹 ‘ ( 𝑝 · 𝑞 ) ) 〉 } ) |
9 | 1 2 8 | imasaddvallem | ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑋 ) ∙ ( 𝐹 ‘ 𝑌 ) ) = ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) ) |