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 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
domnpropd.2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
domnpropd.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
domnpropd.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 ) )
Assertion domnpropd ( 𝜑 → ( 𝐾 ∈ Domn ↔ 𝐿 ∈ Domn ) )

Proof

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