Step |
Hyp |
Ref |
Expression |
1 |
|
drngmcl.b |
⊢ 𝐵 = ( Base ‘ 𝑅 ) |
2 |
|
drngmcl.t |
⊢ · = ( .r ‘ 𝑅 ) |
3 |
|
drngmcl.z |
⊢ 0 = ( 0g ‘ 𝑅 ) |
4 |
|
eqid |
⊢ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) = ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) |
5 |
1 3 4
|
drngmgp |
⊢ ( 𝑅 ∈ DivRing → ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp ) |
6 |
|
difss |
⊢ ( 𝐵 ∖ { 0 } ) ⊆ 𝐵 |
7 |
|
eqid |
⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 ) |
8 |
7 1
|
mgpbas |
⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) ) |
9 |
4 8
|
ressbas2 |
⊢ ( ( 𝐵 ∖ { 0 } ) ⊆ 𝐵 → ( 𝐵 ∖ { 0 } ) = ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) ) |
10 |
6 9
|
ax-mp |
⊢ ( 𝐵 ∖ { 0 } ) = ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) |
11 |
1
|
fvexi |
⊢ 𝐵 ∈ V |
12 |
|
difexg |
⊢ ( 𝐵 ∈ V → ( 𝐵 ∖ { 0 } ) ∈ V ) |
13 |
7 2
|
mgpplusg |
⊢ · = ( +g ‘ ( mulGrp ‘ 𝑅 ) ) |
14 |
4 13
|
ressplusg |
⊢ ( ( 𝐵 ∖ { 0 } ) ∈ V → · = ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) ) |
15 |
11 12 14
|
mp2b |
⊢ · = ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) |
16 |
10 15
|
grpcl |
⊢ ( ( ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp ∧ 𝑋 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑌 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑋 · 𝑌 ) ∈ ( 𝐵 ∖ { 0 } ) ) |
17 |
5 16
|
syl3an1 |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑋 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑌 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑋 · 𝑌 ) ∈ ( 𝐵 ∖ { 0 } ) ) |