Metamath Proof Explorer


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 φ B = Base K
subrngpropd.2 φ B = Base L
subrngpropd.3 φ x B y B x + K y = x + L y
subrngpropd.4 φ x B y B x K y = x 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 φ B = Base K
2 subrngpropd.2 φ B = Base L
3 subrngpropd.3 φ x B y B x + K y = x + L y
4 subrngpropd.4 φ x B y B x K y = x L y
5 1 2 3 4 rngpropd φ K Rng L Rng
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 rngpropd φ K 𝑠 s Rng L 𝑠 s Rng
42 1 2 eqtr3d φ Base K = Base L
43 42 sseq2d φ s Base K s Base L
44 5 41 43 3anbi123d φ K Rng K 𝑠 s Rng s Base K L Rng L 𝑠 s Rng s Base L
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 |-