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

Proof

Step Hyp Ref Expression
1 subrgpropd.1 
 |-  ( ph -> B = ( Base ` K ) )
2 subrgpropd.2 
 |-  ( ph -> B = ( Base ` L ) )
3 subrgpropd.3 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
4 subrgpropd.4 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )
5 1 2 3 4 ringpropd 
 |-  ( ph -> ( K e. Ring <-> L e. Ring ) )
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 ringpropd 
 |-  ( ph -> ( ( K |`s s ) e. Ring <-> ( L |`s s ) e. Ring ) )
42 5 41 anbi12d 
 |-  ( ph -> ( ( K e. Ring /\ ( K |`s s ) e. Ring ) <-> ( L e. Ring /\ ( L |`s s ) e. Ring ) ) )
43 1 2 eqtr3d 
 |-  ( ph -> ( Base ` K ) = ( Base ` L ) )
44 43 sseq2d 
 |-  ( ph -> ( s C_ ( Base ` K ) <-> s C_ ( Base ` L ) ) )
45 1 2 4 rngidpropd 
 |-  ( ph -> ( 1r ` K ) = ( 1r ` L ) )
46 45 eleq1d 
 |-  ( ph -> ( ( 1r ` K ) e. s <-> ( 1r ` L ) e. s ) )
47 44 46 anbi12d 
 |-  ( ph -> ( ( s C_ ( Base ` K ) /\ ( 1r ` K ) e. s ) <-> ( s C_ ( Base ` L ) /\ ( 1r ` L ) e. s ) ) )
48 42 47 anbi12d 
 |-  ( ph -> ( ( ( K e. Ring /\ ( K |`s s ) e. Ring ) /\ ( s C_ ( Base ` K ) /\ ( 1r ` K ) e. s ) ) <-> ( ( L e. Ring /\ ( L |`s s ) e. Ring ) /\ ( s C_ ( Base ` L ) /\ ( 1r ` L ) e. s ) ) ) )
49 eqid 
 |-  ( 1r ` K ) = ( 1r ` K )
50 8 49 issubrg 
 |-  ( s e. ( SubRing ` K ) <-> ( ( K e. Ring /\ ( K |`s s ) e. Ring ) /\ ( s C_ ( Base ` K ) /\ ( 1r ` K ) e. s ) ) )
51 eqid 
 |-  ( 1r ` L ) = ( 1r ` L )
52 14 51 issubrg 
 |-  ( s e. ( SubRing ` L ) <-> ( ( L e. Ring /\ ( L |`s s ) e. Ring ) /\ ( s C_ ( Base ` L ) /\ ( 1r ` L ) e. s ) ) )
53 48 50 52 3bitr4g 
 |-  ( ph -> ( s e. ( SubRing ` K ) <-> s e. ( SubRing ` L ) ) )
54 53 eqrdv 
 |-  ( ph -> ( SubRing ` K ) = ( SubRing ` L ) )