This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem domnpropd

Description: If two structures have the same components (properties), one is a domain iff the other one is. (Contributed by Thierry Arnoux, 13-Oct-2025)

Ref Expression
Hypotheses domnpropd.1 
|- ( ph -> B = ( Base ` K ) )
domnpropd.2 
|- ( ph -> B = ( Base ` L ) )
domnpropd.3 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
domnpropd.4 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )
Assertion domnpropd 
|- ( ph -> ( K e. Domn <-> L e. Domn ) )

Proof

Step Hyp Ref Expression
1 domnpropd.1 
 |-  ( ph -> B = ( Base ` K ) )
2 domnpropd.2 
 |-  ( ph -> B = ( Base ` L ) )
3 domnpropd.3 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
4 domnpropd.4 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )
5 1 2 3 4 nzrpropd 
 |-  ( ph -> ( K e. NzRing <-> L e. NzRing ) )
6 1 2 eqtr3d 
 |-  ( ph -> ( Base ` K ) = ( Base ` L ) )
7 6 adantr 
 |-  ( ( ph /\ x e. ( Base ` K ) ) -> ( Base ` K ) = ( Base ` L ) )
8 simpll 
 |-  ( ( ( ph /\ x e. ( Base ` K ) ) /\ y e. ( Base ` K ) ) -> ph )
9 1 eleq2d 
 |-  ( ph -> ( x e. B <-> x e. ( Base ` K ) ) )
10 9 biimpar 
 |-  ( ( ph /\ x e. ( Base ` K ) ) -> x e. B )
11 10 adantr 
 |-  ( ( ( ph /\ x e. ( Base ` K ) ) /\ y e. ( Base ` K ) ) -> x e. B )
12 1 eleq2d 
 |-  ( ph -> ( y e. B <-> y e. ( Base ` K ) ) )
13 12 biimpar 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> y e. B )
14 13 adantlr 
 |-  ( ( ( ph /\ x e. ( Base ` K ) ) /\ y e. ( Base ` K ) ) -> y e. B )
15 8 11 14 4 syl12anc 
 |-  ( ( ( ph /\ x e. ( Base ` K ) ) /\ y e. ( Base ` K ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )
16 1 2 3 grpidpropd 
 |-  ( ph -> ( 0g ` K ) = ( 0g ` L ) )
17 16 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` K ) ) /\ y e. ( Base ` K ) ) -> ( 0g ` K ) = ( 0g ` L ) )
18 15 17 eqeq12d 
 |-  ( ( ( ph /\ x e. ( Base ` K ) ) /\ y e. ( Base ` K ) ) -> ( ( x ( .r ` K ) y ) = ( 0g ` K ) <-> ( x ( .r ` L ) y ) = ( 0g ` L ) ) )
19 17 eqeq2d 
 |-  ( ( ( ph /\ x e. ( Base ` K ) ) /\ y e. ( Base ` K ) ) -> ( x = ( 0g ` K ) <-> x = ( 0g ` L ) ) )
20 17 eqeq2d 
 |-  ( ( ( ph /\ x e. ( Base ` K ) ) /\ y e. ( Base ` K ) ) -> ( y = ( 0g ` K ) <-> y = ( 0g ` L ) ) )
21 19 20 orbi12d 
 |-  ( ( ( ph /\ x e. ( Base ` K ) ) /\ y e. ( Base ` K ) ) -> ( ( x = ( 0g ` K ) \/ y = ( 0g ` K ) ) <-> ( x = ( 0g ` L ) \/ y = ( 0g ` L ) ) ) )
22 18 21 imbi12d 
 |-  ( ( ( ph /\ x e. ( Base ` K ) ) /\ y e. ( Base ` K ) ) -> ( ( ( x ( .r ` K ) y ) = ( 0g ` K ) -> ( x = ( 0g ` K ) \/ y = ( 0g ` K ) ) ) <-> ( ( x ( .r ` L ) y ) = ( 0g ` L ) -> ( x = ( 0g ` L ) \/ y = ( 0g ` L ) ) ) ) )
23 7 22 raleqbidva 
 |-  ( ( ph /\ x e. ( Base ` K ) ) -> ( A. y e. ( Base ` K ) ( ( x ( .r ` K ) y ) = ( 0g ` K ) -> ( x = ( 0g ` K ) \/ y = ( 0g ` K ) ) ) <-> A. y e. ( Base ` L ) ( ( x ( .r ` L ) y ) = ( 0g ` L ) -> ( x = ( 0g ` L ) \/ y = ( 0g ` L ) ) ) ) )
24 6 23 raleqbidva 
 |-  ( ph -> ( A. x e. ( Base ` K ) A. y e. ( Base ` K ) ( ( x ( .r ` K ) y ) = ( 0g ` K ) -> ( x = ( 0g ` K ) \/ y = ( 0g ` K ) ) ) <-> A. x e. ( Base ` L ) A. y e. ( Base ` L ) ( ( x ( .r ` L ) y ) = ( 0g ` L ) -> ( x = ( 0g ` L ) \/ y = ( 0g ` L ) ) ) ) )
25 5 24 anbi12d 
 |-  ( ph -> ( ( K e. NzRing /\ A. x e. ( Base ` K ) A. y e. ( Base ` K ) ( ( x ( .r ` K ) y ) = ( 0g ` K ) -> ( x = ( 0g ` K ) \/ y = ( 0g ` K ) ) ) ) <-> ( L e. NzRing /\ A. x e. ( Base ` L ) A. y e. ( Base ` L ) ( ( x ( .r ` L ) y ) = ( 0g ` L ) -> ( x = ( 0g ` L ) \/ y = ( 0g ` L ) ) ) ) ) )
26 eqid 
 |-  ( Base ` K ) = ( Base ` K )
27 eqid 
 |-  ( .r ` K ) = ( .r ` K )
28 eqid 
 |-  ( 0g ` K ) = ( 0g ` K )
29 26 27 28 isdomn 
 |-  ( K e. Domn <-> ( K e. NzRing /\ A. x e. ( Base ` K ) A. y e. ( Base ` K ) ( ( x ( .r ` K ) y ) = ( 0g ` K ) -> ( x = ( 0g ` K ) \/ y = ( 0g ` K ) ) ) ) )
30 eqid 
 |-  ( Base ` L ) = ( Base ` L )
31 eqid 
 |-  ( .r ` L ) = ( .r ` L )
32 eqid 
 |-  ( 0g ` L ) = ( 0g ` L )
33 30 31 32 isdomn 
 |-  ( L e. Domn <-> ( L e. NzRing /\ A. x e. ( Base ` L ) A. y e. ( Base ` L ) ( ( x ( .r ` L ) y ) = ( 0g ` L ) -> ( x = ( 0g ` L ) \/ y = ( 0g ` L ) ) ) ) )
34 25 29 33 3bitr4g 
 |-  ( ph -> ( K e. Domn <-> L e. Domn ) )