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 𝐴 )
subsdrg.a ⊢ ( 𝜑 → 𝐴 ∈ ( SubDRing ‘ 𝑅 ) )
Assertion subsdrg ( 𝜑 → ( 𝐵 ∈ ( SubDRing ‘ 𝑆 ) ↔ ( 𝐵 ∈ ( SubDRing ‘ 𝑅 ) ∧ 𝐵 ⊆ 𝐴 ) ) )

Proof

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