Theorem idomnnzpownz

Description: A non-zero power in an integral domain is non-zero. (Contributed by metakunt, 5-May-2025)

	Ref	Expression
Hypotheses	idomnnzpownz.1	⊢ ( 𝜑 → 𝑅 ∈ IDomn )
	idomnnzpownz.2	⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ 𝑅 ) )
	idomnnzpownz.3	⊢ ( 𝜑 → 𝐴 ≠ ( 0g ‘ 𝑅 ) )
	idomnnzpownz.4	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	idomnnzpownz.5	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑅 ) )
Assertion	idomnnzpownz	⊢ ( 𝜑 → ( 𝑁 ↑ 𝐴 ) ≠ ( 0g ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		idomnnzpownz.1	⊢ ( 𝜑 → 𝑅 ∈ IDomn )
2		idomnnzpownz.2	⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ 𝑅 ) )
3		idomnnzpownz.3	⊢ ( 𝜑 → 𝐴 ≠ ( 0g ‘ 𝑅 ) )
4		idomnnzpownz.4	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
5		idomnnzpownz.5	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑅 ) )
6	4	ancli	⊢ ( 𝜑 → ( 𝜑 ∧ 𝑁 ∈ ℕ0 ) )
7		oveq1	⊢ ( 𝑥 = 0 → ( 𝑥 ↑ 𝐴 ) = ( 0 ↑ 𝐴 ) )
8	7	neeq1d	⊢ ( 𝑥 = 0 → ( ( 𝑥 ↑ 𝐴 ) ≠ ( 0g ‘ 𝑅 ) ↔ ( 0 ↑ 𝐴 ) ≠ ( 0g ‘ 𝑅 ) ) )
9		oveq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ↑ 𝐴 ) = ( 𝑦 ↑ 𝐴 ) )
10	9	neeq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ↑ 𝐴 ) ≠ ( 0g ‘ 𝑅 ) ↔ ( 𝑦 ↑ 𝐴 ) ≠ ( 0g ‘ 𝑅 ) ) )
11		oveq1	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥 ↑ 𝐴 ) = ( ( 𝑦 + 1 ) ↑ 𝐴 ) )
12	11	neeq1d	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝑥 ↑ 𝐴 ) ≠ ( 0g ‘ 𝑅 ) ↔ ( ( 𝑦 + 1 ) ↑ 𝐴 ) ≠ ( 0g ‘ 𝑅 ) ) )
13		oveq1	⊢ ( 𝑥 = 𝑁 → ( 𝑥 ↑ 𝐴 ) = ( 𝑁 ↑ 𝐴 ) )
14	13	neeq1d	⊢ ( 𝑥 = 𝑁 → ( ( 𝑥 ↑ 𝐴 ) ≠ ( 0g ‘ 𝑅 ) ↔ ( 𝑁 ↑ 𝐴 ) ≠ ( 0g ‘ 𝑅 ) ) )
15		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
16		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
17	15 16	mgpbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
18	2 17	eleqtrdi	⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) )
19		eqid	⊢ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
20		eqid	⊢ ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) )
21	19 20 5	mulg0	⊢ ( 𝐴 ∈ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) → ( 0 ↑ 𝐴 ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) )
22	18 21	syl	⊢ ( 𝜑 → ( 0 ↑ 𝐴 ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) ) )
23		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
24	15 23	ringidval	⊢ ( 1r ‘ 𝑅 ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) )
25	22 24	eqtr4di	⊢ ( 𝜑 → ( 0 ↑ 𝐴 ) = ( 1r ‘ 𝑅 ) )
26		isidom	⊢ ( 𝑅 ∈ IDomn ↔ ( 𝑅 ∈ CRing ∧ 𝑅 ∈ Domn ) )
27	26	simprbi	⊢ ( 𝑅 ∈ IDomn → 𝑅 ∈ Domn )
28		domnnzr	⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ NzRing )
29		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
30	23 29	nzrnz	⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
31	1 27 28 30	4syl	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
32	25 31	eqnetrd	⊢ ( 𝜑 → ( 0 ↑ 𝐴 ) ≠ ( 0g ‘ 𝑅 ) )
33	1	idomringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
34	15	ringmgp	⊢ ( 𝑅 ∈ Ring → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
35	33 34	syl	⊢ ( 𝜑 → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
36	35	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
37	36	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝐴 ) ≠ ( 0g ‘ 𝑅 ) ) → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
38		simplr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝐴 ) ≠ ( 0g ‘ 𝑅 ) ) → 𝑦 ∈ ℕ0 )
39	18	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝐴 ) ≠ ( 0g ‘ 𝑅 ) ) → 𝐴 ∈ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) )
40		eqid	⊢ ( +g ‘ ( mulGrp ‘ 𝑅 ) ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
41	19 5 40	mulgnn0p1	⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ 𝐴 ∈ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) ) → ( ( 𝑦 + 1 ) ↑ 𝐴 ) = ( ( 𝑦 ↑ 𝐴 ) ( +g ‘ ( mulGrp ‘ 𝑅 ) ) 𝐴 ) )
42	37 38 39 41	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝐴 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( 𝑦 + 1 ) ↑ 𝐴 ) = ( ( 𝑦 ↑ 𝐴 ) ( +g ‘ ( mulGrp ‘ 𝑅 ) ) 𝐴 ) )
43		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
44	15 43	mgpplusg	⊢ ( .r ‘ 𝑅 ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
45	44	a1i	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝐴 ) ≠ ( 0g ‘ 𝑅 ) ) → ( .r ‘ 𝑅 ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) ) )
46	45	eqcomd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝐴 ) ≠ ( 0g ‘ 𝑅 ) ) → ( +g ‘ ( mulGrp ‘ 𝑅 ) ) = ( .r ‘ 𝑅 ) )
47	46	oveqd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝐴 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( 𝑦 ↑ 𝐴 ) ( +g ‘ ( mulGrp ‘ 𝑅 ) ) 𝐴 ) = ( ( 𝑦 ↑ 𝐴 ) ( .r ‘ 𝑅 ) 𝐴 ) )
48	1 27	syl	⊢ ( 𝜑 → 𝑅 ∈ Domn )
49	48	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) → 𝑅 ∈ Domn )
50	49	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝐴 ) ≠ ( 0g ‘ 𝑅 ) ) → 𝑅 ∈ Domn )
51	19 5	mulgnn0cl	⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ 𝐴 ∈ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) ) → ( 𝑦 ↑ 𝐴 ) ∈ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) )
52	37 38 39 51	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝐴 ) ≠ ( 0g ‘ 𝑅 ) ) → ( 𝑦 ↑ 𝐴 ) ∈ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) )
53	17	eqcomi	⊢ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) = ( Base ‘ 𝑅 )
54	53	a1i	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝐴 ) ≠ ( 0g ‘ 𝑅 ) ) → ( Base ‘ ( mulGrp ‘ 𝑅 ) ) = ( Base ‘ 𝑅 ) )
55	52 54	eleqtrd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝐴 ) ≠ ( 0g ‘ 𝑅 ) ) → ( 𝑦 ↑ 𝐴 ) ∈ ( Base ‘ 𝑅 ) )
56		simpr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝐴 ) ≠ ( 0g ‘ 𝑅 ) ) → ( 𝑦 ↑ 𝐴 ) ≠ ( 0g ‘ 𝑅 ) )
57	55 56	jca	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝐴 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( 𝑦 ↑ 𝐴 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑦 ↑ 𝐴 ) ≠ ( 0g ‘ 𝑅 ) ) )
58	2 3	jca	⊢ ( 𝜑 → ( 𝐴 ∈ ( Base ‘ 𝑅 ) ∧ 𝐴 ≠ ( 0g ‘ 𝑅 ) ) )
59	58	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) → ( 𝐴 ∈ ( Base ‘ 𝑅 ) ∧ 𝐴 ≠ ( 0g ‘ 𝑅 ) ) )
60	59	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝐴 ) ≠ ( 0g ‘ 𝑅 ) ) → ( 𝐴 ∈ ( Base ‘ 𝑅 ) ∧ 𝐴 ≠ ( 0g ‘ 𝑅 ) ) )
61	16 43 29	domnmuln0	⊢ ( ( 𝑅 ∈ Domn ∧ ( ( 𝑦 ↑ 𝐴 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑦 ↑ 𝐴 ) ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ ( Base ‘ 𝑅 ) ∧ 𝐴 ≠ ( 0g ‘ 𝑅 ) ) ) → ( ( 𝑦 ↑ 𝐴 ) ( .r ‘ 𝑅 ) 𝐴 ) ≠ ( 0g ‘ 𝑅 ) )
62	50 57 60 61	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝐴 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( 𝑦 ↑ 𝐴 ) ( .r ‘ 𝑅 ) 𝐴 ) ≠ ( 0g ‘ 𝑅 ) )
63	47 62	eqnetrd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝐴 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( 𝑦 ↑ 𝐴 ) ( +g ‘ ( mulGrp ‘ 𝑅 ) ) 𝐴 ) ≠ ( 0g ‘ 𝑅 ) )
64	42 63	eqnetrd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝐴 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( 𝑦 + 1 ) ↑ 𝐴 ) ≠ ( 0g ‘ 𝑅 ) )
65	8 10 12 14 32 64	nn0indd	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 ↑ 𝐴 ) ≠ ( 0g ‘ 𝑅 ) )
66	6 65	syl	⊢ ( 𝜑 → ( 𝑁 ↑ 𝐴 ) ≠ ( 0g ‘ 𝑅 ) )