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 ) )