Metamath Proof Explorer

Theorem dvdsrpropd

Description: The divisibility relation depends only on the ring's base set and multiplication operation. (Contributed by Mario Carneiro, 26-Dec-2014)

Ref Expression
Hypotheses rngidpropd.1 
|- ( ph -> B = ( Base ` K ) )
rngidpropd.2 
|- ( ph -> B = ( Base ` L ) )
rngidpropd.3 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )
Assertion dvdsrpropd 
|- ( ph -> ( ||r ` K ) = ( ||r ` L ) )

Proof

Step Hyp Ref Expression
1 rngidpropd.1 
 |-  ( ph -> B = ( Base ` K ) )
2 rngidpropd.2 
 |-  ( ph -> B = ( Base ` L ) )
3 rngidpropd.3 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )
4 3 anassrs 
 |-  ( ( ( ph /\ x e. B ) /\ y e. B ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )
5 4 eqeq1d 
 |-  ( ( ( ph /\ x e. B ) /\ y e. B ) -> ( ( x ( .r ` K ) y ) = z <-> ( x ( .r ` L ) y ) = z ) )
6 5 an32s 
 |-  ( ( ( ph /\ y e. B ) /\ x e. B ) -> ( ( x ( .r ` K ) y ) = z <-> ( x ( .r ` L ) y ) = z ) )
7 6 rexbidva 
 |-  ( ( ph /\ y e. B ) -> ( E. x e. B ( x ( .r ` K ) y ) = z <-> E. x e. B ( x ( .r ` L ) y ) = z ) )
8 7 pm5.32da 
 |-  ( ph -> ( ( y e. B /\ E. x e. B ( x ( .r ` K ) y ) = z ) <-> ( y e. B /\ E. x e. B ( x ( .r ` L ) y ) = z ) ) )
9 1 eleq2d 
 |-  ( ph -> ( y e. B <-> y e. ( Base ` K ) ) )
10 1 rexeqdv 
 |-  ( ph -> ( E. x e. B ( x ( .r ` K ) y ) = z <-> E. x e. ( Base ` K ) ( x ( .r ` K ) y ) = z ) )
11 9 10 anbi12d 
 |-  ( ph -> ( ( y e. B /\ E. x e. B ( x ( .r ` K ) y ) = z ) <-> ( y e. ( Base ` K ) /\ E. x e. ( Base ` K ) ( x ( .r ` K ) y ) = z ) ) )
12 2 eleq2d 
 |-  ( ph -> ( y e. B <-> y e. ( Base ` L ) ) )
13 2 rexeqdv 
 |-  ( ph -> ( E. x e. B ( x ( .r ` L ) y ) = z <-> E. x e. ( Base ` L ) ( x ( .r ` L ) y ) = z ) )
14 12 13 anbi12d 
 |-  ( ph -> ( ( y e. B /\ E. x e. B ( x ( .r ` L ) y ) = z ) <-> ( y e. ( Base ` L ) /\ E. x e. ( Base ` L ) ( x ( .r ` L ) y ) = z ) ) )
15 8 11 14 3bitr3d 
 |-  ( ph -> ( ( y e. ( Base ` K ) /\ E. x e. ( Base ` K ) ( x ( .r ` K ) y ) = z ) <-> ( y e. ( Base ` L ) /\ E. x e. ( Base ` L ) ( x ( .r ` L ) y ) = z ) ) )
16 15 opabbidv 
 |-  ( ph -> { <. y , z >. | ( y e. ( Base ` K ) /\ E. x e. ( Base ` K ) ( x ( .r ` K ) y ) = z ) } = { <. y , z >. | ( y e. ( Base ` L ) /\ E. x e. ( Base ` L ) ( x ( .r ` L ) y ) = z ) } )
17 eqid 
 |-  ( Base ` K ) = ( Base ` K )
18 eqid 
 |-  ( ||r ` K ) = ( ||r ` K )
19 eqid 
 |-  ( .r ` K ) = ( .r ` K )
20 17 18 19 dvdsrval 
 |-  ( ||r ` K ) = { <. y , z >. | ( y e. ( Base ` K ) /\ E. x e. ( Base ` K ) ( x ( .r ` K ) y ) = z ) }
21 eqid 
 |-  ( Base ` L ) = ( Base ` L )
22 eqid 
 |-  ( ||r ` L ) = ( ||r ` L )
23 eqid 
 |-  ( .r ` L ) = ( .r ` L )
24 21 22 23 dvdsrval 
 |-  ( ||r ` L ) = { <. y , z >. | ( y e. ( Base ` L ) /\ E. x e. ( Base ` L ) ( x ( .r ` L ) y ) = z ) }
25 16 20 24 3eqtr4g 
 |-  ( ph -> ( ||r ` K ) = ( ||r ` L ) )