| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fveq2 6906 | . . 3
⊢ (𝑓 = ( Frac ‘𝑅) → (SubRing‘𝑓) = (SubRing‘( Frac
‘𝑅))) | 
| 2 |  | oveq1 7438 | . . . 4
⊢ (𝑓 = ( Frac ‘𝑅) → (𝑓 ↾s 𝑠) = (( Frac ‘𝑅) ↾s 𝑠)) | 
| 3 | 2 | breq2d 5155 | . . 3
⊢ (𝑓 = ( Frac ‘𝑅) → (𝑅 ≃𝑟 (𝑓 ↾s 𝑠) ↔ 𝑅 ≃𝑟 (( Frac
‘𝑅)
↾s 𝑠))) | 
| 4 | 1, 3 | rexeqbidv 3347 | . 2
⊢ (𝑓 = ( Frac ‘𝑅) → (∃𝑠 ∈ (SubRing‘𝑓)𝑅 ≃𝑟 (𝑓 ↾s 𝑠) ↔ ∃𝑠 ∈ (SubRing‘( Frac
‘𝑅))𝑅 ≃𝑟 (( Frac
‘𝑅)
↾s 𝑠))) | 
| 5 |  | idomsubr.1 | . . 3
⊢ (𝜑 → 𝑅 ∈ IDomn) | 
| 6 | 5 | fracfld 33310 | . 2
⊢ (𝜑 → ( Frac ‘𝑅) ∈ Field) | 
| 7 |  | oveq2 7439 | . . . 4
⊢ (𝑠 = ran (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) → (( Frac ‘𝑅) ↾s 𝑠) = (( Frac ‘𝑅) ↾s ran (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))))) | 
| 8 | 7 | breq2d 5155 | . . 3
⊢ (𝑠 = ran (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) → (𝑅 ≃𝑟 (( Frac
‘𝑅)
↾s 𝑠)
↔ 𝑅
≃𝑟 (( Frac ‘𝑅) ↾s ran (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)))))) | 
| 9 |  | eqid 2737 | . . . . 5
⊢
(Base‘𝑅) =
(Base‘𝑅) | 
| 10 |  | eqid 2737 | . . . . 5
⊢
(RLReg‘𝑅) =
(RLReg‘𝑅) | 
| 11 |  | eqid 2737 | . . . . 5
⊢
(1r‘𝑅) = (1r‘𝑅) | 
| 12 | 5 | idomcringd 20727 | . . . . 5
⊢ (𝜑 → 𝑅 ∈ CRing) | 
| 13 |  | eqid 2737 | . . . . 5
⊢ (𝑅 ~RL
(RLReg‘𝑅)) = (𝑅 ~RL
(RLReg‘𝑅)) | 
| 14 |  | opeq1 4873 | . . . . . . 7
⊢ (𝑥 = 𝑦 → 〈𝑥, (1r‘𝑅)〉 = 〈𝑦, (1r‘𝑅)〉) | 
| 15 | 14 | eceq1d 8785 | . . . . . 6
⊢ (𝑥 = 𝑦 → [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)) = [〈𝑦, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) | 
| 16 | 15 | cbvmptv 5255 | . . . . 5
⊢ (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) = (𝑦 ∈ (Base‘𝑅) ↦ [〈𝑦, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) | 
| 17 | 9, 10, 11, 12, 13, 16 | fracf1 33309 | . . . 4
⊢ (𝜑 → ((𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))):(Base‘𝑅)–1-1→(((Base‘𝑅) × (RLReg‘𝑅)) / (𝑅 ~RL (RLReg‘𝑅))) ∧ (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∈ (𝑅 RingHom ( Frac ‘𝑅)))) | 
| 18 |  | rnrhmsubrg 20605 | . . . 4
⊢ ((𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∈ (𝑅 RingHom ( Frac ‘𝑅)) → ran (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∈ (SubRing‘( Frac
‘𝑅))) | 
| 19 | 17, 18 | simpl2im 503 | . . 3
⊢ (𝜑 → ran (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∈ (SubRing‘( Frac
‘𝑅))) | 
| 20 |  | ssidd 4007 | . . . . . 6
⊢ (𝜑 → ran (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ⊆ ran (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)))) | 
| 21 | 17 | simprd 495 | . . . . . 6
⊢ (𝜑 → (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∈ (𝑅 RingHom ( Frac ‘𝑅))) | 
| 22 |  | eqid 2737 | . . . . . . . 8
⊢ (( Frac
‘𝑅)
↾s ran (𝑥
∈ (Base‘𝑅)
↦ [〈𝑥,
(1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)))) = (( Frac ‘𝑅) ↾s ran (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)))) | 
| 23 | 22 | resrhm2b 20602 | . . . . . . 7
⊢ ((ran
(𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∈ (SubRing‘( Frac
‘𝑅)) ∧ ran (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ⊆ ran (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)))) → ((𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∈ (𝑅 RingHom ( Frac ‘𝑅)) ↔ (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∈ (𝑅 RingHom (( Frac ‘𝑅) ↾s ran (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))))))) | 
| 24 | 23 | biimpa 476 | . . . . . 6
⊢ (((ran
(𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∈ (SubRing‘( Frac
‘𝑅)) ∧ ran (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ⊆ ran (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)))) ∧ (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∈ (𝑅 RingHom ( Frac ‘𝑅))) → (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∈ (𝑅 RingHom (( Frac ‘𝑅) ↾s ran (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)))))) | 
| 25 | 19, 20, 21, 24 | syl21anc 838 | . . . . 5
⊢ (𝜑 → (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∈ (𝑅 RingHom (( Frac ‘𝑅) ↾s ran (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)))))) | 
| 26 | 17 | simpld 494 | . . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))):(Base‘𝑅)–1-1→(((Base‘𝑅) × (RLReg‘𝑅)) / (𝑅 ~RL (RLReg‘𝑅)))) | 
| 27 |  | f1f1orn 6859 | . . . . . . 7
⊢ ((𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))):(Base‘𝑅)–1-1→(((Base‘𝑅) × (RLReg‘𝑅)) / (𝑅 ~RL (RLReg‘𝑅))) → (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))):(Base‘𝑅)–1-1-onto→ran
(𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)))) | 
| 28 | 26, 27 | syl 17 | . . . . . 6
⊢ (𝜑 → (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))):(Base‘𝑅)–1-1-onto→ran
(𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)))) | 
| 29 |  | f1f 6804 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))):(Base‘𝑅)–1-1→(((Base‘𝑅) × (RLReg‘𝑅)) / (𝑅 ~RL (RLReg‘𝑅))) → (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))):(Base‘𝑅)⟶(((Base‘𝑅) × (RLReg‘𝑅)) / (𝑅 ~RL (RLReg‘𝑅)))) | 
| 30 | 26, 29 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))):(Base‘𝑅)⟶(((Base‘𝑅) × (RLReg‘𝑅)) / (𝑅 ~RL (RLReg‘𝑅)))) | 
| 31 | 30 | frnd 6744 | . . . . . . . . 9
⊢ (𝜑 → ran (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ⊆ (((Base‘𝑅) × (RLReg‘𝑅)) / (𝑅 ~RL (RLReg‘𝑅)))) | 
| 32 |  | eqid 2737 | . . . . . . . . . 10
⊢ ( Frac
‘𝑅) = ( Frac
‘𝑅) | 
| 33 | 9, 10, 32, 13 | fracbas 33307 | . . . . . . . . 9
⊢
(((Base‘𝑅)
× (RLReg‘𝑅))
/ (𝑅
~RL (RLReg‘𝑅))) = (Base‘( Frac ‘𝑅)) | 
| 34 | 31, 33 | sseqtrdi 4024 | . . . . . . . 8
⊢ (𝜑 → ran (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ⊆ (Base‘( Frac
‘𝑅))) | 
| 35 |  | eqid 2737 | . . . . . . . . 9
⊢
(Base‘( Frac ‘𝑅)) = (Base‘( Frac ‘𝑅)) | 
| 36 | 22, 35 | ressbas2 17283 | . . . . . . . 8
⊢ (ran
(𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ⊆ (Base‘( Frac
‘𝑅)) → ran
(𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) = (Base‘(( Frac
‘𝑅)
↾s ran (𝑥
∈ (Base‘𝑅)
↦ [〈𝑥,
(1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)))))) | 
| 37 | 34, 36 | syl 17 | . . . . . . 7
⊢ (𝜑 → ran (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) = (Base‘(( Frac
‘𝑅)
↾s ran (𝑥
∈ (Base‘𝑅)
↦ [〈𝑥,
(1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)))))) | 
| 38 | 37 | f1oeq3d 6845 | . . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))):(Base‘𝑅)–1-1-onto→ran
(𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ↔ (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))):(Base‘𝑅)–1-1-onto→(Base‘(( Frac ‘𝑅) ↾s ran (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))))))) | 
| 39 | 28, 38 | mpbid 232 | . . . . 5
⊢ (𝜑 → (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))):(Base‘𝑅)–1-1-onto→(Base‘(( Frac ‘𝑅) ↾s ran (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)))))) | 
| 40 |  | eqid 2737 | . . . . . 6
⊢
(Base‘(( Frac ‘𝑅) ↾s ran (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))))) = (Base‘(( Frac
‘𝑅)
↾s ran (𝑥
∈ (Base‘𝑅)
↦ [〈𝑥,
(1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))))) | 
| 41 | 9, 40 | isrim 20492 | . . . . 5
⊢ ((𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∈ (𝑅 RingIso (( Frac ‘𝑅) ↾s ran (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))))) ↔ ((𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∈ (𝑅 RingHom (( Frac ‘𝑅) ↾s ran (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))))) ∧ (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))):(Base‘𝑅)–1-1-onto→(Base‘(( Frac ‘𝑅) ↾s ran (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))))))) | 
| 42 | 25, 39, 41 | sylanbrc 583 | . . . 4
⊢ (𝜑 → (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∈ (𝑅 RingIso (( Frac ‘𝑅) ↾s ran (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅)))))) | 
| 43 |  | brrici 20505 | . . . 4
⊢ ((𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))) ∈ (𝑅 RingIso (( Frac ‘𝑅) ↾s ran (𝑥 ∈ (Base‘𝑅) ↦ [〈𝑥, (1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))))) → 𝑅 ≃𝑟 (( Frac
‘𝑅)
↾s ran (𝑥
∈ (Base‘𝑅)
↦ [〈𝑥,
(1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))))) | 
| 44 | 42, 43 | syl 17 | . . 3
⊢ (𝜑 → 𝑅 ≃𝑟 (( Frac
‘𝑅)
↾s ran (𝑥
∈ (Base‘𝑅)
↦ [〈𝑥,
(1r‘𝑅)〉](𝑅 ~RL (RLReg‘𝑅))))) | 
| 45 | 8, 19, 44 | rspcedvdw 3625 | . 2
⊢ (𝜑 → ∃𝑠 ∈ (SubRing‘( Frac ‘𝑅))𝑅 ≃𝑟 (( Frac
‘𝑅)
↾s 𝑠)) | 
| 46 | 4, 6, 45 | rspcedvdw 3625 | 1
⊢ (𝜑 → ∃𝑓 ∈ Field ∃𝑠 ∈ (SubRing‘𝑓)𝑅 ≃𝑟 (𝑓 ↾s 𝑠)) |