Step |
Hyp |
Ref |
Expression |
1 |
|
qusaddf.u |
⊢ ( 𝜑 → 𝑈 = ( 𝑅 /s ∼ ) ) |
2 |
|
qusaddf.v |
⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) ) |
3 |
|
qusaddf.r |
⊢ ( 𝜑 → ∼ Er 𝑉 ) |
4 |
|
qusaddf.z |
⊢ ( 𝜑 → 𝑅 ∈ 𝑍 ) |
5 |
|
qusaddf.e |
⊢ ( 𝜑 → ( ( 𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞 ) → ( 𝑎 · 𝑏 ) ∼ ( 𝑝 · 𝑞 ) ) ) |
6 |
|
qusaddf.c |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( 𝑝 · 𝑞 ) ∈ 𝑉 ) |
7 |
|
qusmulf.p |
⊢ · = ( .r ‘ 𝑅 ) |
8 |
|
qusmulf.a |
⊢ ∙ = ( .r ‘ 𝑈 ) |
9 |
|
eqid |
⊢ ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ ) = ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ ) |
10 |
|
fvex |
⊢ ( Base ‘ 𝑅 ) ∈ V |
11 |
2 10
|
eqeltrdi |
⊢ ( 𝜑 → 𝑉 ∈ V ) |
12 |
|
erex |
⊢ ( ∼ Er 𝑉 → ( 𝑉 ∈ V → ∼ ∈ V ) ) |
13 |
3 11 12
|
sylc |
⊢ ( 𝜑 → ∼ ∈ V ) |
14 |
1 2 9 13 4
|
qusval |
⊢ ( 𝜑 → 𝑈 = ( ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ ) “s 𝑅 ) ) |
15 |
1 2 9 13 4
|
quslem |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ ) : 𝑉 –onto→ ( 𝑉 / ∼ ) ) |
16 |
14 2 15 4 7 8
|
imasmulr |
⊢ ( 𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 { 〈 〈 ( ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ ) ‘ 𝑝 ) , ( ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ ) ‘ 𝑞 ) 〉 , ( ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ ) ‘ ( 𝑝 · 𝑞 ) ) 〉 } ) |
17 |
1 2 3 4 5 6 9 16
|
qusaddflem |
⊢ ( 𝜑 → ∙ : ( ( 𝑉 / ∼ ) × ( 𝑉 / ∼ ) ) ⟶ ( 𝑉 / ∼ ) ) |