resssra

Description: The subring algebra of a restricted structure is the restriction of the subring algebra. (Contributed by Thierry Arnoux, 2-Apr-2025)

	Ref	Expression
Hypotheses	resssra.a	$⊢ A = {Base}_{R}$
	resssra.s	$⊢ S = R ↾_{𝑠} B$
	resssra.b	$⊢ φ \to B \subseteq A$
	resssra.c	$⊢ φ \to C \subseteq B$
	resssra.r	$⊢ φ \to R \in V$
Assertion	resssra	$⊢ φ \to subringAlg (S) (C) = subringAlg (R) (C) ↾_{𝑠} B$

Proof

Step	Hyp	Ref	Expression
1		resssra.a	$⊢ A = {Base}_{R}$
2		resssra.s	$⊢ S = R ↾_{𝑠} B$
3		resssra.b	$⊢ φ \to B \subseteq A$
4		resssra.c	$⊢ φ \to C \subseteq B$
5		resssra.r	$⊢ φ \to R \in V$
6		eqidd	$⊢ φ \to subringAlg (R) (C) = subringAlg (R) (C)$
7	4 3	sstrd	$⊢ φ \to C \subseteq A$
8	7 1	sseqtrdi	$⊢ φ \to C \subseteq {Base}_{R}$
9	6 8	srabase	$⊢ φ \to {Base}_{R} = {Base}_{subringAlg (R) (C)}$
10	1 9	eqtrid	$⊢ φ \to A = {Base}_{subringAlg (R) (C)}$
11	10	oveq2d	$⊢ φ \to subringAlg (R) (C) ↾_{𝑠} A = subringAlg (R) (C) ↾_{𝑠} {Base}_{subringAlg (R) (C)}$
12	11	adantr	$⊢ (φ \land A \subseteq B) \to subringAlg (R) (C) ↾_{𝑠} A = subringAlg (R) (C) ↾_{𝑠} {Base}_{subringAlg (R) (C)}$
13		simpr	$⊢ (φ \land A \subseteq B) \to A \subseteq B$
14	3	adantr	$⊢ (φ \land A \subseteq B) \to B \subseteq A$
15	13 14	eqssd	$⊢ (φ \land A \subseteq B) \to A = B$
16	15	oveq2d	$⊢ (φ \land A \subseteq B) \to subringAlg (R) (C) ↾_{𝑠} A = subringAlg (R) (C) ↾_{𝑠} B$
17		fvex	$⊢ subringAlg (R) (C) \in V$
18		eqid	$⊢ {Base}_{subringAlg (R) (C)} = {Base}_{subringAlg (R) (C)}$
19	18	ressid	$⊢ subringAlg (R) (C) \in V \to subringAlg (R) (C) ↾_{𝑠} {Base}_{subringAlg (R) (C)} = subringAlg (R) (C)$
20	17 19	mp1i	$⊢ (φ \land A \subseteq B) \to subringAlg (R) (C) ↾_{𝑠} {Base}_{subringAlg (R) (C)} = subringAlg (R) (C)$
21	12 16 20	3eqtr3d	$⊢ (φ \land A \subseteq B) \to subringAlg (R) (C) ↾_{𝑠} B = subringAlg (R) (C)$
22	1	oveq2i	$⊢ R ↾_{𝑠} A = R ↾_{𝑠} {Base}_{R}$
23	5	elexd	$⊢ φ \to R \in V$
24		eqid	$⊢ {Base}_{R} = {Base}_{R}$
25	24	ressid	$⊢ R \in V \to R ↾_{𝑠} {Base}_{R} = R$
26	23 25	syl	$⊢ φ \to R ↾_{𝑠} {Base}_{R} = R$
27	22 26	eqtrid	$⊢ φ \to R ↾_{𝑠} A = R$
28	27	adantr	$⊢ (φ \land A \subseteq B) \to R ↾_{𝑠} A = R$
29	15	oveq2d	$⊢ (φ \land A \subseteq B) \to R ↾_{𝑠} A = R ↾_{𝑠} B$
30	29 2	eqtr4di	$⊢ (φ \land A \subseteq B) \to R ↾_{𝑠} A = S$
31	28 30	eqtr3d	$⊢ (φ \land A \subseteq B) \to R = S$
32	31	fveq2d	$⊢ (φ \land A \subseteq B) \to subringAlg (R) = subringAlg (S)$
33	32	fveq1d	$⊢ (φ \land A \subseteq B) \to subringAlg (R) (C) = subringAlg (S) (C)$
34	21 33	eqtr2d	$⊢ (φ \land A \subseteq B) \to subringAlg (S) (C) = subringAlg (R) (C) ↾_{𝑠} B$
35		simpr	$⊢ (φ \land \neg A \subseteq B) \to \neg A \subseteq B$
36	23	adantr	$⊢ (φ \land \neg A \subseteq B) \to R \in V$
37	1	fvexi	$⊢ A \in V$
38	37	a1i	$⊢ φ \to A \in V$
39	38 3	ssexd	$⊢ φ \to B \in V$
40	39	adantr	$⊢ (φ \land \neg A \subseteq B) \to B \in V$
41	2 1	ressval2	$⊢ (\neg A \subseteq B \land R \in V \land B \in V) \to S = R sSet ⟨{Base}_{ndx}, B \cap A⟩$
42	35 36 40 41	syl3anc	$⊢ (φ \land \neg A \subseteq B) \to S = R sSet ⟨{Base}_{ndx}, B \cap A⟩$
43		df-ss	$⊢ B \subseteq A \leftrightarrow B \cap A = B$
44	3 43	sylib	$⊢ φ \to B \cap A = B$
45	44	opeq2d	$⊢ φ \to ⟨{Base}_{ndx}, B \cap A⟩ = ⟨{Base}_{ndx}, B⟩$
46	45	oveq2d	$⊢ φ \to R sSet ⟨{Base}_{ndx}, B \cap A⟩ = R sSet ⟨{Base}_{ndx}, B⟩$
47	46	adantr	$⊢ (φ \land \neg A \subseteq B) \to R sSet ⟨{Base}_{ndx}, B \cap A⟩ = R sSet ⟨{Base}_{ndx}, B⟩$
48	42 47	eqtrd	$⊢ (φ \land \neg A \subseteq B) \to S = R sSet ⟨{Base}_{ndx}, B⟩$
49	2	oveq1i	$⊢ S ↾_{𝑠} C = (R ↾_{𝑠} B) ↾_{𝑠} C$
50		ressabs	$⊢ (B \in V \land C \subseteq B) \to (R ↾_{𝑠} B) ↾_{𝑠} C = R ↾_{𝑠} C$
51	39 4 50	syl2anc	$⊢ φ \to (R ↾_{𝑠} B) ↾_{𝑠} C = R ↾_{𝑠} C$
52	49 51	eqtrid	$⊢ φ \to S ↾_{𝑠} C = R ↾_{𝑠} C$
53	52	opeq2d	$⊢ φ \to ⟨Scalar (ndx), S ↾_{𝑠} C⟩ = ⟨Scalar (ndx), R ↾_{𝑠} C⟩$
54	53	adantr	$⊢ (φ \land \neg A \subseteq B) \to ⟨Scalar (ndx), S ↾_{𝑠} C⟩ = ⟨Scalar (ndx), R ↾_{𝑠} C⟩$
55	48 54	oveq12d	$⊢ (φ \land \neg A \subseteq B) \to S sSet ⟨Scalar (ndx), S ↾_{𝑠} C⟩ = (R sSet ⟨{Base}_{ndx}, B⟩) sSet ⟨Scalar (ndx), R ↾_{𝑠} C⟩$
56		scandxnbasendx	$⊢ Scalar (ndx) \neq {Base}_{ndx}$
57	56	a1i	$⊢ φ \to Scalar (ndx) \neq {Base}_{ndx}$
58		ovexd	$⊢ φ \to R ↾_{𝑠} C \in V$
59		fvex	$⊢ Scalar (ndx) \in V$
60		fvex	$⊢ {Base}_{ndx} \in V$
61	59 60	setscom	$⊢ ((R \in V \land Scalar (ndx) \neq {Base}_{ndx}) \land (R ↾_{𝑠} C \in V \land B \in V)) \to (R sSet ⟨Scalar (ndx), R ↾_{𝑠} C⟩) sSet ⟨{Base}_{ndx}, B⟩ = (R sSet ⟨{Base}_{ndx}, B⟩) sSet ⟨Scalar (ndx), R ↾_{𝑠} C⟩$
62	23 57 58 39 61	syl22anc	$⊢ φ \to (R sSet ⟨Scalar (ndx), R ↾_{𝑠} C⟩) sSet ⟨{Base}_{ndx}, B⟩ = (R sSet ⟨{Base}_{ndx}, B⟩) sSet ⟨Scalar (ndx), R ↾_{𝑠} C⟩$
63	62	adantr	$⊢ (φ \land \neg A \subseteq B) \to (R sSet ⟨Scalar (ndx), R ↾_{𝑠} C⟩) sSet ⟨{Base}_{ndx}, B⟩ = (R sSet ⟨{Base}_{ndx}, B⟩) sSet ⟨Scalar (ndx), R ↾_{𝑠} C⟩$
64	55 63	eqtr4d	$⊢ (φ \land \neg A \subseteq B) \to S sSet ⟨Scalar (ndx), S ↾_{𝑠} C⟩ = (R sSet ⟨Scalar (ndx), R ↾_{𝑠} C⟩) sSet ⟨{Base}_{ndx}, B⟩$
65		eqid	$⊢ \cdot_{R} = \cdot_{R}$
66	2 65	ressmulr	$⊢ B \in V \to \cdot_{R} = \cdot_{S}$
67	39 66	syl	$⊢ φ \to \cdot_{R} = \cdot_{S}$
68	67	eqcomd	$⊢ φ \to \cdot_{S} = \cdot_{R}$
69	68	opeq2d	$⊢ φ \to ⟨\cdot_{ndx}, \cdot_{S}⟩ = ⟨\cdot_{ndx}, \cdot_{R}⟩$
70	69	adantr	$⊢ (φ \land \neg A \subseteq B) \to ⟨\cdot_{ndx}, \cdot_{S}⟩ = ⟨\cdot_{ndx}, \cdot_{R}⟩$
71	64 70	oveq12d	$⊢ (φ \land \neg A \subseteq B) \to (S sSet ⟨Scalar (ndx), S ↾_{𝑠} C⟩) sSet ⟨\cdot_{ndx}, \cdot_{S}⟩ = ((R sSet ⟨Scalar (ndx), R ↾_{𝑠} C⟩) sSet ⟨{Base}_{ndx}, B⟩) sSet ⟨\cdot_{ndx}, \cdot_{R}⟩$
72		ovexd	$⊢ φ \to R sSet ⟨Scalar (ndx), R ↾_{𝑠} C⟩ \in V$
73		vscandxnbasendx	$⊢ \cdot_{ndx} \neq {Base}_{ndx}$
74	73	a1i	$⊢ φ \to \cdot_{ndx} \neq {Base}_{ndx}$
75		fvexd	$⊢ φ \to \cdot_{R} \in V$
76		fvex	$⊢ \cdot_{ndx} \in V$
77	76 60	setscom	$⊢ ((R sSet ⟨Scalar (ndx), R ↾_{𝑠} C⟩ \in V \land \cdot_{ndx} \neq {Base}_{ndx}) \land (\cdot_{R} \in V \land B \in V)) \to ((R sSet ⟨Scalar (ndx), R ↾_{𝑠} C⟩) sSet ⟨\cdot_{ndx}, \cdot_{R}⟩) sSet ⟨{Base}_{ndx}, B⟩ = ((R sSet ⟨Scalar (ndx), R ↾_{𝑠} C⟩) sSet ⟨{Base}_{ndx}, B⟩) sSet ⟨\cdot_{ndx}, \cdot_{R}⟩$
78	72 74 75 39 77	syl22anc	$⊢ φ \to ((R sSet ⟨Scalar (ndx), R ↾_{𝑠} C⟩) sSet ⟨\cdot_{ndx}, \cdot_{R}⟩) sSet ⟨{Base}_{ndx}, B⟩ = ((R sSet ⟨Scalar (ndx), R ↾_{𝑠} C⟩) sSet ⟨{Base}_{ndx}, B⟩) sSet ⟨\cdot_{ndx}, \cdot_{R}⟩$
79	78	adantr	$⊢ (φ \land \neg A \subseteq B) \to ((R sSet ⟨Scalar (ndx), R ↾_{𝑠} C⟩) sSet ⟨\cdot_{ndx}, \cdot_{R}⟩) sSet ⟨{Base}_{ndx}, B⟩ = ((R sSet ⟨Scalar (ndx), R ↾_{𝑠} C⟩) sSet ⟨{Base}_{ndx}, B⟩) sSet ⟨\cdot_{ndx}, \cdot_{R}⟩$
80	71 79	eqtr4d	$⊢ (φ \land \neg A \subseteq B) \to (S sSet ⟨Scalar (ndx), S ↾_{𝑠} C⟩) sSet ⟨\cdot_{ndx}, \cdot_{S}⟩ = ((R sSet ⟨Scalar (ndx), R ↾_{𝑠} C⟩) sSet ⟨\cdot_{ndx}, \cdot_{R}⟩) sSet ⟨{Base}_{ndx}, B⟩$
81	68	opeq2d	$⊢ φ \to ⟨\cdot_{𝑖} (ndx), \cdot_{S}⟩ = ⟨\cdot_{𝑖} (ndx), \cdot_{R}⟩$
82	81	adantr	$⊢ (φ \land \neg A \subseteq B) \to ⟨\cdot_{𝑖} (ndx), \cdot_{S}⟩ = ⟨\cdot_{𝑖} (ndx), \cdot_{R}⟩$
83	80 82	oveq12d	$⊢ (φ \land \neg A \subseteq B) \to ((S sSet ⟨Scalar (ndx), S ↾_{𝑠} C⟩) sSet ⟨\cdot_{ndx}, \cdot_{S}⟩) sSet ⟨\cdot_{𝑖} (ndx), \cdot_{S}⟩ = (((R sSet ⟨Scalar (ndx), R ↾_{𝑠} C⟩) sSet ⟨\cdot_{ndx}, \cdot_{R}⟩) sSet ⟨{Base}_{ndx}, B⟩) sSet ⟨\cdot_{𝑖} (ndx), \cdot_{R}⟩$
84		ovexd	$⊢ φ \to (R sSet ⟨Scalar (ndx), R ↾_{𝑠} C⟩) sSet ⟨\cdot_{ndx}, \cdot_{R}⟩ \in V$
85		ipndxnbasendx	$⊢ \cdot_{𝑖} (ndx) \neq {Base}_{ndx}$
86	85	a1i	$⊢ φ \to \cdot_{𝑖} (ndx) \neq {Base}_{ndx}$
87		fvex	$⊢ \cdot_{𝑖} (ndx) \in V$
88	87 60	setscom	$⊢ (((R sSet ⟨Scalar (ndx), R ↾_{𝑠} C⟩) sSet ⟨\cdot_{ndx}, \cdot_{R}⟩ \in V \land \cdot_{𝑖} (ndx) \neq {Base}_{ndx}) \land (\cdot_{R} \in V \land B \in V)) \to (((R sSet ⟨Scalar (ndx), R ↾_{𝑠} C⟩) sSet ⟨\cdot_{ndx}, \cdot_{R}⟩) sSet ⟨\cdot_{𝑖} (ndx), \cdot_{R}⟩) sSet ⟨{Base}_{ndx}, B⟩ = (((R sSet ⟨Scalar (ndx), R ↾_{𝑠} C⟩) sSet ⟨\cdot_{ndx}, \cdot_{R}⟩) sSet ⟨{Base}_{ndx}, B⟩) sSet ⟨\cdot_{𝑖} (ndx), \cdot_{R}⟩$
89	84 86 75 39 88	syl22anc	$⊢ φ \to (((R sSet ⟨Scalar (ndx), R ↾_{𝑠} C⟩) sSet ⟨\cdot_{ndx}, \cdot_{R}⟩) sSet ⟨\cdot_{𝑖} (ndx), \cdot_{R}⟩) sSet ⟨{Base}_{ndx}, B⟩ = (((R sSet ⟨Scalar (ndx), R ↾_{𝑠} C⟩) sSet ⟨\cdot_{ndx}, \cdot_{R}⟩) sSet ⟨{Base}_{ndx}, B⟩) sSet ⟨\cdot_{𝑖} (ndx), \cdot_{R}⟩$
90	89	adantr	$⊢ (φ \land \neg A \subseteq B) \to (((R sSet ⟨Scalar (ndx), R ↾_{𝑠} C⟩) sSet ⟨\cdot_{ndx}, \cdot_{R}⟩) sSet ⟨\cdot_{𝑖} (ndx), \cdot_{R}⟩) sSet ⟨{Base}_{ndx}, B⟩ = (((R sSet ⟨Scalar (ndx), R ↾_{𝑠} C⟩) sSet ⟨\cdot_{ndx}, \cdot_{R}⟩) sSet ⟨{Base}_{ndx}, B⟩) sSet ⟨\cdot_{𝑖} (ndx), \cdot_{R}⟩$
91	83 90	eqtr4d	$⊢ (φ \land \neg A \subseteq B) \to ((S sSet ⟨Scalar (ndx), S ↾_{𝑠} C⟩) sSet ⟨\cdot_{ndx}, \cdot_{S}⟩) sSet ⟨\cdot_{𝑖} (ndx), \cdot_{S}⟩ = (((R sSet ⟨Scalar (ndx), R ↾_{𝑠} C⟩) sSet ⟨\cdot_{ndx}, \cdot_{R}⟩) sSet ⟨\cdot_{𝑖} (ndx), \cdot_{R}⟩) sSet ⟨{Base}_{ndx}, B⟩$
92	2	ovexi	$⊢ S \in V$
93	2 1	ressbas2	$⊢ B \subseteq A \to B = {Base}_{S}$
94	3 93	syl	$⊢ φ \to B = {Base}_{S}$
95	4 94	sseqtrd	$⊢ φ \to C \subseteq {Base}_{S}$
96	95	adantr	$⊢ (φ \land \neg A \subseteq B) \to C \subseteq {Base}_{S}$
97		sraval	$⊢ (S \in V \land C \subseteq {Base}_{S}) \to subringAlg (S) (C) = ((S sSet ⟨Scalar (ndx), S ↾_{𝑠} C⟩) sSet ⟨\cdot_{ndx}, \cdot_{S}⟩) sSet ⟨\cdot_{𝑖} (ndx), \cdot_{S}⟩$
98	92 96 97	sylancr	$⊢ (φ \land \neg A \subseteq B) \to subringAlg (S) (C) = ((S sSet ⟨Scalar (ndx), S ↾_{𝑠} C⟩) sSet ⟨\cdot_{ndx}, \cdot_{S}⟩) sSet ⟨\cdot_{𝑖} (ndx), \cdot_{S}⟩$
99	10	adantr	$⊢ (φ \land \neg A \subseteq B) \to A = {Base}_{subringAlg (R) (C)}$
100	99	sseq1d	$⊢ (φ \land \neg A \subseteq B) \to (A \subseteq B \leftrightarrow {Base}_{subringAlg (R) (C)} \subseteq B)$
101	35 100	mtbid	$⊢ (φ \land \neg A \subseteq B) \to \neg {Base}_{subringAlg (R) (C)} \subseteq B$
102		fvexd	$⊢ (φ \land \neg A \subseteq B) \to subringAlg (R) (C) \in V$
103		eqid	$⊢ subringAlg (R) (C) ↾_{𝑠} B = subringAlg (R) (C) ↾_{𝑠} B$
104	103 18	ressval2	$⊢ (\neg {Base}_{subringAlg (R) (C)} \subseteq B \land subringAlg (R) (C) \in V \land B \in V) \to subringAlg (R) (C) ↾_{𝑠} B = subringAlg (R) (C) sSet ⟨{Base}_{ndx}, B \cap {Base}_{subringAlg (R) (C)}⟩$
105	101 102 40 104	syl3anc	$⊢ (φ \land \neg A \subseteq B) \to subringAlg (R) (C) ↾_{𝑠} B = subringAlg (R) (C) sSet ⟨{Base}_{ndx}, B \cap {Base}_{subringAlg (R) (C)}⟩$
106	10	ineq2d	$⊢ φ \to B \cap A = B \cap {Base}_{subringAlg (R) (C)}$
107	106 44	eqtr3d	$⊢ φ \to B \cap {Base}_{subringAlg (R) (C)} = B$
108	107	opeq2d	$⊢ φ \to ⟨{Base}_{ndx}, B \cap {Base}_{subringAlg (R) (C)}⟩ = ⟨{Base}_{ndx}, B⟩$
109	108	oveq2d	$⊢ φ \to subringAlg (R) (C) sSet ⟨{Base}_{ndx}, B \cap {Base}_{subringAlg (R) (C)}⟩ = subringAlg (R) (C) sSet ⟨{Base}_{ndx}, B⟩$
110	109	adantr	$⊢ (φ \land \neg A \subseteq B) \to subringAlg (R) (C) sSet ⟨{Base}_{ndx}, B \cap {Base}_{subringAlg (R) (C)}⟩ = subringAlg (R) (C) sSet ⟨{Base}_{ndx}, B⟩$
111		sraval	$⊢ (R \in V \land C \subseteq {Base}_{R}) \to subringAlg (R) (C) = ((R sSet ⟨Scalar (ndx), R ↾_{𝑠} C⟩) sSet ⟨\cdot_{ndx}, \cdot_{R}⟩) sSet ⟨\cdot_{𝑖} (ndx), \cdot_{R}⟩$
112	5 8 111	syl2anc	$⊢ φ \to subringAlg (R) (C) = ((R sSet ⟨Scalar (ndx), R ↾_{𝑠} C⟩) sSet ⟨\cdot_{ndx}, \cdot_{R}⟩) sSet ⟨\cdot_{𝑖} (ndx), \cdot_{R}⟩$
113	112	oveq1d	$⊢ φ \to subringAlg (R) (C) sSet ⟨{Base}_{ndx}, B⟩ = (((R sSet ⟨Scalar (ndx), R ↾_{𝑠} C⟩) sSet ⟨\cdot_{ndx}, \cdot_{R}⟩) sSet ⟨\cdot_{𝑖} (ndx), \cdot_{R}⟩) sSet ⟨{Base}_{ndx}, B⟩$
114	113	adantr	$⊢ (φ \land \neg A \subseteq B) \to subringAlg (R) (C) sSet ⟨{Base}_{ndx}, B⟩ = (((R sSet ⟨Scalar (ndx), R ↾_{𝑠} C⟩) sSet ⟨\cdot_{ndx}, \cdot_{R}⟩) sSet ⟨\cdot_{𝑖} (ndx), \cdot_{R}⟩) sSet ⟨{Base}_{ndx}, B⟩$
115	105 110 114	3eqtrd	$⊢ (φ \land \neg A \subseteq B) \to subringAlg (R) (C) ↾_{𝑠} B = (((R sSet ⟨Scalar (ndx), R ↾_{𝑠} C⟩) sSet ⟨\cdot_{ndx}, \cdot_{R}⟩) sSet ⟨\cdot_{𝑖} (ndx), \cdot_{R}⟩) sSet ⟨{Base}_{ndx}, B⟩$
116	91 98 115	3eqtr4d	$⊢ (φ \land \neg A \subseteq B) \to subringAlg (S) (C) = subringAlg (R) (C) ↾_{𝑠} B$
117	34 116	pm2.61dan	$⊢ φ \to subringAlg (S) (C) = subringAlg (R) (C) ↾_{𝑠} B$

Metamath Proof Explorer

Theorem resssra

Proof