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 ⊢ φ → B = Base K
domnpropd.2 ⊢ φ → B = Base L
domnpropd.3 ⊢ φ ∧ x ∈ B ∧ y ∈ B → x + K y = x + L y
domnpropd.4 ⊢ φ ∧ x ∈ B ∧ y ∈ B → x ⋅ K y = x ⋅ L y
Assertion domnpropd ⊢ φ → K ∈ Domn ↔ L ∈ Domn

Proof

Step Hyp Ref Expression
1 domnpropd.1 ⊢ φ → B = Base K
2 domnpropd.2 ⊢ φ → B = Base L
3 domnpropd.3 ⊢ φ ∧ x ∈ B ∧ y ∈ B → x + K y = x + L y
4 domnpropd.4 ⊢ φ ∧ x ∈ B ∧ y ∈ B → x ⋅ K y = x ⋅ L y
5 1 2 3 4 nzrpropd ⊢ φ → K ∈ NzRing ↔ L ∈ NzRing
6 1 2 eqtr3d ⊢ φ → Base K = Base L
7 6 adantr ⊢ φ ∧ x ∈ Base K → Base K = Base L
8 simpll ⊢ φ ∧ x ∈ Base K ∧ y ∈ Base K → φ
9 1 eleq2d ⊢ φ → x ∈ B ↔ x ∈ Base K
10 9 biimpar ⊢ φ ∧ x ∈ Base K → x ∈ B
11 10 adantr ⊢ φ ∧ x ∈ Base K ∧ y ∈ Base K → x ∈ B
12 1 eleq2d ⊢ φ → y ∈ B ↔ y ∈ Base K
13 12 biimpar ⊢ φ ∧ y ∈ Base K → y ∈ B
14 13 adantlr ⊢ φ ∧ x ∈ Base K ∧ y ∈ Base K → y ∈ B
15 8 11 14 4 syl12anc ⊢ φ ∧ x ∈ Base K ∧ y ∈ Base K → x ⋅ K y = x ⋅ L y
16 1 2 3 grpidpropd ⊢ φ → 0 K = 0 L
17 16 ad2antrr ⊢ φ ∧ x ∈ Base K ∧ y ∈ Base K → 0 K = 0 L
18 15 17 eqeq12d ⊢ φ ∧ x ∈ Base K ∧ y ∈ Base K → x ⋅ K y = 0 K ↔ x ⋅ L y = 0 L
19 17 eqeq2d ⊢ φ ∧ x ∈ Base K ∧ y ∈ Base K → x = 0 K ↔ x = 0 L
20 17 eqeq2d ⊢ φ ∧ x ∈ Base K ∧ y ∈ Base K → y = 0 K ↔ y = 0 L
21 19 20 orbi12d ⊢ φ ∧ x ∈ Base K ∧ y ∈ Base K → x = 0 K ∨ y = 0 K ↔ x = 0 L ∨ y = 0 L
22 18 21 imbi12d ⊢ φ ∧ x ∈ Base K ∧ y ∈ Base K → x ⋅ K y = 0 K → x = 0 K ∨ y = 0 K ↔ x ⋅ L y = 0 L → x = 0 L ∨ y = 0 L
23 7 22 raleqbidva ⊢ φ ∧ x ∈ Base K → ∀ y ∈ Base K x ⋅ K y = 0 K → x = 0 K ∨ y = 0 K ↔ ∀ y ∈ Base L x ⋅ L y = 0 L → x = 0 L ∨ y = 0 L
24 6 23 raleqbidva ⊢ φ → ∀ x ∈ Base K ∀ y ∈ Base K x ⋅ K y = 0 K → x = 0 K ∨ y = 0 K ↔ ∀ x ∈ Base L ∀ y ∈ Base L x ⋅ L y = 0 L → x = 0 L ∨ y = 0 L
25 5 24 anbi12d ⊢ φ → K ∈ NzRing ∧ ∀ x ∈ Base K ∀ y ∈ Base K x ⋅ K y = 0 K → x = 0 K ∨ y = 0 K ↔ L ∈ NzRing ∧ ∀ x ∈ Base L ∀ y ∈ Base L x ⋅ L y = 0 L → x = 0 L ∨ y = 0 L
26 eqid ⊢ Base K = Base K
27 eqid ⊢ ⋅ K = ⋅ K
28 eqid ⊢ 0 K = 0 K
29 26 27 28 isdomn ⊢ K ∈ Domn ↔ K ∈ NzRing ∧ ∀ x ∈ Base K ∀ y ∈ Base K x ⋅ K y = 0 K → x = 0 K ∨ y = 0 K
30 eqid ⊢ Base L = Base L
31 eqid ⊢ ⋅ L = ⋅ L
32 eqid ⊢ 0 L = 0 L
33 30 31 32 isdomn ⊢ L ∈ Domn ↔ L ∈ NzRing ∧ ∀ x ∈ Base L ∀ y ∈ Base L x ⋅ L y = 0 L → x = 0 L ∨ y = 0 L
34 25 29 33 3bitr4g ⊢ φ → K ∈ Domn ↔ L ∈ Domn