Theorem subrngpropd

Description: If two structures have the same ring components (properties), they have the same set of subrings. (Contributed by AV, 17-Feb-2025)

	Ref	Expression
Hypotheses	subrngpropd.1	$$⊢\phi \to B={\mathrm{Base}}_K$$
	subrngpropd.2	$$⊢\phi \to B={\mathrm{Base}}_L$$
	subrngpropd.3	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{K}y=x{+}_{L}y$$
	subrngpropd.4	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{\cdot }_{K}y=x{\cdot }_{L}y$$
Assertion	subrngpropd	Could not format assertion : No typesetting found for |- ( ph -> ( SubRng ` K ) = ( SubRng ` L ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		subrngpropd.1	$$⊢\phi \to B={\mathrm{Base}}_K$$
2		subrngpropd.2	$$⊢\phi \to B={\mathrm{Base}}_L$$
3		subrngpropd.3	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{K}y=x{+}_{L}y$$
4		subrngpropd.4	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{\cdot }_{K}y=x{\cdot }_{L}y$$
5	1 2 3 4	rngpropd	$$⊢\phi \to \left(K\in \mathrm{Rng}\leftrightarrow L\in \mathrm{Rng}\right)$$
6	1	ineq2d	$$⊢\phi \to s\cap B=s\cap {\mathrm{Base}}_K$$
7		eqid	$$⊢K{\upharpoonright }_{𝑠}s=K{\upharpoonright }_{𝑠}s$$
8		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
9	7 8	ressbas	$$⊢s\in \mathrm{V}\to s\cap {\mathrm{Base}}_K={\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}s\right)}$$
10	9	elv	$$⊢s\cap {\mathrm{Base}}_K={\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}s\right)}$$
11	6 10	eqtrdi	$$⊢\phi \to s\cap B={\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}s\right)}$$
12	2	ineq2d	$$⊢\phi \to s\cap B=s\cap {\mathrm{Base}}_L$$
13		eqid	$$⊢L{\upharpoonright }_{𝑠}s=L{\upharpoonright }_{𝑠}s$$
14		eqid	$$⊢{\mathrm{Base}}_L={\mathrm{Base}}_L$$
15	13 14	ressbas	$$⊢s\in \mathrm{V}\to s\cap {\mathrm{Base}}_L={\mathrm{Base}}_{\left(L{\upharpoonright }_{𝑠}s\right)}$$
16	15	elv	$$⊢s\cap {\mathrm{Base}}_L={\mathrm{Base}}_{\left(L{\upharpoonright }_{𝑠}s\right)}$$
17	12 16	eqtrdi	$$⊢\phi \to s\cap B={\mathrm{Base}}_{\left(L{\upharpoonright }_{𝑠}s\right)}$$
18		elinel2	$$⊢x\in \left(s\cap B\right)\to x\in B$$
19		elinel2	$$⊢y\in \left(s\cap B\right)\to y\in B$$
20	18 19	anim12i	$$⊢\left(x\in \left(s\cap B\right)\wedge y\in \left(s\cap B\right)\right)\to \left(x\in B\wedge y\in B\right)$$
21		eqid	$$⊢{+}_K={+}_K$$
22	7 21	ressplusg	$$⊢s\in \mathrm{V}\to {+}_K={+}_{\left(K{\upharpoonright }_{𝑠}s\right)}$$
23	22	elv	$$⊢{+}_K={+}_{\left(K{\upharpoonright }_{𝑠}s\right)}$$
24	23	oveqi	$$⊢x{+}_{K}y=x{+}_{\left(K{\upharpoonright }_{𝑠}s\right)}y$$
25		eqid	$$⊢{+}_L={+}_L$$
26	13 25	ressplusg	$$⊢s\in \mathrm{V}\to {+}_L={+}_{\left(L{\upharpoonright }_{𝑠}s\right)}$$
27	26	elv	$$⊢{+}_L={+}_{\left(L{\upharpoonright }_{𝑠}s\right)}$$
28	27	oveqi	$$⊢x{+}_{L}y=x{+}_{\left(L{\upharpoonright }_{𝑠}s\right)}y$$
29	3 24 28	3eqtr3g	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{\left(K{\upharpoonright }_{𝑠}s\right)}y=x{+}_{\left(L{\upharpoonright }_{𝑠}s\right)}y$$
30	20 29	sylan2	$$⊢\left(\phi \wedge \left(x\in \left(s\cap B\right)\wedge y\in \left(s\cap B\right)\right)\right)\to x{+}_{\left(K{\upharpoonright }_{𝑠}s\right)}y=x{+}_{\left(L{\upharpoonright }_{𝑠}s\right)}y$$
31		eqid	$$⊢{\cdot }_K={\cdot }_K$$
32	7 31	ressmulr	$$⊢s\in \mathrm{V}\to {\cdot }_K={\cdot }_{\left(K{\upharpoonright }_{𝑠}s\right)}$$
33	32	elv	$$⊢{\cdot }_K={\cdot }_{\left(K{\upharpoonright }_{𝑠}s\right)}$$
34	33	oveqi	$$⊢x{\cdot }_{K}y=x{\cdot }_{\left(K{\upharpoonright }_{𝑠}s\right)}y$$
35		eqid	$$⊢{\cdot }_L={\cdot }_L$$
36	13 35	ressmulr	$$⊢s\in \mathrm{V}\to {\cdot }_L={\cdot }_{\left(L{\upharpoonright }_{𝑠}s\right)}$$
37	36	elv	$$⊢{\cdot }_L={\cdot }_{\left(L{\upharpoonright }_{𝑠}s\right)}$$
38	37	oveqi	$$⊢x{\cdot }_{L}y=x{\cdot }_{\left(L{\upharpoonright }_{𝑠}s\right)}y$$
39	4 34 38	3eqtr3g	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{\cdot }_{\left(K{\upharpoonright }_{𝑠}s\right)}y=x{\cdot }_{\left(L{\upharpoonright }_{𝑠}s\right)}y$$
40	20 39	sylan2	$$⊢\left(\phi \wedge \left(x\in \left(s\cap B\right)\wedge y\in \left(s\cap B\right)\right)\right)\to x{\cdot }_{\left(K{\upharpoonright }_{𝑠}s\right)}y=x{\cdot }_{\left(L{\upharpoonright }_{𝑠}s\right)}y$$
41	11 17 30 40	rngpropd	$$⊢\phi \to \left(K{\upharpoonright }_{𝑠}s\in \mathrm{Rng}\leftrightarrow L{\upharpoonright }_{𝑠}s\in \mathrm{Rng}\right)$$
42	1 2	eqtr3d	$$⊢\phi \to {\mathrm{Base}}_K={\mathrm{Base}}_L$$
43	42	sseq2d	$$⊢\phi \to \left(s\subseteq {\mathrm{Base}}_K\leftrightarrow s\subseteq {\mathrm{Base}}_L\right)$$
44	5 41 43	3anbi123d	$$⊢\phi \to \left(\left(K\in \mathrm{Rng}\wedge K{\upharpoonright }_{𝑠}s\in \mathrm{Rng}\wedge s\subseteq {\mathrm{Base}}_K\right)\leftrightarrow \left(L\in \mathrm{Rng}\wedge L{\upharpoonright }_{𝑠}s\in \mathrm{Rng}\wedge s\subseteq {\mathrm{Base}}_L\right)\right)$$
45	8	issubrng	Could not format ( s e. ( SubRng ` K ) <-> ( K e. Rng /\ ( K |`s s ) e. Rng /\ s C_ ( Base ` K ) ) ) : No typesetting found for |- ( s e. ( SubRng ` K ) <-> ( K e. Rng /\ ( K |`s s ) e. Rng /\ s C_ ( Base ` K ) ) ) with typecode |-
46	14	issubrng	Could not format ( s e. ( SubRng ` L ) <-> ( L e. Rng /\ ( L |`s s ) e. Rng /\ s C_ ( Base ` L ) ) ) : No typesetting found for |- ( s e. ( SubRng ` L ) <-> ( L e. Rng /\ ( L |`s s ) e. Rng /\ s C_ ( Base ` L ) ) ) with typecode |-
47	44 45 46	3bitr4g	Could not format ( ph -> ( s e. ( SubRng ` K ) <-> s e. ( SubRng ` L ) ) ) : No typesetting found for |- ( ph -> ( s e. ( SubRng ` K ) <-> s e. ( SubRng ` L ) ) ) with typecode |-
48	47	eqrdv	Could not format ( ph -> ( SubRng ` K ) = ( SubRng ` L ) ) : No typesetting found for |- ( ph -> ( SubRng ` K ) = ( SubRng ` L ) ) with typecode |-