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 
|- ( ph -> B = ( Base ` K ) )
subrngpropd.2 
|- ( ph -> B = ( Base ` L ) )
subrngpropd.3 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
subrngpropd.4 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )
Assertion subrngpropd 
|- ( ph -> ( SubRng ` K ) = ( SubRng ` L ) )

Proof

Step Hyp Ref Expression
1 subrngpropd.1 
 |-  ( ph -> B = ( Base ` K ) )
2 subrngpropd.2 
 |-  ( ph -> B = ( Base ` L ) )
3 subrngpropd.3 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
4 subrngpropd.4 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )
5 1 2 3 4 rngpropd 
 |-  ( ph -> ( K e. Rng <-> L e. Rng ) )
6 1 ineq2d 
 |-  ( ph -> ( s i^i B ) = ( s i^i ( Base ` K ) ) )
7 eqid 
 |-  ( K |`s s ) = ( K |`s s )
8 eqid 
 |-  ( Base ` K ) = ( Base ` K )
9 7 8 ressbas 
 |-  ( s e. _V -> ( s i^i ( Base ` K ) ) = ( Base ` ( K |`s s ) ) )
10 9 elv 
 |-  ( s i^i ( Base ` K ) ) = ( Base ` ( K |`s s ) )
11 6 10 eqtrdi 
 |-  ( ph -> ( s i^i B ) = ( Base ` ( K |`s s ) ) )
12 2 ineq2d 
 |-  ( ph -> ( s i^i B ) = ( s i^i ( Base ` L ) ) )
13 eqid 
 |-  ( L |`s s ) = ( L |`s s )
14 eqid 
 |-  ( Base ` L ) = ( Base ` L )
15 13 14 ressbas 
 |-  ( s e. _V -> ( s i^i ( Base ` L ) ) = ( Base ` ( L |`s s ) ) )
16 15 elv 
 |-  ( s i^i ( Base ` L ) ) = ( Base ` ( L |`s s ) )
17 12 16 eqtrdi 
 |-  ( ph -> ( s i^i B ) = ( Base ` ( L |`s s ) ) )
18 elinel2 
 |-  ( x e. ( s i^i B ) -> x e. B )
19 elinel2 
 |-  ( y e. ( s i^i B ) -> y e. B )
20 18 19 anim12i 
 |-  ( ( x e. ( s i^i B ) /\ y e. ( s i^i B ) ) -> ( x e. B /\ y e. B ) )
21 eqid 
 |-  ( +g ` K ) = ( +g ` K )
22 7 21 ressplusg 
 |-  ( s e. _V -> ( +g ` K ) = ( +g ` ( K |`s s ) ) )
23 22 elv 
 |-  ( +g ` K ) = ( +g ` ( K |`s s ) )
24 23 oveqi 
 |-  ( x ( +g ` K ) y ) = ( x ( +g ` ( K |`s s ) ) y )
25 eqid 
 |-  ( +g ` L ) = ( +g ` L )
26 13 25 ressplusg 
 |-  ( s e. _V -> ( +g ` L ) = ( +g ` ( L |`s s ) ) )
27 26 elv 
 |-  ( +g ` L ) = ( +g ` ( L |`s s ) )
28 27 oveqi 
 |-  ( x ( +g ` L ) y ) = ( x ( +g ` ( L |`s s ) ) y )
29 3 24 28 3eqtr3g 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` ( K |`s s ) ) y ) = ( x ( +g ` ( L |`s s ) ) y ) )
30 20 29 sylan2 
 |-  ( ( ph /\ ( x e. ( s i^i B ) /\ y e. ( s i^i B ) ) ) -> ( x ( +g ` ( K |`s s ) ) y ) = ( x ( +g ` ( L |`s s ) ) y ) )
31 eqid 
 |-  ( .r ` K ) = ( .r ` K )
32 7 31 ressmulr 
 |-  ( s e. _V -> ( .r ` K ) = ( .r ` ( K |`s s ) ) )
33 32 elv 
 |-  ( .r ` K ) = ( .r ` ( K |`s s ) )
34 33 oveqi 
 |-  ( x ( .r ` K ) y ) = ( x ( .r ` ( K |`s s ) ) y )
35 eqid 
 |-  ( .r ` L ) = ( .r ` L )
36 13 35 ressmulr 
 |-  ( s e. _V -> ( .r ` L ) = ( .r ` ( L |`s s ) ) )
37 36 elv 
 |-  ( .r ` L ) = ( .r ` ( L |`s s ) )
38 37 oveqi 
 |-  ( x ( .r ` L ) y ) = ( x ( .r ` ( L |`s s ) ) y )
39 4 34 38 3eqtr3g 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` ( K |`s s ) ) y ) = ( x ( .r ` ( L |`s s ) ) y ) )
40 20 39 sylan2 
 |-  ( ( ph /\ ( x e. ( s i^i B ) /\ y e. ( s i^i B ) ) ) -> ( x ( .r ` ( K |`s s ) ) y ) = ( x ( .r ` ( L |`s s ) ) y ) )
41 11 17 30 40 rngpropd 
 |-  ( ph -> ( ( K |`s s ) e. Rng <-> ( L |`s s ) e. Rng ) )
42 1 2 eqtr3d 
 |-  ( ph -> ( Base ` K ) = ( Base ` L ) )
43 42 sseq2d 
 |-  ( ph -> ( s C_ ( Base ` K ) <-> s C_ ( Base ` L ) ) )
44 5 41 43 3anbi123d 
 |-  ( ph -> ( ( K e. Rng /\ ( K |`s s ) e. Rng /\ s C_ ( Base ` K ) ) <-> ( L e. Rng /\ ( L |`s s ) e. Rng /\ s C_ ( Base ` L ) ) ) )
45 8 issubrng 
 |-  ( s e. ( SubRng ` K ) <-> ( K e. Rng /\ ( K |`s s ) e. Rng /\ s C_ ( Base ` K ) ) )
46 14 issubrng 
 |-  ( s e. ( SubRng ` L ) <-> ( L e. Rng /\ ( L |`s s ) e. Rng /\ s C_ ( Base ` L ) ) )
47 44 45 46 3bitr4g 
 |-  ( ph -> ( s e. ( SubRng ` K ) <-> s e. ( SubRng ` L ) ) )
48 47 eqrdv 
 |-  ( ph -> ( SubRng ` K ) = ( SubRng ` L ) )