Metamath Proof Explorer

Theorem lazcjcl

Description: The extended integers are closed under conjugation if the conjugation of the adjoined complex number is an extended integer. (Contributed by AV, 26-Oct-2026)

Ref Expression
Hypothesis laznegcl.r ⊢ 𝑅 = ( Z[]l ‘ 𝑆 )
Assertion lazcjcl ( ( 𝑆 ∈ ℂ ∧ ( ∗ ‘ 𝑆 ) ∈ 𝑅 ) → ( 𝐴 ∈ 𝑅 → ( ∗ ‘ 𝐴 ) ∈ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 laznegcl.r ⊢ 𝑅 = ( Z[]l ‘ 𝑆 )
2 1 eleq2i ⊢ ( 𝐴 ∈ 𝑅 ↔ 𝐴 ∈ ( Z[]l ‘ 𝑆 ) )
3 ellazim ⊢ ( ( 𝑆 ∈ ℂ ∧ 𝐴 ∈ ( Z[]l ‘ 𝑆 ) ) → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) )
4 3 ex ⊢ ( 𝑆 ∈ ℂ → ( 𝐴 ∈ ( Z[]l ‘ 𝑆 ) → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) )
5 4 adantr ⊢ ( ( 𝑆 ∈ ℂ ∧ ( ∗ ‘ 𝑆 ) ∈ 𝑅 ) → ( 𝐴 ∈ ( Z[]l ‘ 𝑆 ) → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) )
6 2 5 biimtrid ⊢ ( ( 𝑆 ∈ ℂ ∧ ( ∗ ‘ 𝑆 ) ∈ 𝑅 ) → ( 𝐴 ∈ 𝑅 → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) )
7 fveq2 ⊢ ( 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) → ( ∗ ‘ 𝐴 ) = ( ∗ ‘ ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) )
8 zcn ⊢ ( 𝑎 ∈ ℤ → 𝑎 ∈ ℂ )
9 8 ad2antrl ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( ∗ ‘ 𝑆 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑎 ∈ ℂ )
10 zcn ⊢ ( 𝑏 ∈ ℤ → 𝑏 ∈ ℂ )
11 10 adantl ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → 𝑏 ∈ ℂ )
12 simpl ⊢ ( ( 𝑆 ∈ ℂ ∧ ( ∗ ‘ 𝑆 ) ∈ 𝑅 ) → 𝑆 ∈ ℂ )
13 mulcl ⊢ ( ( 𝑏 ∈ ℂ ∧ 𝑆 ∈ ℂ ) → ( 𝑏 · 𝑆 ) ∈ ℂ )
14 11 12 13 syl2anr ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( ∗ ‘ 𝑆 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑏 · 𝑆 ) ∈ ℂ )
15 9 14 cjaddd ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( ∗ ‘ 𝑆 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ∗ ‘ ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) = ( ( ∗ ‘ 𝑎 ) + ( ∗ ‘ ( 𝑏 · 𝑆 ) ) ) )
16 zre ⊢ ( 𝑎 ∈ ℤ → 𝑎 ∈ ℝ )
17 16 ad2antrl ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( ∗ ‘ 𝑆 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑎 ∈ ℝ )
18 17 cjred ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( ∗ ‘ 𝑆 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ∗ ‘ 𝑎 ) = 𝑎 )
19 11 adantl ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( ∗ ‘ 𝑆 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑏 ∈ ℂ )
20 12 adantr ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( ∗ ‘ 𝑆 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑆 ∈ ℂ )
21 19 20 cjmuld ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( ∗ ‘ 𝑆 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ∗ ‘ ( 𝑏 · 𝑆 ) ) = ( ( ∗ ‘ 𝑏 ) · ( ∗ ‘ 𝑆 ) ) )
22 zre ⊢ ( 𝑏 ∈ ℤ → 𝑏 ∈ ℝ )
23 22 adantl ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → 𝑏 ∈ ℝ )
24 23 adantl ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( ∗ ‘ 𝑆 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑏 ∈ ℝ )
25 24 cjred ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( ∗ ‘ 𝑆 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ∗ ‘ 𝑏 ) = 𝑏 )
26 25 oveq1d ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( ∗ ‘ 𝑆 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( ∗ ‘ 𝑏 ) · ( ∗ ‘ 𝑆 ) ) = ( 𝑏 · ( ∗ ‘ 𝑆 ) ) )
27 21 26 eqtrd ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( ∗ ‘ 𝑆 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ∗ ‘ ( 𝑏 · 𝑆 ) ) = ( 𝑏 · ( ∗ ‘ 𝑆 ) ) )
28 18 27 oveq12d ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( ∗ ‘ 𝑆 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( ∗ ‘ 𝑎 ) + ( ∗ ‘ ( 𝑏 · 𝑆 ) ) ) = ( 𝑎 + ( 𝑏 · ( ∗ ‘ 𝑆 ) ) ) )
29 15 28 eqtrd ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( ∗ ‘ 𝑆 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ∗ ‘ ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) = ( 𝑎 + ( 𝑏 · ( ∗ ‘ 𝑆 ) ) ) )
30 7 29 sylan9eqr ⊢ ( ( ( ( 𝑆 ∈ ℂ ∧ ( ∗ ‘ 𝑆 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) → ( ∗ ‘ 𝐴 ) = ( 𝑎 + ( 𝑏 · ( ∗ ‘ 𝑆 ) ) ) )
31 zellaz ⊢ ( ( 𝑆 ∈ ℂ ∧ 𝑎 ∈ ℤ ) → 𝑎 ∈ ( Z[]l ‘ 𝑆 ) )
32 31 ad2ant2r ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( ∗ ‘ 𝑆 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑎 ∈ ( Z[]l ‘ 𝑆 ) )
33 32 1 eleqtrrdi ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( ∗ ‘ 𝑆 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑎 ∈ 𝑅 )
34 simpr ⊢ ( ( 𝑆 ∈ ℂ ∧ ( ∗ ‘ 𝑆 ) ∈ 𝑅 ) → ( ∗ ‘ 𝑆 ) ∈ 𝑅 )
35 simpr ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → 𝑏 ∈ ℤ )
36 34 35 anim12ci ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( ∗ ‘ 𝑆 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑏 ∈ ℤ ∧ ( ∗ ‘ 𝑆 ) ∈ 𝑅 ) )
37 1 lazmulzcl ⊢ ( 𝑆 ∈ ℂ → ( ( 𝑏 ∈ ℤ ∧ ( ∗ ‘ 𝑆 ) ∈ 𝑅 ) → ( 𝑏 · ( ∗ ‘ 𝑆 ) ) ∈ 𝑅 ) )
38 20 36 37 sylc ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( ∗ ‘ 𝑆 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑏 · ( ∗ ‘ 𝑆 ) ) ∈ 𝑅 )
39 33 38 jca ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( ∗ ‘ 𝑆 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑎 ∈ 𝑅 ∧ ( 𝑏 · ( ∗ ‘ 𝑆 ) ) ∈ 𝑅 ) )
40 1 lazaddcl ⊢ ( 𝑆 ∈ ℂ → ( ( 𝑎 ∈ 𝑅 ∧ ( 𝑏 · ( ∗ ‘ 𝑆 ) ) ∈ 𝑅 ) → ( 𝑎 + ( 𝑏 · ( ∗ ‘ 𝑆 ) ) ) ∈ 𝑅 ) )
41 20 39 40 sylc ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( ∗ ‘ 𝑆 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑎 + ( 𝑏 · ( ∗ ‘ 𝑆 ) ) ) ∈ 𝑅 )
42 41 adantr ⊢ ( ( ( ( 𝑆 ∈ ℂ ∧ ( ∗ ‘ 𝑆 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) → ( 𝑎 + ( 𝑏 · ( ∗ ‘ 𝑆 ) ) ) ∈ 𝑅 )
43 30 42 eqeltrd ⊢ ( ( ( ( 𝑆 ∈ ℂ ∧ ( ∗ ‘ 𝑆 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) → ( ∗ ‘ 𝐴 ) ∈ 𝑅 )
44 43 ex ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( ∗ ‘ 𝑆 ) ∈ 𝑅 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) → ( ∗ ‘ 𝐴 ) ∈ 𝑅 ) )
45 44 rexlimdvva ⊢ ( ( 𝑆 ∈ ℂ ∧ ( ∗ ‘ 𝑆 ) ∈ 𝑅 ) → ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝐴 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) → ( ∗ ‘ 𝐴 ) ∈ 𝑅 ) )
46 6 45 syld ⊢ ( ( 𝑆 ∈ ℂ ∧ ( ∗ ‘ 𝑆 ) ∈ 𝑅 ) → ( 𝐴 ∈ 𝑅 → ( ∗ ‘ 𝐴 ) ∈ 𝑅 ) )