Metamath Proof Explorer

Theorem subsubrg

Description: A subring of a subring is a subring. (Contributed by Mario Carneiro, 4-Dec-2014)

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

Proof

Step Hyp Ref Expression
1 subsubrg.s ⊢ 𝑆 = ( 𝑅 ↾s 𝐴 )
2 subrgrcl ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝑅 ∈ Ring )
3 2 adantr ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐵 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑅 ∈ Ring )
4 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
5 4 subrgss ⊢ ( 𝐵 ∈ ( SubRing ‘ 𝑆 ) → 𝐵 ⊆ ( Base ‘ 𝑆 ) )
6 5 adantl ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐵 ∈ ( SubRing ‘ 𝑆 ) ) → 𝐵 ⊆ ( Base ‘ 𝑆 ) )
7 1 subrgbas ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝐴 = ( Base ‘ 𝑆 ) )
8 7 adantr ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐵 ∈ ( SubRing ‘ 𝑆 ) ) → 𝐴 = ( Base ‘ 𝑆 ) )
9 6 8 sseqtrrd ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐵 ∈ ( SubRing ‘ 𝑆 ) ) → 𝐵 ⊆ 𝐴 )
10 1 oveq1i ⊢ ( 𝑆 ↾s 𝐵 ) = ( ( 𝑅 ↾s 𝐴 ) ↾s 𝐵 )
11 ressabs ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐵 ⊆ 𝐴 ) → ( ( 𝑅 ↾s 𝐴 ) ↾s 𝐵 ) = ( 𝑅 ↾s 𝐵 ) )
12 10 11 syl5eq ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑆 ↾s 𝐵 ) = ( 𝑅 ↾s 𝐵 ) )
13 9 12 syldan ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐵 ∈ ( SubRing ‘ 𝑆 ) ) → ( 𝑆 ↾s 𝐵 ) = ( 𝑅 ↾s 𝐵 ) )
14 eqid ⊢ ( 𝑆 ↾s 𝐵 ) = ( 𝑆 ↾s 𝐵 )
15 14 subrgring ⊢ ( 𝐵 ∈ ( SubRing ‘ 𝑆 ) → ( 𝑆 ↾s 𝐵 ) ∈ Ring )
16 15 adantl ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐵 ∈ ( SubRing ‘ 𝑆 ) ) → ( 𝑆 ↾s 𝐵 ) ∈ Ring )
17 13 16 eqeltrrd ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐵 ∈ ( SubRing ‘ 𝑆 ) ) → ( 𝑅 ↾s 𝐵 ) ∈ Ring )
18 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
19 18 subrgss ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝐴 ⊆ ( Base ‘ 𝑅 ) )
20 19 adantr ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐵 ∈ ( SubRing ‘ 𝑆 ) ) → 𝐴 ⊆ ( Base ‘ 𝑅 ) )
21 9 20 sstrd ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐵 ∈ ( SubRing ‘ 𝑆 ) ) → 𝐵 ⊆ ( Base ‘ 𝑅 ) )
22 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
23 1 22 subrg1 ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑆 ) )
24 23 adantr ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐵 ∈ ( SubRing ‘ 𝑆 ) ) → ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑆 ) )
25 eqid ⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
26 25 subrg1cl ⊢ ( 𝐵 ∈ ( SubRing ‘ 𝑆 ) → ( 1r ‘ 𝑆 ) ∈ 𝐵 )
27 26 adantl ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐵 ∈ ( SubRing ‘ 𝑆 ) ) → ( 1r ‘ 𝑆 ) ∈ 𝐵 )
28 24 27 eqeltrd ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐵 ∈ ( SubRing ‘ 𝑆 ) ) → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
29 21 28 jca ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐵 ∈ ( SubRing ‘ 𝑆 ) ) → ( 𝐵 ⊆ ( Base ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ∈ 𝐵 ) )
30 18 22 issubrg ⊢ ( 𝐵 ∈ ( SubRing ‘ 𝑅 ) ↔ ( ( 𝑅 ∈ Ring ∧ ( 𝑅 ↾s 𝐵 ) ∈ Ring ) ∧ ( 𝐵 ⊆ ( Base ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ∈ 𝐵 ) ) )
31 3 17 29 30 syl21anbrc ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐵 ∈ ( SubRing ‘ 𝑆 ) ) → 𝐵 ∈ ( SubRing ‘ 𝑅 ) )
32 31 9 jca ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐵 ∈ ( SubRing ‘ 𝑆 ) ) → ( 𝐵 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐵 ⊆ 𝐴 ) )
33 1 subrgring ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝑆 ∈ Ring )
34 33 adantr ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝐵 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐵 ⊆ 𝐴 ) ) → 𝑆 ∈ Ring )
35 12 adantrl ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝐵 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐵 ⊆ 𝐴 ) ) → ( 𝑆 ↾s 𝐵 ) = ( 𝑅 ↾s 𝐵 ) )
36 eqid ⊢ ( 𝑅 ↾s 𝐵 ) = ( 𝑅 ↾s 𝐵 )
37 36 subrgring ⊢ ( 𝐵 ∈ ( SubRing ‘ 𝑅 ) → ( 𝑅 ↾s 𝐵 ) ∈ Ring )
38 37 ad2antrl ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝐵 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐵 ⊆ 𝐴 ) ) → ( 𝑅 ↾s 𝐵 ) ∈ Ring )
39 35 38 eqeltrd ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝐵 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐵 ⊆ 𝐴 ) ) → ( 𝑆 ↾s 𝐵 ) ∈ Ring )
40 simprr ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝐵 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐵 ⊆ 𝐴 ) ) → 𝐵 ⊆ 𝐴 )
41 7 adantr ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝐵 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐵 ⊆ 𝐴 ) ) → 𝐴 = ( Base ‘ 𝑆 ) )
42 40 41 sseqtrd ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝐵 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐵 ⊆ 𝐴 ) ) → 𝐵 ⊆ ( Base ‘ 𝑆 ) )
43 23 adantr ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝐵 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐵 ⊆ 𝐴 ) ) → ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑆 ) )
44 22 subrg1cl ⊢ ( 𝐵 ∈ ( SubRing ‘ 𝑅 ) → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
45 44 ad2antrl ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝐵 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐵 ⊆ 𝐴 ) ) → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
46 43 45 eqeltrrd ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝐵 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐵 ⊆ 𝐴 ) ) → ( 1r ‘ 𝑆 ) ∈ 𝐵 )
47 42 46 jca ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝐵 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐵 ⊆ 𝐴 ) ) → ( 𝐵 ⊆ ( Base ‘ 𝑆 ) ∧ ( 1r ‘ 𝑆 ) ∈ 𝐵 ) )
48 4 25 issubrg ⊢ ( 𝐵 ∈ ( SubRing ‘ 𝑆 ) ↔ ( ( 𝑆 ∈ Ring ∧ ( 𝑆 ↾s 𝐵 ) ∈ Ring ) ∧ ( 𝐵 ⊆ ( Base ‘ 𝑆 ) ∧ ( 1r ‘ 𝑆 ) ∈ 𝐵 ) ) )
49 34 39 47 48 syl21anbrc ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝐵 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐵 ⊆ 𝐴 ) ) → 𝐵 ∈ ( SubRing ‘ 𝑆 ) )
50 32 49 impbida ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( 𝐵 ∈ ( SubRing ‘ 𝑆 ) ↔ ( 𝐵 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐵 ⊆ 𝐴 ) ) )