Step |
Hyp |
Ref |
Expression |
0 |
|
cdrng |
⊢ DivRingOps |
1 |
|
vg |
⊢ 𝑔 |
2 |
|
vh |
⊢ ℎ |
3 |
1
|
cv |
⊢ 𝑔 |
4 |
2
|
cv |
⊢ ℎ |
5 |
3 4
|
cop |
⊢ 〈 𝑔 , ℎ 〉 |
6 |
|
crngo |
⊢ RingOps |
7 |
5 6
|
wcel |
⊢ 〈 𝑔 , ℎ 〉 ∈ RingOps |
8 |
3
|
crn |
⊢ ran 𝑔 |
9 |
|
cgi |
⊢ GId |
10 |
3 9
|
cfv |
⊢ ( GId ‘ 𝑔 ) |
11 |
10
|
csn |
⊢ { ( GId ‘ 𝑔 ) } |
12 |
8 11
|
cdif |
⊢ ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) |
13 |
12 12
|
cxp |
⊢ ( ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) × ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) ) |
14 |
4 13
|
cres |
⊢ ( ℎ ↾ ( ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) × ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) ) ) |
15 |
|
cgr |
⊢ GrpOp |
16 |
14 15
|
wcel |
⊢ ( ℎ ↾ ( ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) × ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) ) ) ∈ GrpOp |
17 |
7 16
|
wa |
⊢ ( 〈 𝑔 , ℎ 〉 ∈ RingOps ∧ ( ℎ ↾ ( ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) × ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) ) ) ∈ GrpOp ) |
18 |
17 1 2
|
copab |
⊢ { 〈 𝑔 , ℎ 〉 ∣ ( 〈 𝑔 , ℎ 〉 ∈ RingOps ∧ ( ℎ ↾ ( ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) × ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) ) ) ∈ GrpOp ) } |
19 |
0 18
|
wceq |
⊢ DivRingOps = { 〈 𝑔 , ℎ 〉 ∣ ( 〈 𝑔 , ℎ 〉 ∈ RingOps ∧ ( ℎ ↾ ( ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) × ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) ) ) ∈ GrpOp ) } |