subrgpropd

Description: If two structures have the same group components (properties), they have the same set of subrings. (Contributed by Mario Carneiro, 9-Feb-2015)

	Ref	Expression
Hypotheses	subrgpropd.1	$⊢ φ \to B = {Base}_{K}$
	subrgpropd.2	$⊢ φ \to B = {Base}_{L}$
	subrgpropd.3	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{K} y = x +_{L} y$
	subrgpropd.4	$⊢ (φ \land (x \in B \land y \in B)) \to x \cdot_{K} y = x \cdot_{L} y$
Assertion	subrgpropd	$⊢ φ \to SubRing (K) = SubRing (L)$

Proof

Step	Hyp	Ref	Expression
1		subrgpropd.1	$⊢ φ \to B = {Base}_{K}$
2		subrgpropd.2	$⊢ φ \to B = {Base}_{L}$
3		subrgpropd.3	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{K} y = x +_{L} y$
4		subrgpropd.4	$⊢ (φ \land (x \in B \land y \in B)) \to x \cdot_{K} y = x \cdot_{L} y$
5	1 2 3 4	ringpropd	$⊢ φ \to (K \in Ring \leftrightarrow L \in Ring)$
6	1	ineq2d	$⊢ φ \to s \cap B = s \cap {Base}_{K}$
7		eqid	$⊢ K ↾_{𝑠} s = K ↾_{𝑠} s$
8		eqid	$⊢ {Base}_{K} = {Base}_{K}$
9	7 8	ressbas	$⊢ s \in V \to s \cap {Base}_{K} = {Base}_{(K ↾_{𝑠} s)}$
10	9	elv	$⊢ s \cap {Base}_{K} = {Base}_{(K ↾_{𝑠} s)}$
11	6 10	eqtrdi	$⊢ φ \to s \cap B = {Base}_{(K ↾_{𝑠} s)}$
12	2	ineq2d	$⊢ φ \to s \cap B = s \cap {Base}_{L}$
13		eqid	$⊢ L ↾_{𝑠} s = L ↾_{𝑠} s$
14		eqid	$⊢ {Base}_{L} = {Base}_{L}$
15	13 14	ressbas	$⊢ s \in V \to s \cap {Base}_{L} = {Base}_{(L ↾_{𝑠} s)}$
16	15	elv	$⊢ s \cap {Base}_{L} = {Base}_{(L ↾_{𝑠} s)}$
17	12 16	eqtrdi	$⊢ φ \to s \cap B = {Base}_{(L ↾_{𝑠} s)}$
18		elinel2	$⊢ x \in (s \cap B) \to x \in B$
19		elinel2	$⊢ y \in (s \cap B) \to y \in B$
20	18 19	anim12i	$⊢ (x \in (s \cap B) \land y \in (s \cap B)) \to (x \in B \land y \in B)$
21		eqid	$⊢ +_{K} = +_{K}$
22	7 21	ressplusg	$⊢ s \in V \to +_{K} = +_{(K ↾_{𝑠} s)}$
23	22	elv	$⊢ +_{K} = +_{(K ↾_{𝑠} s)}$
24	23	oveqi	$⊢ x +_{K} y = x +_{(K ↾_{𝑠} s)} y$
25		eqid	$⊢ +_{L} = +_{L}$
26	13 25	ressplusg	$⊢ s \in V \to +_{L} = +_{(L ↾_{𝑠} s)}$
27	26	elv	$⊢ +_{L} = +_{(L ↾_{𝑠} s)}$
28	27	oveqi	$⊢ x +_{L} y = x +_{(L ↾_{𝑠} s)} y$
29	3 24 28	3eqtr3g	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{(K ↾_{𝑠} s)} y = x +_{(L ↾_{𝑠} s)} y$
30	20 29	sylan2	$⊢ (φ \land (x \in (s \cap B) \land y \in (s \cap B))) \to x +_{(K ↾_{𝑠} s)} y = x +_{(L ↾_{𝑠} s)} y$
31		eqid	$⊢ \cdot_{K} = \cdot_{K}$
32	7 31	ressmulr	$⊢ s \in V \to \cdot_{K} = \cdot_{(K ↾_{𝑠} s)}$
33	32	elv	$⊢ \cdot_{K} = \cdot_{(K ↾_{𝑠} s)}$
34	33	oveqi	$⊢ x \cdot_{K} y = x \cdot_{(K ↾_{𝑠} s)} y$
35		eqid	$⊢ \cdot_{L} = \cdot_{L}$
36	13 35	ressmulr	$⊢ s \in V \to \cdot_{L} = \cdot_{(L ↾_{𝑠} s)}$
37	36	elv	$⊢ \cdot_{L} = \cdot_{(L ↾_{𝑠} s)}$
38	37	oveqi	$⊢ x \cdot_{L} y = x \cdot_{(L ↾_{𝑠} s)} y$
39	4 34 38	3eqtr3g	$⊢ (φ \land (x \in B \land y \in B)) \to x \cdot_{(K ↾_{𝑠} s)} y = x \cdot_{(L ↾_{𝑠} s)} y$
40	20 39	sylan2	$⊢ (φ \land (x \in (s \cap B) \land y \in (s \cap B))) \to x \cdot_{(K ↾_{𝑠} s)} y = x \cdot_{(L ↾_{𝑠} s)} y$
41	11 17 30 40	ringpropd	$⊢ φ \to (K ↾_{𝑠} s \in Ring \leftrightarrow L ↾_{𝑠} s \in Ring)$
42	5 41	anbi12d	$⊢ φ \to ((K \in Ring \land K ↾_{𝑠} s \in Ring) \leftrightarrow (L \in Ring \land L ↾_{𝑠} s \in Ring))$
43	1 2	eqtr3d	$⊢ φ \to {Base}_{K} = {Base}_{L}$
44	43	sseq2d	$⊢ φ \to (s \subseteq {Base}_{K} \leftrightarrow s \subseteq {Base}_{L})$
45	1 2 4	rngidpropd	$⊢ φ \to 1_{K} = 1_{L}$
46	45	eleq1d	$⊢ φ \to (1_{K} \in s \leftrightarrow 1_{L} \in s)$
47	44 46	anbi12d	$⊢ φ \to ((s \subseteq {Base}_{K} \land 1_{K} \in s) \leftrightarrow (s \subseteq {Base}_{L} \land 1_{L} \in s))$
48	42 47	anbi12d	$⊢ φ \to (((K \in Ring \land K ↾_{𝑠} s \in Ring) \land (s \subseteq {Base}_{K} \land 1_{K} \in s)) \leftrightarrow ((L \in Ring \land L ↾_{𝑠} s \in Ring) \land (s \subseteq {Base}_{L} \land 1_{L} \in s)))$
49		eqid	$⊢ 1_{K} = 1_{K}$
50	8 49	issubrg	$⊢ s \in SubRing (K) \leftrightarrow ((K \in Ring \land K ↾_{𝑠} s \in Ring) \land (s \subseteq {Base}_{K} \land 1_{K} \in s))$
51		eqid	$⊢ 1_{L} = 1_{L}$
52	14 51	issubrg	$⊢ s \in SubRing (L) \leftrightarrow ((L \in Ring \land L ↾_{𝑠} s \in Ring) \land (s \subseteq {Base}_{L} \land 1_{L} \in s))$
53	48 50 52	3bitr4g	$⊢ φ \to (s \in SubRing (K) \leftrightarrow s \in SubRing (L))$
54	53	eqrdv	$⊢ φ \to SubRing (K) = SubRing (L)$

Metamath Proof Explorer

Theorem subrgpropd

Proof