Metamath Proof Explorer


Theorem 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 φ B = Base K
subrgpropd.2 φ B = Base L
subrgpropd.3 φ x B y B x + K y = x + L y
subrgpropd.4 φ x B y B x K y = x L y
Assertion subrgpropd φ SubRing K = SubRing L

Proof

Step Hyp Ref Expression
1 subrgpropd.1 φ B = Base K
2 subrgpropd.2 φ B = Base L
3 subrgpropd.3 φ x B y B x + K y = x + L y
4 subrgpropd.4 φ x B y B x K y = x L y
5 1 2 3 4 ringpropd φ K Ring L Ring
6 1 ineq2d φ s B = s Base K
7 eqid K 𝑠 s = K 𝑠 s
8 eqid Base K = Base K
9 7 8 ressbas s V s Base K = Base K 𝑠 s
10 9 elv s Base K = Base K 𝑠 s
11 6 10 eqtrdi φ s B = Base K 𝑠 s
12 2 ineq2d φ s B = s Base L
13 eqid L 𝑠 s = L 𝑠 s
14 eqid Base L = Base L
15 13 14 ressbas s V s Base L = Base L 𝑠 s
16 15 elv s Base L = Base L 𝑠 s
17 12 16 eqtrdi φ s B = Base L 𝑠 s
18 elinel2 x s B x B
19 elinel2 y s B y B
20 18 19 anim12i x s B y s B x B y B
21 eqid + K = + K
22 7 21 ressplusg s V + 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 V + L = + L 𝑠 s
27 26 elv + L = + L 𝑠 s
28 27 oveqi x + L y = x + L 𝑠 s y
29 3 24 28 3eqtr3g φ x B y B x + K 𝑠 s y = x + L 𝑠 s y
30 20 29 sylan2 φ x s B y s B x + K 𝑠 s y = x + L 𝑠 s y
31 eqid K = K
32 7 31 ressmulr s V K = K 𝑠 s
33 32 elv K = K 𝑠 s
34 33 oveqi x K y = x K 𝑠 s y
35 eqid L = L
36 13 35 ressmulr s V L = L 𝑠 s
37 36 elv L = L 𝑠 s
38 37 oveqi x L y = x L 𝑠 s y
39 4 34 38 3eqtr3g φ x B y B x K 𝑠 s y = x L 𝑠 s y
40 20 39 sylan2 φ x s B y s B x K 𝑠 s y = x L 𝑠 s y
41 11 17 30 40 ringpropd φ K 𝑠 s Ring L 𝑠 s Ring
42 5 41 anbi12d φ K Ring K 𝑠 s Ring L Ring L 𝑠 s Ring
43 1 2 eqtr3d φ Base K = Base L
44 43 sseq2d φ s Base K s Base L
45 1 2 4 rngidpropd φ 1 K = 1 L
46 45 eleq1d φ 1 K s 1 L s
47 44 46 anbi12d φ s Base K 1 K s s Base L 1 L s
48 42 47 anbi12d φ K Ring K 𝑠 s Ring s Base K 1 K s L Ring L 𝑠 s Ring s Base L 1 L s
49 eqid 1 K = 1 K
50 8 49 issubrg s SubRing K K Ring K 𝑠 s Ring s Base K 1 K s
51 eqid 1 L = 1 L
52 14 51 issubrg s SubRing L L Ring L 𝑠 s Ring s Base L 1 L s
53 48 50 52 3bitr4g φ s SubRing K s SubRing L
54 53 eqrdv φ SubRing K = SubRing L