Theorem subsubrng

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

	Ref	Expression
Hypothesis	subsubrng.s	$$⊢S=R{\upharpoonright }_{𝑠}A$$
Assertion	subsubrng	Could not format assertion : No typesetting found for |- ( A e. ( SubRng ` R ) -> ( B e. ( SubRng ` S ) <-> ( B e. ( SubRng ` R ) /\ B C_ A ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		subsubrng.s	$$⊢S=R{\upharpoonright }_{𝑠}A$$
2		subrngrcl	Could not format ( A e. ( SubRng ` R ) -> R e. Rng ) : No typesetting found for |- ( A e. ( SubRng ` R ) -> R e. Rng ) with typecode |-
3	2	adantr	Could not format ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` S ) ) -> R e. Rng ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` S ) ) -> R e. Rng ) with typecode |-
4		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
5	4	subrngss	Could not format ( B e. ( SubRng ` S ) -> B C_ ( Base ` S ) ) : No typesetting found for |- ( B e. ( SubRng ` S ) -> B C_ ( Base ` S ) ) with typecode |-
6	5	adantl	Could not format ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` S ) ) -> B C_ ( Base ` S ) ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` S ) ) -> B C_ ( Base ` S ) ) with typecode |-
7	1	subrngbas	Could not format ( A e. ( SubRng ` R ) -> A = ( Base ` S ) ) : No typesetting found for |- ( A e. ( SubRng ` R ) -> A = ( Base ` S ) ) with typecode |-
8	7	adantr	Could not format ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` S ) ) -> A = ( Base ` S ) ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` S ) ) -> A = ( Base ` S ) ) with typecode |-
9	6 8	sseqtrrd	Could not format ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` S ) ) -> B C_ A ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` S ) ) -> B C_ A ) with typecode |-
10	1	oveq1i	$$⊢S{\upharpoonright }_{𝑠}B=\left(R{\upharpoonright }_{𝑠}A\right){\upharpoonright }_{𝑠}B$$
11		ressabs	Could not format ( ( A e. ( SubRng ` R ) /\ B C_ A ) -> ( ( R |`s A ) |`s B ) = ( R |`s B ) ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ B C_ A ) -> ( ( R |`s A ) |`s B ) = ( R |`s B ) ) with typecode |-
12	10 11	eqtrid	Could not format ( ( A e. ( SubRng ` R ) /\ B C_ A ) -> ( S |`s B ) = ( R |`s B ) ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ B C_ A ) -> ( S |`s B ) = ( R |`s B ) ) with typecode |-
13	9 12	syldan	Could not format ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` S ) ) -> ( S |`s B ) = ( R |`s B ) ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` S ) ) -> ( S |`s B ) = ( R |`s B ) ) with typecode |-
14		eqid	$$⊢S{\upharpoonright }_{𝑠}B=S{\upharpoonright }_{𝑠}B$$
15	14	subrngrng	Could not format ( B e. ( SubRng ` S ) -> ( S |`s B ) e. Rng ) : No typesetting found for |- ( B e. ( SubRng ` S ) -> ( S |`s B ) e. Rng ) with typecode |-
16	15	adantl	Could not format ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` S ) ) -> ( S |`s B ) e. Rng ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` S ) ) -> ( S |`s B ) e. Rng ) with typecode |-
17	13 16	eqeltrrd	Could not format ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` S ) ) -> ( R |`s B ) e. Rng ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` S ) ) -> ( R |`s B ) e. Rng ) with typecode |-
18		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
19	18	subrngss	Could not format ( A e. ( SubRng ` R ) -> A C_ ( Base ` R ) ) : No typesetting found for |- ( A e. ( SubRng ` R ) -> A C_ ( Base ` R ) ) with typecode |-
20	19	adantr	Could not format ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` S ) ) -> A C_ ( Base ` R ) ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` S ) ) -> A C_ ( Base ` R ) ) with typecode |-
21	9 20	sstrd	Could not format ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` S ) ) -> B C_ ( Base ` R ) ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` S ) ) -> B C_ ( Base ` R ) ) with typecode |-
22	18	issubrng	Could not format ( B e. ( SubRng ` R ) <-> ( R e. Rng /\ ( R |`s B ) e. Rng /\ B C_ ( Base ` R ) ) ) : No typesetting found for |- ( B e. ( SubRng ` R ) <-> ( R e. Rng /\ ( R |`s B ) e. Rng /\ B C_ ( Base ` R ) ) ) with typecode |-
23	3 17 21 22	syl3anbrc	Could not format ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` S ) ) -> B e. ( SubRng ` R ) ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` S ) ) -> B e. ( SubRng ` R ) ) with typecode |-
24	23 9	jca	Could not format ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` S ) ) -> ( B e. ( SubRng ` R ) /\ B C_ A ) ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` S ) ) -> ( B e. ( SubRng ` R ) /\ B C_ A ) ) with typecode |-
25	1	subrngrng	Could not format ( A e. ( SubRng ` R ) -> S e. Rng ) : No typesetting found for |- ( A e. ( SubRng ` R ) -> S e. Rng ) with typecode |-
26	25	adantr	Could not format ( ( A e. ( SubRng ` R ) /\ ( B e. ( SubRng ` R ) /\ B C_ A ) ) -> S e. Rng ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ ( B e. ( SubRng ` R ) /\ B C_ A ) ) -> S e. Rng ) with typecode |-
27	12	adantrl	Could not format ( ( A e. ( SubRng ` R ) /\ ( B e. ( SubRng ` R ) /\ B C_ A ) ) -> ( S |`s B ) = ( R |`s B ) ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ ( B e. ( SubRng ` R ) /\ B C_ A ) ) -> ( S |`s B ) = ( R |`s B ) ) with typecode |-
28		eqid	$$⊢R{\upharpoonright }_{𝑠}B=R{\upharpoonright }_{𝑠}B$$
29	28	subrngrng	Could not format ( B e. ( SubRng ` R ) -> ( R |`s B ) e. Rng ) : No typesetting found for |- ( B e. ( SubRng ` R ) -> ( R |`s B ) e. Rng ) with typecode |-
30	29	ad2antrl	Could not format ( ( A e. ( SubRng ` R ) /\ ( B e. ( SubRng ` R ) /\ B C_ A ) ) -> ( R |`s B ) e. Rng ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ ( B e. ( SubRng ` R ) /\ B C_ A ) ) -> ( R |`s B ) e. Rng ) with typecode |-
31	27 30	eqeltrd	Could not format ( ( A e. ( SubRng ` R ) /\ ( B e. ( SubRng ` R ) /\ B C_ A ) ) -> ( S |`s B ) e. Rng ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ ( B e. ( SubRng ` R ) /\ B C_ A ) ) -> ( S |`s B ) e. Rng ) with typecode |-
32		simprr	Could not format ( ( A e. ( SubRng ` R ) /\ ( B e. ( SubRng ` R ) /\ B C_ A ) ) -> B C_ A ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ ( B e. ( SubRng ` R ) /\ B C_ A ) ) -> B C_ A ) with typecode |-
33	7	adantr	Could not format ( ( A e. ( SubRng ` R ) /\ ( B e. ( SubRng ` R ) /\ B C_ A ) ) -> A = ( Base ` S ) ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ ( B e. ( SubRng ` R ) /\ B C_ A ) ) -> A = ( Base ` S ) ) with typecode |-
34	32 33	sseqtrd	Could not format ( ( A e. ( SubRng ` R ) /\ ( B e. ( SubRng ` R ) /\ B C_ A ) ) -> B C_ ( Base ` S ) ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ ( B e. ( SubRng ` R ) /\ B C_ A ) ) -> B C_ ( Base ` S ) ) with typecode |-
35	4	issubrng	Could not format ( B e. ( SubRng ` S ) <-> ( S e. Rng /\ ( S |`s B ) e. Rng /\ B C_ ( Base ` S ) ) ) : No typesetting found for |- ( B e. ( SubRng ` S ) <-> ( S e. Rng /\ ( S |`s B ) e. Rng /\ B C_ ( Base ` S ) ) ) with typecode |-
36	26 31 34 35	syl3anbrc	Could not format ( ( A e. ( SubRng ` R ) /\ ( B e. ( SubRng ` R ) /\ B C_ A ) ) -> B e. ( SubRng ` S ) ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ ( B e. ( SubRng ` R ) /\ B C_ A ) ) -> B e. ( SubRng ` S ) ) with typecode |-
37	24 36	impbida	Could not format ( A e. ( SubRng ` R ) -> ( B e. ( SubRng ` S ) <-> ( B e. ( SubRng ` R ) /\ B C_ A ) ) ) : No typesetting found for |- ( A e. ( SubRng ` R ) -> ( B e. ( SubRng ` S ) <-> ( B e. ( SubRng ` R ) /\ B C_ A ) ) ) with typecode |-