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

Metamath Proof Explorer

Theorem ply1unit

Description: In a field F , a polynomial C is a unit iff it has degree 0. This corresponds to the nonzero scalars, see ply1asclunit . (Contributed by Thierry Arnoux, 25-Apr-2025)

Ref Expression
Hypotheses ply1asclunit.1 ⊢ 𝑃 = ( Poly1 ‘ 𝐹 )
ply1asclunit.2 ⊢ 𝐴 = ( algSc ‘ 𝑃 )
ply1asclunit.3 ⊢ 𝐵 = ( Base ‘ 𝐹 )
ply1asclunit.4 ⊢ 0 = ( 0g ‘ 𝐹 )
ply1asclunit.5 ⊢ ( 𝜑 → 𝐹 ∈ Field )
ply1unit.d ⊢ 𝐷 = ( deg1 ‘ 𝐹 )
ply1unit.f ⊢ ( 𝜑 → 𝐶 ∈ ( Base ‘ 𝑃 ) )
Assertion ply1unit ( 𝜑 → ( 𝐶 ∈ ( Unit ‘ 𝑃 ) ↔ ( 𝐷 ‘ 𝐶 ) = 0 ) )

Proof

Step Hyp Ref Expression
1 ply1asclunit.1 ⊢ 𝑃 = ( Poly1 ‘ 𝐹 )
2 ply1asclunit.2 ⊢ 𝐴 = ( algSc ‘ 𝑃 )
3 ply1asclunit.3 ⊢ 𝐵 = ( Base ‘ 𝐹 )
4 ply1asclunit.4 ⊢ 0 = ( 0g ‘ 𝐹 )
5 ply1asclunit.5 ⊢ ( 𝜑 → 𝐹 ∈ Field )
6 ply1unit.d ⊢ 𝐷 = ( deg1 ‘ 𝐹 )
7 ply1unit.f ⊢ ( 𝜑 → 𝐶 ∈ ( Base ‘ 𝑃 ) )
8 5 fldcrngd ⊢ ( 𝜑 → 𝐹 ∈ CRing )
9 8 crngringd ⊢ ( 𝜑 → 𝐹 ∈ Ring )
10 9 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( Unit ‘ 𝑃 ) ) → 𝐹 ∈ Ring )
11 1 ply1ring ⊢ ( 𝐹 ∈ Ring → 𝑃 ∈ Ring )
12 9 11 syl ⊢ ( 𝜑 → 𝑃 ∈ Ring )
13 eqid ⊢ ( Unit ‘ 𝑃 ) = ( Unit ‘ 𝑃 )
14 eqid ⊢ ( invr ‘ 𝑃 ) = ( invr ‘ 𝑃 )
15 13 14 unitinvcl ⊢ ( ( 𝑃 ∈ Ring ∧ 𝐶 ∈ ( Unit ‘ 𝑃 ) ) → ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ∈ ( Unit ‘ 𝑃 ) )
16 12 15 sylan ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( Unit ‘ 𝑃 ) ) → ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ∈ ( Unit ‘ 𝑃 ) )
17 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
18 17 13 unitcl ⊢ ( ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ∈ ( Unit ‘ 𝑃 ) → ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ∈ ( Base ‘ 𝑃 ) )
19 16 18 syl ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( Unit ‘ 𝑃 ) ) → ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ∈ ( Base ‘ 𝑃 ) )
20 eqid ⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
21 5 flddrngd ⊢ ( 𝜑 → 𝐹 ∈ DivRing )
22 drngnzr ⊢ ( 𝐹 ∈ DivRing → 𝐹 ∈ NzRing )
23 1 ply1nz ⊢ ( 𝐹 ∈ NzRing → 𝑃 ∈ NzRing )
24 21 22 23 3syl ⊢ ( 𝜑 → 𝑃 ∈ NzRing )
25 24 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( Unit ‘ 𝑃 ) ) → 𝑃 ∈ NzRing )
26 13 20 25 16 unitnz ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( Unit ‘ 𝑃 ) ) → ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ≠ ( 0g ‘ 𝑃 ) )
27 6 1 20 17 deg1nn0cl ⊢ ( ( 𝐹 ∈ Ring ∧ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ∈ ( Base ‘ 𝑃 ) ∧ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ≠ ( 0g ‘ 𝑃 ) ) → ( 𝐷 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ) ∈ ℕ0 )
28 10 19 26 27 syl3anc ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( Unit ‘ 𝑃 ) ) → ( 𝐷 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ) ∈ ℕ0 )
29 28 nn0red ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( Unit ‘ 𝑃 ) ) → ( 𝐷 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ) ∈ ℝ )
30 28 nn0ge0d ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( Unit ‘ 𝑃 ) ) → 0 ≤ ( 𝐷 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ) )
31 29 30 jca ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( Unit ‘ 𝑃 ) ) → ( ( 𝐷 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐷 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ) ) )
32 7 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( Unit ‘ 𝑃 ) ) → 𝐶 ∈ ( Base ‘ 𝑃 ) )
33 simpr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( Unit ‘ 𝑃 ) ) → 𝐶 ∈ ( Unit ‘ 𝑃 ) )
34 13 20 25 33 unitnz ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( Unit ‘ 𝑃 ) ) → 𝐶 ≠ ( 0g ‘ 𝑃 ) )
35 6 1 20 17 deg1nn0cl ⊢ ( ( 𝐹 ∈ Ring ∧ 𝐶 ∈ ( Base ‘ 𝑃 ) ∧ 𝐶 ≠ ( 0g ‘ 𝑃 ) ) → ( 𝐷 ‘ 𝐶 ) ∈ ℕ0 )
36 10 32 34 35 syl3anc ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( Unit ‘ 𝑃 ) ) → ( 𝐷 ‘ 𝐶 ) ∈ ℕ0 )
37 36 nn0red ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( Unit ‘ 𝑃 ) ) → ( 𝐷 ‘ 𝐶 ) ∈ ℝ )
38 36 nn0ge0d ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( Unit ‘ 𝑃 ) ) → 0 ≤ ( 𝐷 ‘ 𝐶 ) )
39 eqid ⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
40 eqid ⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 )
41 13 14 39 40 unitlinv ⊢ ( ( 𝑃 ∈ Ring ∧ 𝐶 ∈ ( Unit ‘ 𝑃 ) ) → ( ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) = ( 1r ‘ 𝑃 ) )
42 12 41 sylan ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( Unit ‘ 𝑃 ) ) → ( ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) = ( 1r ‘ 𝑃 ) )
43 42 fveq2d ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( Unit ‘ 𝑃 ) ) → ( 𝐷 ‘ ( ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) = ( 𝐷 ‘ ( 1r ‘ 𝑃 ) ) )
44 eqid ⊢ ( RLReg ‘ 𝐹 ) = ( RLReg ‘ 𝐹 )
45 drngdomn ⊢ ( 𝐹 ∈ DivRing → 𝐹 ∈ Domn )
46 21 45 syl ⊢ ( 𝜑 → 𝐹 ∈ Domn )
47 46 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( Unit ‘ 𝑃 ) ) → 𝐹 ∈ Domn )
48 eqid ⊢ ( coe1 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ) = ( coe1 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) )
49 48 17 1 3 coe1fvalcl ⊢ ( ( ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝐷 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ) ∈ ℕ0 ) → ( ( coe1 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ) ‘ ( 𝐷 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ) ) ∈ 𝐵 )
50 19 28 49 syl2anc ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( Unit ‘ 𝑃 ) ) → ( ( coe1 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ) ‘ ( 𝐷 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ) ) ∈ 𝐵 )
51 6 1 20 17 4 48 deg1ldg ⊢ ( ( 𝐹 ∈ Ring ∧ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ∈ ( Base ‘ 𝑃 ) ∧ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ≠ ( 0g ‘ 𝑃 ) ) → ( ( coe1 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ) ‘ ( 𝐷 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ) ) ≠ 0 )
52 10 19 26 51 syl3anc ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( Unit ‘ 𝑃 ) ) → ( ( coe1 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ) ‘ ( 𝐷 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ) ) ≠ 0 )
53 3 44 4 domnrrg ⊢ ( ( 𝐹 ∈ Domn ∧ ( ( coe1 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ) ‘ ( 𝐷 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ) ) ∈ 𝐵 ∧ ( ( coe1 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ) ‘ ( 𝐷 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ) ) ≠ 0 ) → ( ( coe1 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ) ‘ ( 𝐷 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ) ) ∈ ( RLReg ‘ 𝐹 ) )
54 47 50 52 53 syl3anc ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( Unit ‘ 𝑃 ) ) → ( ( coe1 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ) ‘ ( 𝐷 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ) ) ∈ ( RLReg ‘ 𝐹 ) )
55 6 1 44 17 39 20 10 19 26 54 32 34 deg1mul2 ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( Unit ‘ 𝑃 ) ) → ( 𝐷 ‘ ( ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ( .r ‘ 𝑃 ) 𝐶 ) ) = ( ( 𝐷 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ) + ( 𝐷 ‘ 𝐶 ) ) )
56 eqid ⊢ ( Monic1p ‘ 𝐹 ) = ( Monic1p ‘ 𝐹 )
57 1 40 56 6 mon1pid ⊢ ( 𝐹 ∈ NzRing → ( ( 1r ‘ 𝑃 ) ∈ ( Monic1p ‘ 𝐹 ) ∧ ( 𝐷 ‘ ( 1r ‘ 𝑃 ) ) = 0 ) )
58 57 simprd ⊢ ( 𝐹 ∈ NzRing → ( 𝐷 ‘ ( 1r ‘ 𝑃 ) ) = 0 )
59 21 22 58 3syl ⊢ ( 𝜑 → ( 𝐷 ‘ ( 1r ‘ 𝑃 ) ) = 0 )
60 59 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( Unit ‘ 𝑃 ) ) → ( 𝐷 ‘ ( 1r ‘ 𝑃 ) ) = 0 )
61 43 55 60 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( Unit ‘ 𝑃 ) ) → ( ( 𝐷 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ) + ( 𝐷 ‘ 𝐶 ) ) = 0 )
62 add20 ⊢ ( ( ( ( 𝐷 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐷 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ) ) ∧ ( ( 𝐷 ‘ 𝐶 ) ∈ ℝ ∧ 0 ≤ ( 𝐷 ‘ 𝐶 ) ) ) → ( ( ( 𝐷 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ) + ( 𝐷 ‘ 𝐶 ) ) = 0 ↔ ( ( 𝐷 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ) = 0 ∧ ( 𝐷 ‘ 𝐶 ) = 0 ) ) )
63 62 anassrs ⊢ ( ( ( ( ( 𝐷 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐷 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ) ) ∧ ( 𝐷 ‘ 𝐶 ) ∈ ℝ ) ∧ 0 ≤ ( 𝐷 ‘ 𝐶 ) ) → ( ( ( 𝐷 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ) + ( 𝐷 ‘ 𝐶 ) ) = 0 ↔ ( ( 𝐷 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ) = 0 ∧ ( 𝐷 ‘ 𝐶 ) = 0 ) ) )
64 63 simplbda ⊢ ( ( ( ( ( ( 𝐷 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐷 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ) ) ∧ ( 𝐷 ‘ 𝐶 ) ∈ ℝ ) ∧ 0 ≤ ( 𝐷 ‘ 𝐶 ) ) ∧ ( ( 𝐷 ‘ ( ( invr ‘ 𝑃 ) ‘ 𝐶 ) ) + ( 𝐷 ‘ 𝐶 ) ) = 0 ) → ( 𝐷 ‘ 𝐶 ) = 0 )
65 31 37 38 61 64 syl1111anc ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( Unit ‘ 𝑃 ) ) → ( 𝐷 ‘ 𝐶 ) = 0 )
66 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐶 ) = 0 ) → 𝐹 ∈ Ring )
67 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐶 ) = 0 ) → 𝐶 ∈ ( Base ‘ 𝑃 ) )
68 6 1 17 deg1xrcl ⊢ ( 𝐶 ∈ ( Base ‘ 𝑃 ) → ( 𝐷 ‘ 𝐶 ) ∈ ℝ* )
69 7 68 syl ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐶 ) ∈ ℝ* )
70 0xr ⊢ 0 ∈ ℝ*
71 xeqlelt ⊢ ( ( ( 𝐷 ‘ 𝐶 ) ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( ( 𝐷 ‘ 𝐶 ) = 0 ↔ ( ( 𝐷 ‘ 𝐶 ) ≤ 0 ∧ ¬ ( 𝐷 ‘ 𝐶 ) < 0 ) ) )
72 69 70 71 sylancl ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐶 ) = 0 ↔ ( ( 𝐷 ‘ 𝐶 ) ≤ 0 ∧ ¬ ( 𝐷 ‘ 𝐶 ) < 0 ) ) )
73 72 simprbda ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐶 ) = 0 ) → ( 𝐷 ‘ 𝐶 ) ≤ 0 )
74 6 1 17 2 deg1le0 ⊢ ( ( 𝐹 ∈ Ring ∧ 𝐶 ∈ ( Base ‘ 𝑃 ) ) → ( ( 𝐷 ‘ 𝐶 ) ≤ 0 ↔ 𝐶 = ( 𝐴 ‘ ( ( coe1 ‘ 𝐶 ) ‘ 0 ) ) ) )
75 74 biimpa ⊢ ( ( ( 𝐹 ∈ Ring ∧ 𝐶 ∈ ( Base ‘ 𝑃 ) ) ∧ ( 𝐷 ‘ 𝐶 ) ≤ 0 ) → 𝐶 = ( 𝐴 ‘ ( ( coe1 ‘ 𝐶 ) ‘ 0 ) ) )
76 66 67 73 75 syl21anc ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐶 ) = 0 ) → 𝐶 = ( 𝐴 ‘ ( ( coe1 ‘ 𝐶 ) ‘ 0 ) ) )
77 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐶 ) = 0 ) → 𝐹 ∈ Field )
78 0nn0 ⊢ 0 ∈ ℕ0
79 eqid ⊢ ( coe1 ‘ 𝐶 ) = ( coe1 ‘ 𝐶 )
80 79 17 1 3 coe1fvalcl ⊢ ( ( 𝐶 ∈ ( Base ‘ 𝑃 ) ∧ 0 ∈ ℕ0 ) → ( ( coe1 ‘ 𝐶 ) ‘ 0 ) ∈ 𝐵 )
81 67 78 80 sylancl ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐶 ) = 0 ) → ( ( coe1 ‘ 𝐶 ) ‘ 0 ) ∈ 𝐵 )
82 simpl ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐶 ) = 0 ) → 𝜑 )
83 72 simplbda ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐶 ) = 0 ) → ¬ ( 𝐷 ‘ 𝐶 ) < 0 )
84 6 1 20 17 deg1lt0 ⊢ ( ( 𝐹 ∈ Ring ∧ 𝐶 ∈ ( Base ‘ 𝑃 ) ) → ( ( 𝐷 ‘ 𝐶 ) < 0 ↔ 𝐶 = ( 0g ‘ 𝑃 ) ) )
85 84 necon3bbid ⊢ ( ( 𝐹 ∈ Ring ∧ 𝐶 ∈ ( Base ‘ 𝑃 ) ) → ( ¬ ( 𝐷 ‘ 𝐶 ) < 0 ↔ 𝐶 ≠ ( 0g ‘ 𝑃 ) ) )
86 85 biimpa ⊢ ( ( ( 𝐹 ∈ Ring ∧ 𝐶 ∈ ( Base ‘ 𝑃 ) ) ∧ ¬ ( 𝐷 ‘ 𝐶 ) < 0 ) → 𝐶 ≠ ( 0g ‘ 𝑃 ) )
87 66 67 83 86 syl21anc ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐶 ) = 0 ) → 𝐶 ≠ ( 0g ‘ 𝑃 ) )
88 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐶 ) ≤ 0 ) → 𝐹 ∈ Ring )
89 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐶 ) ≤ 0 ) → 𝐶 ∈ ( Base ‘ 𝑃 ) )
90 simpr ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐶 ) ≤ 0 ) → ( 𝐷 ‘ 𝐶 ) ≤ 0 )
91 6 1 4 17 20 88 89 90 deg1le0eq0 ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐶 ) ≤ 0 ) → ( 𝐶 = ( 0g ‘ 𝑃 ) ↔ ( ( coe1 ‘ 𝐶 ) ‘ 0 ) = 0 ) )
92 91 necon3bid ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐶 ) ≤ 0 ) → ( 𝐶 ≠ ( 0g ‘ 𝑃 ) ↔ ( ( coe1 ‘ 𝐶 ) ‘ 0 ) ≠ 0 ) )
93 92 biimpa ⊢ ( ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐶 ) ≤ 0 ) ∧ 𝐶 ≠ ( 0g ‘ 𝑃 ) ) → ( ( coe1 ‘ 𝐶 ) ‘ 0 ) ≠ 0 )
94 82 73 87 93 syl21anc ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐶 ) = 0 ) → ( ( coe1 ‘ 𝐶 ) ‘ 0 ) ≠ 0 )
95 1 2 3 4 77 81 94 ply1asclunit ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐶 ) = 0 ) → ( 𝐴 ‘ ( ( coe1 ‘ 𝐶 ) ‘ 0 ) ) ∈ ( Unit ‘ 𝑃 ) )
96 76 95 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝐷 ‘ 𝐶 ) = 0 ) → 𝐶 ∈ ( Unit ‘ 𝑃 ) )
97 65 96 impbida ⊢ ( 𝜑 → ( 𝐶 ∈ ( Unit ‘ 𝑃 ) ↔ ( 𝐷 ‘ 𝐶 ) = 0 ) )