Metamath Proof Explorer

Theorem subsdrg

Description: A subring of a sub-division-ring is a sub-division-ring. See also subsubrg . (Contributed by Thierry Arnoux, 26-Oct-2025)

Ref Expression
Hypotheses subsdrg.s ⊢ S = R ↾ 𝑠 A
subsdrg.a ⊢ φ → A ∈ SubDRing ⁡ R
Assertion subsdrg ⊢ φ → B ∈ SubDRing ⁡ S ↔ B ∈ SubDRing ⁡ R ∧ B ⊆ A

Proof

Step Hyp Ref Expression
1 subsdrg.s ⊢ S = R ↾ 𝑠 A
2 subsdrg.a ⊢ φ → A ∈ SubDRing ⁡ R
3 eqid ⊢ Base S = Base S
4 3 sdrgss ⊢ B ∈ SubDRing ⁡ S → B ⊆ Base S
5 4 adantl ⊢ φ ∧ B ∈ SubDRing ⁡ S → B ⊆ Base S
6 eqid ⊢ Base R = Base R
7 6 sdrgss ⊢ A ∈ SubDRing ⁡ R → A ⊆ Base R
8 1 6 ressbas2 ⊢ A ⊆ Base R → A = Base S
9 2 7 8 3syl ⊢ φ → A = Base S
10 9 adantr ⊢ φ ∧ B ∈ SubDRing ⁡ S → A = Base S
11 5 10 sseqtrrd ⊢ φ ∧ B ∈ SubDRing ⁡ S → B ⊆ A
12 11 ex ⊢ φ → B ∈ SubDRing ⁡ S → B ⊆ A
13 12 pm4.71d ⊢ φ → B ∈ SubDRing ⁡ S ↔ B ∈ SubDRing ⁡ S ∧ B ⊆ A
14 1 sdrgdrng ⊢ A ∈ SubDRing ⁡ R → S ∈ DivRing
15 2 14 syl ⊢ φ → S ∈ DivRing
16 sdrgrcl ⊢ A ∈ SubDRing ⁡ R → R ∈ DivRing
17 2 16 syl ⊢ φ → R ∈ DivRing
18 15 17 2thd ⊢ φ → S ∈ DivRing ↔ R ∈ DivRing
19 18 adantr ⊢ φ ∧ B ⊆ A → S ∈ DivRing ↔ R ∈ DivRing
20 sdrgsubrg ⊢ A ∈ SubDRing ⁡ R → A ∈ SubRing ⁡ R
21 1 subsubrg ⊢ A ∈ SubRing ⁡ R → B ∈ SubRing ⁡ S ↔ B ∈ SubRing ⁡ R ∧ B ⊆ A
22 2 20 21 3syl ⊢ φ → B ∈ SubRing ⁡ S ↔ B ∈ SubRing ⁡ R ∧ B ⊆ A
23 22 rbaibd ⊢ φ ∧ B ⊆ A → B ∈ SubRing ⁡ S ↔ B ∈ SubRing ⁡ R
24 1 oveq1i ⊢ S ↾ 𝑠 B = R ↾ 𝑠 A ↾ 𝑠 B
25 ressabs ⊢ A ∈ SubDRing ⁡ R ∧ B ⊆ A → R ↾ 𝑠 A ↾ 𝑠 B = R ↾ 𝑠 B
26 2 25 sylan ⊢ φ ∧ B ⊆ A → R ↾ 𝑠 A ↾ 𝑠 B = R ↾ 𝑠 B
27 24 26 eqtrid ⊢ φ ∧ B ⊆ A → S ↾ 𝑠 B = R ↾ 𝑠 B
28 27 eleq1d ⊢ φ ∧ B ⊆ A → S ↾ 𝑠 B ∈ DivRing ↔ R ↾ 𝑠 B ∈ DivRing
29 19 23 28 3anbi123d ⊢ φ ∧ B ⊆ A → S ∈ DivRing ∧ B ∈ SubRing ⁡ S ∧ S ↾ 𝑠 B ∈ DivRing ↔ R ∈ DivRing ∧ B ∈ SubRing ⁡ R ∧ R ↾ 𝑠 B ∈ DivRing
30 issdrg ⊢ B ∈ SubDRing ⁡ S ↔ S ∈ DivRing ∧ B ∈ SubRing ⁡ S ∧ S ↾ 𝑠 B ∈ DivRing
31 issdrg ⊢ B ∈ SubDRing ⁡ R ↔ R ∈ DivRing ∧ B ∈ SubRing ⁡ R ∧ R ↾ 𝑠 B ∈ DivRing
32 29 30 31 3bitr4g ⊢ φ ∧ B ⊆ A → B ∈ SubDRing ⁡ S ↔ B ∈ SubDRing ⁡ R
33 32 ex ⊢ φ → B ⊆ A → B ∈ SubDRing ⁡ S ↔ B ∈ SubDRing ⁡ R
34 33 pm5.32rd ⊢ φ → B ∈ SubDRing ⁡ S ∧ B ⊆ A ↔ B ∈ SubDRing ⁡ R ∧ B ⊆ A
35 13 34 bitrd ⊢ φ → B ∈ SubDRing ⁡ S ↔ B ∈ SubDRing ⁡ R ∧ B ⊆ A