Step |
Hyp |
Ref |
Expression |
1 |
|
isdivrng1.1 |
⊢ 𝐺 = ( 1st ‘ 𝑅 ) |
2 |
|
isdivrng1.2 |
⊢ 𝐻 = ( 2nd ‘ 𝑅 ) |
3 |
|
isdivrng1.3 |
⊢ 𝑍 = ( GId ‘ 𝐺 ) |
4 |
|
isdivrng1.4 |
⊢ 𝑋 = ran 𝐺 |
5 |
|
df-drngo |
⊢ DivRingOps = { 〈 𝑔 , ℎ 〉 ∣ ( 〈 𝑔 , ℎ 〉 ∈ RingOps ∧ ( ℎ ↾ ( ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) × ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) ) ) ∈ GrpOp ) } |
6 |
5
|
relopabi |
⊢ Rel DivRingOps |
7 |
|
1st2nd |
⊢ ( ( Rel DivRingOps ∧ 𝑅 ∈ DivRingOps ) → 𝑅 = 〈 ( 1st ‘ 𝑅 ) , ( 2nd ‘ 𝑅 ) 〉 ) |
8 |
6 7
|
mpan |
⊢ ( 𝑅 ∈ DivRingOps → 𝑅 = 〈 ( 1st ‘ 𝑅 ) , ( 2nd ‘ 𝑅 ) 〉 ) |
9 |
|
relrngo |
⊢ Rel RingOps |
10 |
|
1st2nd |
⊢ ( ( Rel RingOps ∧ 𝑅 ∈ RingOps ) → 𝑅 = 〈 ( 1st ‘ 𝑅 ) , ( 2nd ‘ 𝑅 ) 〉 ) |
11 |
9 10
|
mpan |
⊢ ( 𝑅 ∈ RingOps → 𝑅 = 〈 ( 1st ‘ 𝑅 ) , ( 2nd ‘ 𝑅 ) 〉 ) |
12 |
11
|
adantr |
⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) → 𝑅 = 〈 ( 1st ‘ 𝑅 ) , ( 2nd ‘ 𝑅 ) 〉 ) |
13 |
1 2
|
opeq12i |
⊢ 〈 𝐺 , 𝐻 〉 = 〈 ( 1st ‘ 𝑅 ) , ( 2nd ‘ 𝑅 ) 〉 |
14 |
13
|
eqeq2i |
⊢ ( 𝑅 = 〈 𝐺 , 𝐻 〉 ↔ 𝑅 = 〈 ( 1st ‘ 𝑅 ) , ( 2nd ‘ 𝑅 ) 〉 ) |
15 |
2
|
fvexi |
⊢ 𝐻 ∈ V |
16 |
|
isdivrngo |
⊢ ( 𝐻 ∈ V → ( 〈 𝐺 , 𝐻 〉 ∈ DivRingOps ↔ ( 〈 𝐺 , 𝐻 〉 ∈ RingOps ∧ ( 𝐻 ↾ ( ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) × ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) ) ) ∈ GrpOp ) ) ) |
17 |
15 16
|
ax-mp |
⊢ ( 〈 𝐺 , 𝐻 〉 ∈ DivRingOps ↔ ( 〈 𝐺 , 𝐻 〉 ∈ RingOps ∧ ( 𝐻 ↾ ( ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) × ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) ) ) ∈ GrpOp ) ) |
18 |
3
|
sneqi |
⊢ { 𝑍 } = { ( GId ‘ 𝐺 ) } |
19 |
4 18
|
difeq12i |
⊢ ( 𝑋 ∖ { 𝑍 } ) = ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) |
20 |
19 19
|
xpeq12i |
⊢ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) = ( ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) × ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) ) |
21 |
20
|
reseq2i |
⊢ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) = ( 𝐻 ↾ ( ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) × ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) ) ) |
22 |
21
|
eleq1i |
⊢ ( ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ↔ ( 𝐻 ↾ ( ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) × ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) ) ) ∈ GrpOp ) |
23 |
22
|
anbi2i |
⊢ ( ( 〈 𝐺 , 𝐻 〉 ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) ↔ ( 〈 𝐺 , 𝐻 〉 ∈ RingOps ∧ ( 𝐻 ↾ ( ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) × ( ran 𝐺 ∖ { ( GId ‘ 𝐺 ) } ) ) ) ∈ GrpOp ) ) |
24 |
17 23
|
bitr4i |
⊢ ( 〈 𝐺 , 𝐻 〉 ∈ DivRingOps ↔ ( 〈 𝐺 , 𝐻 〉 ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) ) |
25 |
|
eleq1 |
⊢ ( 𝑅 = 〈 𝐺 , 𝐻 〉 → ( 𝑅 ∈ DivRingOps ↔ 〈 𝐺 , 𝐻 〉 ∈ DivRingOps ) ) |
26 |
|
eleq1 |
⊢ ( 𝑅 = 〈 𝐺 , 𝐻 〉 → ( 𝑅 ∈ RingOps ↔ 〈 𝐺 , 𝐻 〉 ∈ RingOps ) ) |
27 |
26
|
anbi1d |
⊢ ( 𝑅 = 〈 𝐺 , 𝐻 〉 → ( ( 𝑅 ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) ↔ ( 〈 𝐺 , 𝐻 〉 ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) ) ) |
28 |
25 27
|
bibi12d |
⊢ ( 𝑅 = 〈 𝐺 , 𝐻 〉 → ( ( 𝑅 ∈ DivRingOps ↔ ( 𝑅 ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) ) ↔ ( 〈 𝐺 , 𝐻 〉 ∈ DivRingOps ↔ ( 〈 𝐺 , 𝐻 〉 ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) ) ) ) |
29 |
24 28
|
mpbiri |
⊢ ( 𝑅 = 〈 𝐺 , 𝐻 〉 → ( 𝑅 ∈ DivRingOps ↔ ( 𝑅 ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) ) ) |
30 |
14 29
|
sylbir |
⊢ ( 𝑅 = 〈 ( 1st ‘ 𝑅 ) , ( 2nd ‘ 𝑅 ) 〉 → ( 𝑅 ∈ DivRingOps ↔ ( 𝑅 ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) ) ) |
31 |
8 12 30
|
pm5.21nii |
⊢ ( 𝑅 ∈ DivRingOps ↔ ( 𝑅 ∈ RingOps ∧ ( 𝐻 ↾ ( ( 𝑋 ∖ { 𝑍 } ) × ( 𝑋 ∖ { 𝑍 } ) ) ) ∈ GrpOp ) ) |