This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem subsubrng

Description: A subring of a subring is a subring. (Contributed by AV, 15-Feb-2025)

Ref Expression
Hypothesis subsubrng.s ⊢ 𝑆 = ( 𝑅 ↾s 𝐴 )
Assertion subsubrng ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) → ( 𝐵 ∈ ( SubRng ‘ 𝑆 ) ↔ ( 𝐵 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝐵 ⊆ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 subsubrng.s ⊢ 𝑆 = ( 𝑅 ↾s 𝐴 )
2 subrngrcl ⊢ ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) → 𝑅 ∈ Rng )
3 2 adantr ⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝐵 ∈ ( SubRng ‘ 𝑆 ) ) → 𝑅 ∈ Rng )
4 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
5 4 subrngss ⊢ ( 𝐵 ∈ ( SubRng ‘ 𝑆 ) → 𝐵 ⊆ ( Base ‘ 𝑆 ) )
6 5 adantl ⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝐵 ∈ ( SubRng ‘ 𝑆 ) ) → 𝐵 ⊆ ( Base ‘ 𝑆 ) )
7 1 subrngbas ⊢ ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) → 𝐴 = ( Base ‘ 𝑆 ) )
8 7 adantr ⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝐵 ∈ ( SubRng ‘ 𝑆 ) ) → 𝐴 = ( Base ‘ 𝑆 ) )
9 6 8 sseqtrrd ⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝐵 ∈ ( SubRng ‘ 𝑆 ) ) → 𝐵 ⊆ 𝐴 )
10 1 oveq1i ⊢ ( 𝑆 ↾s 𝐵 ) = ( ( 𝑅 ↾s 𝐴 ) ↾s 𝐵 )
11 ressabs ⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝐵 ⊆ 𝐴 ) → ( ( 𝑅 ↾s 𝐴 ) ↾s 𝐵 ) = ( 𝑅 ↾s 𝐵 ) )
12 10 11 eqtrid ⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑆 ↾s 𝐵 ) = ( 𝑅 ↾s 𝐵 ) )
13 9 12 syldan ⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝐵 ∈ ( SubRng ‘ 𝑆 ) ) → ( 𝑆 ↾s 𝐵 ) = ( 𝑅 ↾s 𝐵 ) )
14 eqid ⊢ ( 𝑆 ↾s 𝐵 ) = ( 𝑆 ↾s 𝐵 )
15 14 subrngrng ⊢ ( 𝐵 ∈ ( SubRng ‘ 𝑆 ) → ( 𝑆 ↾s 𝐵 ) ∈ Rng )
16 15 adantl ⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝐵 ∈ ( SubRng ‘ 𝑆 ) ) → ( 𝑆 ↾s 𝐵 ) ∈ Rng )
17 13 16 eqeltrrd ⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝐵 ∈ ( SubRng ‘ 𝑆 ) ) → ( 𝑅 ↾s 𝐵 ) ∈ Rng )
18 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
19 18 subrngss ⊢ ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) → 𝐴 ⊆ ( Base ‘ 𝑅 ) )
20 19 adantr ⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝐵 ∈ ( SubRng ‘ 𝑆 ) ) → 𝐴 ⊆ ( Base ‘ 𝑅 ) )
21 9 20 sstrd ⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝐵 ∈ ( SubRng ‘ 𝑆 ) ) → 𝐵 ⊆ ( Base ‘ 𝑅 ) )
22 18 issubrng ⊢ ( 𝐵 ∈ ( SubRng ‘ 𝑅 ) ↔ ( 𝑅 ∈ Rng ∧ ( 𝑅 ↾s 𝐵 ) ∈ Rng ∧ 𝐵 ⊆ ( Base ‘ 𝑅 ) ) )
23 3 17 21 22 syl3anbrc ⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝐵 ∈ ( SubRng ‘ 𝑆 ) ) → 𝐵 ∈ ( SubRng ‘ 𝑅 ) )
24 23 9 jca ⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝐵 ∈ ( SubRng ‘ 𝑆 ) ) → ( 𝐵 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝐵 ⊆ 𝐴 ) )
25 1 subrngrng ⊢ ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) → 𝑆 ∈ Rng )
26 25 adantr ⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ ( 𝐵 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝐵 ⊆ 𝐴 ) ) → 𝑆 ∈ Rng )
27 12 adantrl ⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ ( 𝐵 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝐵 ⊆ 𝐴 ) ) → ( 𝑆 ↾s 𝐵 ) = ( 𝑅 ↾s 𝐵 ) )
28 eqid ⊢ ( 𝑅 ↾s 𝐵 ) = ( 𝑅 ↾s 𝐵 )
29 28 subrngrng ⊢ ( 𝐵 ∈ ( SubRng ‘ 𝑅 ) → ( 𝑅 ↾s 𝐵 ) ∈ Rng )
30 29 ad2antrl ⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ ( 𝐵 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝐵 ⊆ 𝐴 ) ) → ( 𝑅 ↾s 𝐵 ) ∈ Rng )
31 27 30 eqeltrd ⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ ( 𝐵 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝐵 ⊆ 𝐴 ) ) → ( 𝑆 ↾s 𝐵 ) ∈ Rng )
32 simprr ⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ ( 𝐵 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝐵 ⊆ 𝐴 ) ) → 𝐵 ⊆ 𝐴 )
33 7 adantr ⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ ( 𝐵 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝐵 ⊆ 𝐴 ) ) → 𝐴 = ( Base ‘ 𝑆 ) )
34 32 33 sseqtrd ⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ ( 𝐵 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝐵 ⊆ 𝐴 ) ) → 𝐵 ⊆ ( Base ‘ 𝑆 ) )
35 4 issubrng ⊢ ( 𝐵 ∈ ( SubRng ‘ 𝑆 ) ↔ ( 𝑆 ∈ Rng ∧ ( 𝑆 ↾s 𝐵 ) ∈ Rng ∧ 𝐵 ⊆ ( Base ‘ 𝑆 ) ) )
36 26 31 34 35 syl3anbrc ⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ ( 𝐵 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝐵 ⊆ 𝐴 ) ) → 𝐵 ∈ ( SubRng ‘ 𝑆 ) )
37 24 36 impbida ⊢ ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) → ( 𝐵 ∈ ( SubRng ‘ 𝑆 ) ↔ ( 𝐵 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝐵 ⊆ 𝐴 ) ) )