primrootscoprbij

Description: A bijection between coprime powers of primitive roots and primitive roots. (Contributed by metakunt, 26-Apr-2025)

	Ref	Expression
Hypotheses	primrootscoprbij.1	$⊢ F = (m \in (R PrimRoots K) ⟼ I \cdot_{R} m)$
	primrootscoprbij.2	$⊢ φ \to R \in CMnd$
	primrootscoprbij.3	$⊢ φ \to K \in ℕ$
	primrootscoprbij.4	$⊢ φ \to I \in ℕ$
	primrootscoprbij.5	$⊢ φ \to J \in ℕ$
	primrootscoprbij.6	$⊢ φ \to Z \in ℤ$
	primrootscoprbij.7	$⊢ φ \to 1 = I \cdot J + K Z$
	primrootscoprbij.8	$⊢ U = \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\}$
Assertion	primrootscoprbij	$⊢ φ \to F : R PrimRoots K \underset{1-1 onto}{⟶} R PrimRoots K$

Proof

Step	Hyp	Ref	Expression
1		primrootscoprbij.1	$⊢ F = (m \in (R PrimRoots K) ⟼ I \cdot_{R} m)$
2		primrootscoprbij.2	$⊢ φ \to R \in CMnd$
3		primrootscoprbij.3	$⊢ φ \to K \in ℕ$
4		primrootscoprbij.4	$⊢ φ \to I \in ℕ$
5		primrootscoprbij.5	$⊢ φ \to J \in ℕ$
6		primrootscoprbij.6	$⊢ φ \to Z \in ℤ$
7		primrootscoprbij.7	$⊢ φ \to 1 = I \cdot J + K Z$
8		primrootscoprbij.8	$⊢ U = \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\}$
9	4	nnzd	$⊢ φ \to I \in ℤ$
10	3	nnzd	$⊢ φ \to K \in ℤ$
11	5	nnzd	$⊢ φ \to J \in ℤ$
12	11 6	jca	$⊢ φ \to (J \in ℤ \land Z \in ℤ)$
13	9 10 12	jca31	$⊢ φ \to ((I \in ℤ \land K \in ℤ) \land (J \in ℤ \land Z \in ℤ))$
14	7	eqcomd	$⊢ φ \to I \cdot J + K Z = 1$
15	13 14	jca	$⊢ φ \to (((I \in ℤ \land K \in ℤ) \land (J \in ℤ \land Z \in ℤ)) \land I \cdot J + K Z = 1)$
16		bezoutr1	$⊢ ((I \in ℤ \land K \in ℤ) \land (J \in ℤ \land Z \in ℤ)) \to (I \cdot J + K Z = 1 \to I \gcd K = 1)$
17	16	imp	$⊢ (((I \in ℤ \land K \in ℤ) \land (J \in ℤ \land Z \in ℤ)) \land I \cdot J + K Z = 1) \to I \gcd K = 1$
18	15 17	syl	$⊢ φ \to I \gcd K = 1$
19	1 2 3 4 18	primrootscoprf	$⊢ φ \to F : R PrimRoots K ⟶ R PrimRoots K$
20		eqid	$⊢ (n \in (R PrimRoots K) ⟼ J \cdot_{R} n) = (n \in (R PrimRoots K) ⟼ J \cdot_{R} n)$
21	11 10	jca	$⊢ φ \to (J \in ℤ \land K \in ℤ)$
22	9 6	jca	$⊢ φ \to (I \in ℤ \land Z \in ℤ)$
23	21 22	jca	$⊢ φ \to ((J \in ℤ \land K \in ℤ) \land (I \in ℤ \land Z \in ℤ))$
24	5	nncnd	$⊢ φ \to J \in ℂ$
25	4	nncnd	$⊢ φ \to I \in ℂ$
26	24 25	mulcomd	$⊢ φ \to J \cdot I = I \cdot J$
27	26	oveq1d	$⊢ φ \to J \cdot I + K Z = I \cdot J + K Z$
28	27 14	eqtrd	$⊢ φ \to J \cdot I + K Z = 1$
29	23 28	jca	$⊢ φ \to (((J \in ℤ \land K \in ℤ) \land (I \in ℤ \land Z \in ℤ)) \land J \cdot I + K Z = 1)$
30		bezoutr1	$⊢ ((J \in ℤ \land K \in ℤ) \land (I \in ℤ \land Z \in ℤ)) \to (J \cdot I + K Z = 1 \to J \gcd K = 1)$
31	30	imp	$⊢ (((J \in ℤ \land K \in ℤ) \land (I \in ℤ \land Z \in ℤ)) \land J \cdot I + K Z = 1) \to J \gcd K = 1$
32	29 31	syl	$⊢ φ \to J \gcd K = 1$
33	20 2 3 5 32	primrootscoprf	$⊢ φ \to (n \in (R PrimRoots K) ⟼ J \cdot_{R} n) : R PrimRoots K ⟶ R PrimRoots K$
34	1	a1i	$⊢ (φ \land x \in (R PrimRoots K)) \to F = (m \in (R PrimRoots K) ⟼ I \cdot_{R} m)$
35		simpr	$⊢ ((φ \land x \in (R PrimRoots K)) \land m = x) \to m = x$
36	35	oveq2d	$⊢ ((φ \land x \in (R PrimRoots K)) \land m = x) \to I \cdot_{R} m = I \cdot_{R} x$
37		simpr	$⊢ (φ \land x \in (R PrimRoots K)) \to x \in (R PrimRoots K)$
38	2	cmnmndd	$⊢ φ \to R \in Mnd$
39	38	adantr	$⊢ (φ \land x \in (R PrimRoots K)) \to R \in Mnd$
40	4	nnnn0d	$⊢ φ \to I \in ℕ_{0}$
41	40	adantr	$⊢ (φ \land x \in (R PrimRoots K)) \to I \in ℕ_{0}$
42	3	nnnn0d	$⊢ φ \to K \in ℕ_{0}$
43		eqid	$⊢ \cdot_{R} = \cdot_{R}$
44	2 42 43	isprimroot	$⊢ φ \to (x \in (R PrimRoots K) \leftrightarrow (x \in {Base}_{R} \land K \cdot_{R} x = 0_{R} \land \forall l \in ℕ_{0} (l \cdot_{R} x = 0_{R} \to K ∥ l)))$
45	44	biimpd	$⊢ φ \to (x \in (R PrimRoots K) \to (x \in {Base}_{R} \land K \cdot_{R} x = 0_{R} \land \forall l \in ℕ_{0} (l \cdot_{R} x = 0_{R} \to K ∥ l)))$
46	45	imp	$⊢ (φ \land x \in (R PrimRoots K)) \to (x \in {Base}_{R} \land K \cdot_{R} x = 0_{R} \land \forall l \in ℕ_{0} (l \cdot_{R} x = 0_{R} \to K ∥ l))$
47	46	simp1d	$⊢ (φ \land x \in (R PrimRoots K)) \to x \in {Base}_{R}$
48		eqid	$⊢ {Base}_{R} = {Base}_{R}$
49	48 43	mulgnn0cl	$⊢ (R \in Mnd \land I \in ℕ_{0} \land x \in {Base}_{R}) \to I \cdot_{R} x \in {Base}_{R}$
50	39 41 47 49	syl3anc	$⊢ (φ \land x \in (R PrimRoots K)) \to I \cdot_{R} x \in {Base}_{R}$
51	34 36 37 50	fvmptd	$⊢ (φ \land x \in (R PrimRoots K)) \to F (x) = I \cdot_{R} x$
52	51	fveq2d	$⊢ (φ \land x \in (R PrimRoots K)) \to (n \in (R PrimRoots K) ⟼ J \cdot_{R} n) (F (x)) = (n \in (R PrimRoots K) ⟼ J \cdot_{R} n) (I \cdot_{R} x)$
53		eqidd	$⊢ (φ \land x \in (R PrimRoots K)) \to (n \in (R PrimRoots K) ⟼ J \cdot_{R} n) = (n \in (R PrimRoots K) ⟼ J \cdot_{R} n)$
54		simpr	$⊢ ((φ \land x \in (R PrimRoots K)) \land n = I \cdot_{R} x) \to n = I \cdot_{R} x$
55	54	oveq2d	$⊢ ((φ \land x \in (R PrimRoots K)) \land n = I \cdot_{R} x) \to J \cdot_{R} n = J \cdot_{R} (I \cdot_{R} x)$
56	2	adantr	$⊢ (φ \land x \in (R PrimRoots K)) \to R \in CMnd$
57	3	adantr	$⊢ (φ \land x \in (R PrimRoots K)) \to K \in ℕ$
58	4	adantr	$⊢ (φ \land x \in (R PrimRoots K)) \to I \in ℕ$
59	18	adantr	$⊢ (φ \land x \in (R PrimRoots K)) \to I \gcd K = 1$
60		eqid	$⊢ \{s \in {Base}_{R} \| \exists t \in {Base}_{R} t +_{R} s = 0_{R}\} = \{s \in {Base}_{R} \| \exists t \in {Base}_{R} t +_{R} s = 0_{R}\}$
61	56 57 58 59 37 60	primrootscoprmpow	$⊢ (φ \land x \in (R PrimRoots K)) \to I \cdot_{R} x \in (R PrimRoots K)$
62	5	nnnn0d	$⊢ φ \to J \in ℕ_{0}$
63	62	adantr	$⊢ (φ \land x \in (R PrimRoots K)) \to J \in ℕ_{0}$
64	48 43	mulgnn0cl	$⊢ (R \in Mnd \land J \in ℕ_{0} \land I \cdot_{R} x \in {Base}_{R}) \to J \cdot_{R} (I \cdot_{R} x) \in {Base}_{R}$
65	39 63 50 64	syl3anc	$⊢ (φ \land x \in (R PrimRoots K)) \to J \cdot_{R} (I \cdot_{R} x) \in {Base}_{R}$
66	53 55 61 65	fvmptd	$⊢ (φ \land x \in (R PrimRoots K)) \to (n \in (R PrimRoots K) ⟼ J \cdot_{R} n) (I \cdot_{R} x) = J \cdot_{R} (I \cdot_{R} x)$
67	63 41 47	3jca	$⊢ (φ \land x \in (R PrimRoots K)) \to (J \in ℕ_{0} \land I \in ℕ_{0} \land x \in {Base}_{R})$
68	48 43	mulgnn0ass	$⊢ (R \in Mnd \land (J \in ℕ_{0} \land I \in ℕ_{0} \land x \in {Base}_{R})) \to J \cdot I \cdot_{R} x = J \cdot_{R} (I \cdot_{R} x)$
69	39 67 68	syl2anc	$⊢ (φ \land x \in (R PrimRoots K)) \to J \cdot I \cdot_{R} x = J \cdot_{R} (I \cdot_{R} x)$
70	2 3 8	primrootsunit	$⊢ φ \to (R PrimRoots K = (R ↾_{𝑠} U) PrimRoots K \land R ↾_{𝑠} U \in Abel)$
71	70	simpld	$⊢ φ \to R PrimRoots K = (R ↾_{𝑠} U) PrimRoots K$
72	71	eleq2d	$⊢ φ \to (x \in (R PrimRoots K) \leftrightarrow x \in ((R ↾_{𝑠} U) PrimRoots K))$
73	72	biimpd	$⊢ φ \to (x \in (R PrimRoots K) \to x \in ((R ↾_{𝑠} U) PrimRoots K))$
74	70	simprd	$⊢ φ \to R ↾_{𝑠} U \in Abel$
75		ablgrp	$⊢ R ↾_{𝑠} U \in Abel \to R ↾_{𝑠} U \in Grp$
76	74 75	syl	$⊢ φ \to R ↾_{𝑠} U \in Grp$
77		grpmnd	$⊢ R ↾_{𝑠} U \in Grp \to R ↾_{𝑠} U \in Mnd$
78	76 77	syl	$⊢ φ \to R ↾_{𝑠} U \in Mnd$
79	38 78	jca	$⊢ φ \to (R \in Mnd \land R ↾_{𝑠} U \in Mnd)$
80	8	a1i	$⊢ φ \to U = \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\}$
81	80	eleq2d	$⊢ φ \to (f \in U \leftrightarrow f \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\})$
82	81	biimpd	$⊢ φ \to (f \in U \to f \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\})$
83	82	imp	$⊢ (φ \land f \in U) \to f \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\}$
84		oveq2	$⊢ a = f \to i +_{R} a = i +_{R} f$
85	84	eqeq1d	$⊢ a = f \to (i +_{R} a = 0_{R} \leftrightarrow i +_{R} f = 0_{R})$
86	85	rexbidv	$⊢ a = f \to (\exists i \in {Base}_{R} i +_{R} a = 0_{R} \leftrightarrow \exists i \in {Base}_{R} i +_{R} f = 0_{R})$
87	86	elrab	$⊢ f \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\} \leftrightarrow (f \in {Base}_{R} \land \exists i \in {Base}_{R} i +_{R} f = 0_{R})$
88	87	biimpi	$⊢ f \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\} \to (f \in {Base}_{R} \land \exists i \in {Base}_{R} i +_{R} f = 0_{R})$
89	88	simpld	$⊢ f \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\} \to f \in {Base}_{R}$
90	83 89	syl	$⊢ (φ \land f \in U) \to f \in {Base}_{R}$
91	90	ex	$⊢ φ \to (f \in U \to f \in {Base}_{R})$
92	91	ssrdv	$⊢ φ \to U \subseteq {Base}_{R}$
93		oveq2	$⊢ a = 0_{R} \to i +_{R} a = i +_{R} 0_{R}$
94	93	eqeq1d	$⊢ a = 0_{R} \to (i +_{R} a = 0_{R} \leftrightarrow i +_{R} 0_{R} = 0_{R})$
95	94	rexbidv	$⊢ a = 0_{R} \to (\exists i \in {Base}_{R} i +_{R} a = 0_{R} \leftrightarrow \exists i \in {Base}_{R} i +_{R} 0_{R} = 0_{R})$
96		eqid	$⊢ 0_{R} = 0_{R}$
97	48 96	mndidcl	$⊢ R \in Mnd \to 0_{R} \in {Base}_{R}$
98	38 97	syl	$⊢ φ \to 0_{R} \in {Base}_{R}$
99		simpr	$⊢ (φ \land i = 0_{R}) \to i = 0_{R}$
100	99	oveq1d	$⊢ (φ \land i = 0_{R}) \to i +_{R} 0_{R} = 0_{R} +_{R} 0_{R}$
101	100	eqeq1d	$⊢ (φ \land i = 0_{R}) \to (i +_{R} 0_{R} = 0_{R} \leftrightarrow 0_{R} +_{R} 0_{R} = 0_{R})$
102		eqid	$⊢ +_{R} = +_{R}$
103	48 102 96	mndlid	$⊢ (R \in Mnd \land 0_{R} \in {Base}_{R}) \to 0_{R} +_{R} 0_{R} = 0_{R}$
104	38 98 103	syl2anc	$⊢ φ \to 0_{R} +_{R} 0_{R} = 0_{R}$
105	98 101 104	rspcedvd	$⊢ φ \to \exists i \in {Base}_{R} i +_{R} 0_{R} = 0_{R}$
106	95 98 105	elrabd	$⊢ φ \to 0_{R} \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\}$
107	80	eleq2d	$⊢ φ \to (0_{R} \in U \leftrightarrow 0_{R} \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\})$
108	106 107	mpbird	$⊢ φ \to 0_{R} \in U$
109	92 108	jca	$⊢ φ \to (U \subseteq {Base}_{R} \land 0_{R} \in U)$
110	79 109	jca	$⊢ φ \to ((R \in Mnd \land R ↾_{𝑠} U \in Mnd) \land (U \subseteq {Base}_{R} \land 0_{R} \in U))$
111	48 96	issubmndb	$⊢ U \in SubMnd (R) \leftrightarrow ((R \in Mnd \land R ↾_{𝑠} U \in Mnd) \land (U \subseteq {Base}_{R} \land 0_{R} \in U))$
112	110 111	sylibr	$⊢ φ \to U \in SubMnd (R)$
113	112	adantr	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to U \in SubMnd (R)$
114	62	adantr	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to J \in ℕ_{0}$
115	40	adantr	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to I \in ℕ_{0}$
116	114 115	nn0mulcld	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to J \cdot I \in ℕ_{0}$
117	74	ablcmnd	$⊢ φ \to R ↾_{𝑠} U \in CMnd$
118		eqid	$⊢ \cdot_{(R ↾_{𝑠} U)} = \cdot_{(R ↾_{𝑠} U)}$
119	117 42 118	isprimroot	$⊢ φ \to (x \in ((R ↾_{𝑠} U) PrimRoots K) \leftrightarrow (x \in {Base}_{(R ↾_{𝑠} U)} \land K \cdot_{(R ↾_{𝑠} U)} x = 0_{(R ↾_{𝑠} U)} \land \forall l \in ℕ_{0} (l \cdot_{(R ↾_{𝑠} U)} x = 0_{(R ↾_{𝑠} U)} \to K ∥ l)))$
120	119	biimpd	$⊢ φ \to (x \in ((R ↾_{𝑠} U) PrimRoots K) \to (x \in {Base}_{(R ↾_{𝑠} U)} \land K \cdot_{(R ↾_{𝑠} U)} x = 0_{(R ↾_{𝑠} U)} \land \forall l \in ℕ_{0} (l \cdot_{(R ↾_{𝑠} U)} x = 0_{(R ↾_{𝑠} U)} \to K ∥ l)))$
121	120	imp	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to (x \in {Base}_{(R ↾_{𝑠} U)} \land K \cdot_{(R ↾_{𝑠} U)} x = 0_{(R ↾_{𝑠} U)} \land \forall l \in ℕ_{0} (l \cdot_{(R ↾_{𝑠} U)} x = 0_{(R ↾_{𝑠} U)} \to K ∥ l))$
122	121	simp1d	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to x \in {Base}_{(R ↾_{𝑠} U)}$
123		eqid	$⊢ R ↾_{𝑠} U = R ↾_{𝑠} U$
124	123 48	ressbas2	$⊢ U \subseteq {Base}_{R} \to U = {Base}_{(R ↾_{𝑠} U)}$
125	92 124	syl	$⊢ φ \to U = {Base}_{(R ↾_{𝑠} U)}$
126	125	adantr	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to U = {Base}_{(R ↾_{𝑠} U)}$
127	126	eleq2d	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to (x \in U \leftrightarrow x \in {Base}_{(R ↾_{𝑠} U)})$
128	122 127	mpbird	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to x \in U$
129	43 123 118	submmulg	$⊢ (U \in SubMnd (R) \land J \cdot I \in ℕ_{0} \land x \in U) \to J \cdot I \cdot_{R} x = J \cdot I \cdot_{(R ↾_{𝑠} U)} x$
130	113 116 128 129	syl3anc	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to J \cdot I \cdot_{R} x = J \cdot I \cdot_{(R ↾_{𝑠} U)} x$
131	26	adantr	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to J \cdot I = I \cdot J$
132	25 24	mulcld	$⊢ φ \to I \cdot J \in ℂ$
133	3	nncnd	$⊢ φ \to K \in ℂ$
134	6	zcnd	$⊢ φ \to Z \in ℂ$
135	133 134	mulcld	$⊢ φ \to K Z \in ℂ$
136		1cnd	$⊢ φ \to 1 \in ℂ$
137	132 135 136	addlsub	$⊢ φ \to (I \cdot J + K Z = 1 \leftrightarrow I \cdot J = 1 - K Z)$
138	14 137	mpbid	$⊢ φ \to I \cdot J = 1 - K Z$
139	133 134	mulcomd	$⊢ φ \to K Z = Z K$
140	139	oveq2d	$⊢ φ \to 1 - K Z = 1 - Z K$
141	138 140	eqtrd	$⊢ φ \to I \cdot J = 1 - Z K$
142	139 135	eqeltrrd	$⊢ φ \to Z K \in ℂ$
143	136 142	negsubd	$⊢ φ \to 1 + (- Z K) = 1 - Z K$
144	143	eqcomd	$⊢ φ \to 1 - Z K = 1 + (- Z K)$
145	141 144	eqtrd	$⊢ φ \to I \cdot J = 1 + (- Z K)$
146	145	adantr	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to I \cdot J = 1 + (- Z K)$
147	131 146	eqtrd	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to J \cdot I = 1 + (- Z K)$
148	147	oveq1d	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to J \cdot I \cdot_{(R ↾_{𝑠} U)} x = (1 + (- Z K)) \cdot_{(R ↾_{𝑠} U)} x$
149	76	adantr	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to R ↾_{𝑠} U \in Grp$
150		1zzd	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to 1 \in ℤ$
151	6	adantr	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to Z \in ℤ$
152	10	adantr	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to K \in ℤ$
153	151 152	zmulcld	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to Z K \in ℤ$
154	153	znegcld	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to - Z K \in ℤ$
155	150 154 122	3jca	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to (1 \in ℤ \land - Z K \in ℤ \land x \in {Base}_{(R ↾_{𝑠} U)})$
156		eqid	$⊢ {Base}_{(R ↾_{𝑠} U)} = {Base}_{(R ↾_{𝑠} U)}$
157		eqid	$⊢ +_{(R ↾_{𝑠} U)} = +_{(R ↾_{𝑠} U)}$
158	156 118 157	mulgdir	$⊢ (R ↾_{𝑠} U \in Grp \land (1 \in ℤ \land - Z K \in ℤ \land x \in {Base}_{(R ↾_{𝑠} U)})) \to (1 + (- Z K)) \cdot_{(R ↾_{𝑠} U)} x = (1 \cdot_{(R ↾_{𝑠} U)} x) +_{(R ↾_{𝑠} U)} ((- Z K) \cdot_{(R ↾_{𝑠} U)} x)$
159	149 155 158	syl2anc	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to (1 + (- Z K)) \cdot_{(R ↾_{𝑠} U)} x = (1 \cdot_{(R ↾_{𝑠} U)} x) +_{(R ↾_{𝑠} U)} ((- Z K) \cdot_{(R ↾_{𝑠} U)} x)$
160	156 118	mulg1	$⊢ x \in {Base}_{(R ↾_{𝑠} U)} \to 1 \cdot_{(R ↾_{𝑠} U)} x = x$
161	122 160	syl	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to 1 \cdot_{(R ↾_{𝑠} U)} x = x$
162		eqid	$⊢ {inv}_{g} (R ↾_{𝑠} U) = {inv}_{g} (R ↾_{𝑠} U)$
163	156 118 162	mulgneg	$⊢ (R ↾_{𝑠} U \in Grp \land Z K \in ℤ \land x \in {Base}_{(R ↾_{𝑠} U)}) \to (- Z K) \cdot_{(R ↾_{𝑠} U)} x = {inv}_{g} (R ↾_{𝑠} U) (Z K \cdot_{(R ↾_{𝑠} U)} x)$
164	149 153 122 163	syl3anc	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to (- Z K) \cdot_{(R ↾_{𝑠} U)} x = {inv}_{g} (R ↾_{𝑠} U) (Z K \cdot_{(R ↾_{𝑠} U)} x)$
165	161 164	oveq12d	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to (1 \cdot_{(R ↾_{𝑠} U)} x) +_{(R ↾_{𝑠} U)} ((- Z K) \cdot_{(R ↾_{𝑠} U)} x) = x +_{(R ↾_{𝑠} U)} {inv}_{g} (R ↾_{𝑠} U) (Z K \cdot_{(R ↾_{𝑠} U)} x)$
166	151 152 122	3jca	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to (Z \in ℤ \land K \in ℤ \land x \in {Base}_{(R ↾_{𝑠} U)})$
167	156 118	mulgass	$⊢ (R ↾_{𝑠} U \in Grp \land (Z \in ℤ \land K \in ℤ \land x \in {Base}_{(R ↾_{𝑠} U)})) \to Z K \cdot_{(R ↾_{𝑠} U)} x = Z \cdot_{(R ↾_{𝑠} U)} (K \cdot_{(R ↾_{𝑠} U)} x)$
168	149 166 167	syl2anc	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to Z K \cdot_{(R ↾_{𝑠} U)} x = Z \cdot_{(R ↾_{𝑠} U)} (K \cdot_{(R ↾_{𝑠} U)} x)$
169	121	simp2d	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to K \cdot_{(R ↾_{𝑠} U)} x = 0_{(R ↾_{𝑠} U)}$
170	169	oveq2d	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to Z \cdot_{(R ↾_{𝑠} U)} (K \cdot_{(R ↾_{𝑠} U)} x) = Z \cdot_{(R ↾_{𝑠} U)} 0_{(R ↾_{𝑠} U)}$
171		eqid	$⊢ 0_{(R ↾_{𝑠} U)} = 0_{(R ↾_{𝑠} U)}$
172	156 118 171	mulgz	$⊢ (R ↾_{𝑠} U \in Grp \land Z \in ℤ) \to Z \cdot_{(R ↾_{𝑠} U)} 0_{(R ↾_{𝑠} U)} = 0_{(R ↾_{𝑠} U)}$
173	149 151 172	syl2anc	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to Z \cdot_{(R ↾_{𝑠} U)} 0_{(R ↾_{𝑠} U)} = 0_{(R ↾_{𝑠} U)}$
174	170 173	eqtrd	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to Z \cdot_{(R ↾_{𝑠} U)} (K \cdot_{(R ↾_{𝑠} U)} x) = 0_{(R ↾_{𝑠} U)}$
175	168 174	eqtrd	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to Z K \cdot_{(R ↾_{𝑠} U)} x = 0_{(R ↾_{𝑠} U)}$
176	175	fveq2d	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to {inv}_{g} (R ↾_{𝑠} U) (Z K \cdot_{(R ↾_{𝑠} U)} x) = {inv}_{g} (R ↾_{𝑠} U) (0_{(R ↾_{𝑠} U)})$
177	171 162	grpinvid	$⊢ R ↾_{𝑠} U \in Grp \to {inv}_{g} (R ↾_{𝑠} U) (0_{(R ↾_{𝑠} U)}) = 0_{(R ↾_{𝑠} U)}$
178	76 177	syl	$⊢ φ \to {inv}_{g} (R ↾_{𝑠} U) (0_{(R ↾_{𝑠} U)}) = 0_{(R ↾_{𝑠} U)}$
179	178	adantr	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to {inv}_{g} (R ↾_{𝑠} U) (0_{(R ↾_{𝑠} U)}) = 0_{(R ↾_{𝑠} U)}$
180	176 179	eqtrd	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to {inv}_{g} (R ↾_{𝑠} U) (Z K \cdot_{(R ↾_{𝑠} U)} x) = 0_{(R ↾_{𝑠} U)}$
181	180	oveq2d	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to x +_{(R ↾_{𝑠} U)} {inv}_{g} (R ↾_{𝑠} U) (Z K \cdot_{(R ↾_{𝑠} U)} x) = x +_{(R ↾_{𝑠} U)} 0_{(R ↾_{𝑠} U)}$
182	149 77	syl	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to R ↾_{𝑠} U \in Mnd$
183	156 157 171	mndrid	$⊢ (R ↾_{𝑠} U \in Mnd \land x \in {Base}_{(R ↾_{𝑠} U)}) \to x +_{(R ↾_{𝑠} U)} 0_{(R ↾_{𝑠} U)} = x$
184	182 122 183	syl2anc	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to x +_{(R ↾_{𝑠} U)} 0_{(R ↾_{𝑠} U)} = x$
185	181 184	eqtrd	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to x +_{(R ↾_{𝑠} U)} {inv}_{g} (R ↾_{𝑠} U) (Z K \cdot_{(R ↾_{𝑠} U)} x) = x$
186	165 185	eqtrd	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to (1 \cdot_{(R ↾_{𝑠} U)} x) +_{(R ↾_{𝑠} U)} ((- Z K) \cdot_{(R ↾_{𝑠} U)} x) = x$
187	159 186	eqtrd	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to (1 + (- Z K)) \cdot_{(R ↾_{𝑠} U)} x = x$
188	148 187	eqtrd	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to J \cdot I \cdot_{(R ↾_{𝑠} U)} x = x$
189	130 188	eqtrd	$⊢ (φ \land x \in ((R ↾_{𝑠} U) PrimRoots K)) \to J \cdot I \cdot_{R} x = x$
190	189	ex	$⊢ φ \to (x \in ((R ↾_{𝑠} U) PrimRoots K) \to J \cdot I \cdot_{R} x = x)$
191	190	imim2d	$⊢ φ \to ((x \in (R PrimRoots K) \to x \in ((R ↾_{𝑠} U) PrimRoots K)) \to (x \in (R PrimRoots K) \to J \cdot I \cdot_{R} x = x))$
192	73 191	mpd	$⊢ φ \to (x \in (R PrimRoots K) \to J \cdot I \cdot_{R} x = x)$
193	192	imp	$⊢ (φ \land x \in (R PrimRoots K)) \to J \cdot I \cdot_{R} x = x$
194	69 193	eqtr3d	$⊢ (φ \land x \in (R PrimRoots K)) \to J \cdot_{R} (I \cdot_{R} x) = x$
195	66 194	eqtrd	$⊢ (φ \land x \in (R PrimRoots K)) \to (n \in (R PrimRoots K) ⟼ J \cdot_{R} n) (I \cdot_{R} x) = x$
196	52 195	eqtrd	$⊢ (φ \land x \in (R PrimRoots K)) \to (n \in (R PrimRoots K) ⟼ J \cdot_{R} n) (F (x)) = x$
197	196	ralrimiva	$⊢ φ \to \forall x \in (R PrimRoots K) (n \in (R PrimRoots K) ⟼ J \cdot_{R} n) (F (x)) = x$
198		eqidd	$⊢ (φ \land y \in (R PrimRoots K)) \to (n \in (R PrimRoots K) ⟼ J \cdot_{R} n) = (n \in (R PrimRoots K) ⟼ J \cdot_{R} n)$
199		simpr	$⊢ ((φ \land y \in (R PrimRoots K)) \land n = y) \to n = y$
200	199	oveq2d	$⊢ ((φ \land y \in (R PrimRoots K)) \land n = y) \to J \cdot_{R} n = J \cdot_{R} y$
201		simpr	$⊢ (φ \land y \in (R PrimRoots K)) \to y \in (R PrimRoots K)$
202	38	adantr	$⊢ (φ \land y \in (R PrimRoots K)) \to R \in Mnd$
203	62	adantr	$⊢ (φ \land y \in (R PrimRoots K)) \to J \in ℕ_{0}$
204	2 42 43	isprimroot	$⊢ φ \to (y \in (R PrimRoots K) \leftrightarrow (y \in {Base}_{R} \land K \cdot_{R} y = 0_{R} \land \forall l \in ℕ_{0} (l \cdot_{R} y = 0_{R} \to K ∥ l)))$
205	204	biimpd	$⊢ φ \to (y \in (R PrimRoots K) \to (y \in {Base}_{R} \land K \cdot_{R} y = 0_{R} \land \forall l \in ℕ_{0} (l \cdot_{R} y = 0_{R} \to K ∥ l)))$
206	205	imp	$⊢ (φ \land y \in (R PrimRoots K)) \to (y \in {Base}_{R} \land K \cdot_{R} y = 0_{R} \land \forall l \in ℕ_{0} (l \cdot_{R} y = 0_{R} \to K ∥ l))$
207	206	simp1d	$⊢ (φ \land y \in (R PrimRoots K)) \to y \in {Base}_{R}$
208	48 43	mulgnn0cl	$⊢ (R \in Mnd \land J \in ℕ_{0} \land y \in {Base}_{R}) \to J \cdot_{R} y \in {Base}_{R}$
209	202 203 207 208	syl3anc	$⊢ (φ \land y \in (R PrimRoots K)) \to J \cdot_{R} y \in {Base}_{R}$
210	198 200 201 209	fvmptd	$⊢ (φ \land y \in (R PrimRoots K)) \to (n \in (R PrimRoots K) ⟼ J \cdot_{R} n) (y) = J \cdot_{R} y$
211	210	fveq2d	$⊢ (φ \land y \in (R PrimRoots K)) \to F ((n \in (R PrimRoots K) ⟼ J \cdot_{R} n) (y)) = F (J \cdot_{R} y)$
212	1	a1i	$⊢ (φ \land y \in (R PrimRoots K)) \to F = (m \in (R PrimRoots K) ⟼ I \cdot_{R} m)$
213		simpr	$⊢ ((φ \land y \in (R PrimRoots K)) \land m = J \cdot_{R} y) \to m = J \cdot_{R} y$
214	213	oveq2d	$⊢ ((φ \land y \in (R PrimRoots K)) \land m = J \cdot_{R} y) \to I \cdot_{R} m = I \cdot_{R} (J \cdot_{R} y)$
215	2	adantr	$⊢ (φ \land y \in (R PrimRoots K)) \to R \in CMnd$
216	3	adantr	$⊢ (φ \land y \in (R PrimRoots K)) \to K \in ℕ$
217	5	adantr	$⊢ (φ \land y \in (R PrimRoots K)) \to J \in ℕ$
218	32	adantr	$⊢ (φ \land y \in (R PrimRoots K)) \to J \gcd K = 1$
219	215 216 217 218 201 60	primrootscoprmpow	$⊢ (φ \land y \in (R PrimRoots K)) \to J \cdot_{R} y \in (R PrimRoots K)$
220	40	adantr	$⊢ (φ \land y \in (R PrimRoots K)) \to I \in ℕ_{0}$
221	48 43	mulgnn0cl	$⊢ (R \in Mnd \land I \in ℕ_{0} \land J \cdot_{R} y \in {Base}_{R}) \to I \cdot_{R} (J \cdot_{R} y) \in {Base}_{R}$
222	202 220 209 221	syl3anc	$⊢ (φ \land y \in (R PrimRoots K)) \to I \cdot_{R} (J \cdot_{R} y) \in {Base}_{R}$
223	212 214 219 222	fvmptd	$⊢ (φ \land y \in (R PrimRoots K)) \to F (J \cdot_{R} y) = I \cdot_{R} (J \cdot_{R} y)$
224	220 203 207	3jca	$⊢ (φ \land y \in (R PrimRoots K)) \to (I \in ℕ_{0} \land J \in ℕ_{0} \land y \in {Base}_{R})$
225	48 43	mulgnn0ass	$⊢ (R \in Mnd \land (I \in ℕ_{0} \land J \in ℕ_{0} \land y \in {Base}_{R})) \to I \cdot J \cdot_{R} y = I \cdot_{R} (J \cdot_{R} y)$
226	202 224 225	syl2anc	$⊢ (φ \land y \in (R PrimRoots K)) \to I \cdot J \cdot_{R} y = I \cdot_{R} (J \cdot_{R} y)$
227	112	adantr	$⊢ (φ \land y \in (R PrimRoots K)) \to U \in SubMnd (R)$
228	220 203	nn0mulcld	$⊢ (φ \land y \in (R PrimRoots K)) \to I \cdot J \in ℕ_{0}$
229	128	ex	$⊢ φ \to (x \in ((R ↾_{𝑠} U) PrimRoots K) \to x \in U)$
230	229	ssrdv	$⊢ φ \to (R ↾_{𝑠} U) PrimRoots K \subseteq U$
231	71	sseq1d	$⊢ φ \to (R PrimRoots K \subseteq U \leftrightarrow (R ↾_{𝑠} U) PrimRoots K \subseteq U)$
232	230 231	mpbird	$⊢ φ \to R PrimRoots K \subseteq U$
233	232	sseld	$⊢ φ \to (y \in (R PrimRoots K) \to y \in U)$
234	233	imp	$⊢ (φ \land y \in (R PrimRoots K)) \to y \in U$
235	43 123 118	submmulg	$⊢ (U \in SubMnd (R) \land I \cdot J \in ℕ_{0} \land y \in U) \to I \cdot J \cdot_{R} y = I \cdot J \cdot_{(R ↾_{𝑠} U)} y$
236	227 228 234 235	syl3anc	$⊢ (φ \land y \in (R PrimRoots K)) \to I \cdot J \cdot_{R} y = I \cdot J \cdot_{(R ↾_{𝑠} U)} y$
237	145	adantr	$⊢ (φ \land y \in (R PrimRoots K)) \to I \cdot J = 1 + (- Z K)$
238	237	oveq1d	$⊢ (φ \land y \in (R PrimRoots K)) \to I \cdot J \cdot_{(R ↾_{𝑠} U)} y = (1 + (- Z K)) \cdot_{(R ↾_{𝑠} U)} y$
239	76	adantr	$⊢ (φ \land y \in (R PrimRoots K)) \to R ↾_{𝑠} U \in Grp$
240		1zzd	$⊢ (φ \land y \in (R PrimRoots K)) \to 1 \in ℤ$
241	6	adantr	$⊢ (φ \land y \in (R PrimRoots K)) \to Z \in ℤ$
242	10	adantr	$⊢ (φ \land y \in (R PrimRoots K)) \to K \in ℤ$
243	241 242	zmulcld	$⊢ (φ \land y \in (R PrimRoots K)) \to Z K \in ℤ$
244	243	znegcld	$⊢ (φ \land y \in (R PrimRoots K)) \to - Z K \in ℤ$
245	232 125	sseqtrd	$⊢ φ \to R PrimRoots K \subseteq {Base}_{(R ↾_{𝑠} U)}$
246	245	sseld	$⊢ φ \to (y \in (R PrimRoots K) \to y \in {Base}_{(R ↾_{𝑠} U)})$
247	246	imp	$⊢ (φ \land y \in (R PrimRoots K)) \to y \in {Base}_{(R ↾_{𝑠} U)}$
248	240 244 247	3jca	$⊢ (φ \land y \in (R PrimRoots K)) \to (1 \in ℤ \land - Z K \in ℤ \land y \in {Base}_{(R ↾_{𝑠} U)})$
249	156 118 157	mulgdir	$⊢ (R ↾_{𝑠} U \in Grp \land (1 \in ℤ \land - Z K \in ℤ \land y \in {Base}_{(R ↾_{𝑠} U)})) \to (1 + (- Z K)) \cdot_{(R ↾_{𝑠} U)} y = (1 \cdot_{(R ↾_{𝑠} U)} y) +_{(R ↾_{𝑠} U)} ((- Z K) \cdot_{(R ↾_{𝑠} U)} y)$
250	239 248 249	syl2anc	$⊢ (φ \land y \in (R PrimRoots K)) \to (1 + (- Z K)) \cdot_{(R ↾_{𝑠} U)} y = (1 \cdot_{(R ↾_{𝑠} U)} y) +_{(R ↾_{𝑠} U)} ((- Z K) \cdot_{(R ↾_{𝑠} U)} y)$
251	156 118	mulg1	$⊢ y \in {Base}_{(R ↾_{𝑠} U)} \to 1 \cdot_{(R ↾_{𝑠} U)} y = y$
252	247 251	syl	$⊢ (φ \land y \in (R PrimRoots K)) \to 1 \cdot_{(R ↾_{𝑠} U)} y = y$
253	156 118 162	mulgneg	$⊢ (R ↾_{𝑠} U \in Grp \land Z K \in ℤ \land y \in {Base}_{(R ↾_{𝑠} U)}) \to (- Z K) \cdot_{(R ↾_{𝑠} U)} y = {inv}_{g} (R ↾_{𝑠} U) (Z K \cdot_{(R ↾_{𝑠} U)} y)$
254	239 243 247 253	syl3anc	$⊢ (φ \land y \in (R PrimRoots K)) \to (- Z K) \cdot_{(R ↾_{𝑠} U)} y = {inv}_{g} (R ↾_{𝑠} U) (Z K \cdot_{(R ↾_{𝑠} U)} y)$
255	241 242 247	3jca	$⊢ (φ \land y \in (R PrimRoots K)) \to (Z \in ℤ \land K \in ℤ \land y \in {Base}_{(R ↾_{𝑠} U)})$
256	156 118	mulgass	$⊢ (R ↾_{𝑠} U \in Grp \land (Z \in ℤ \land K \in ℤ \land y \in {Base}_{(R ↾_{𝑠} U)})) \to Z K \cdot_{(R ↾_{𝑠} U)} y = Z \cdot_{(R ↾_{𝑠} U)} (K \cdot_{(R ↾_{𝑠} U)} y)$
257	239 255 256	syl2anc	$⊢ (φ \land y \in (R PrimRoots K)) \to Z K \cdot_{(R ↾_{𝑠} U)} y = Z \cdot_{(R ↾_{𝑠} U)} (K \cdot_{(R ↾_{𝑠} U)} y)$
258	117 42 118	isprimroot	$⊢ φ \to (y \in ((R ↾_{𝑠} U) PrimRoots K) \leftrightarrow (y \in {Base}_{(R ↾_{𝑠} U)} \land K \cdot_{(R ↾_{𝑠} U)} y = 0_{(R ↾_{𝑠} U)} \land \forall l \in ℕ_{0} (l \cdot_{(R ↾_{𝑠} U)} y = 0_{(R ↾_{𝑠} U)} \to K ∥ l)))$
259	258	biimpd	$⊢ φ \to (y \in ((R ↾_{𝑠} U) PrimRoots K) \to (y \in {Base}_{(R ↾_{𝑠} U)} \land K \cdot_{(R ↾_{𝑠} U)} y = 0_{(R ↾_{𝑠} U)} \land \forall l \in ℕ_{0} (l \cdot_{(R ↾_{𝑠} U)} y = 0_{(R ↾_{𝑠} U)} \to K ∥ l)))$
260	259	imp	$⊢ (φ \land y \in ((R ↾_{𝑠} U) PrimRoots K)) \to (y \in {Base}_{(R ↾_{𝑠} U)} \land K \cdot_{(R ↾_{𝑠} U)} y = 0_{(R ↾_{𝑠} U)} \land \forall l \in ℕ_{0} (l \cdot_{(R ↾_{𝑠} U)} y = 0_{(R ↾_{𝑠} U)} \to K ∥ l))$
261	260	simp2d	$⊢ (φ \land y \in ((R ↾_{𝑠} U) PrimRoots K)) \to K \cdot_{(R ↾_{𝑠} U)} y = 0_{(R ↾_{𝑠} U)}$
262	261	ex	$⊢ φ \to (y \in ((R ↾_{𝑠} U) PrimRoots K) \to K \cdot_{(R ↾_{𝑠} U)} y = 0_{(R ↾_{𝑠} U)})$
263	71	eleq2d	$⊢ φ \to (y \in (R PrimRoots K) \leftrightarrow y \in ((R ↾_{𝑠} U) PrimRoots K))$
264	263	imbi1d	$⊢ φ \to ((y \in (R PrimRoots K) \to K \cdot_{(R ↾_{𝑠} U)} y = 0_{(R ↾_{𝑠} U)}) \leftrightarrow (y \in ((R ↾_{𝑠} U) PrimRoots K) \to K \cdot_{(R ↾_{𝑠} U)} y = 0_{(R ↾_{𝑠} U)}))$
265	262 264	mpbird	$⊢ φ \to (y \in (R PrimRoots K) \to K \cdot_{(R ↾_{𝑠} U)} y = 0_{(R ↾_{𝑠} U)})$
266	265	imp	$⊢ (φ \land y \in (R PrimRoots K)) \to K \cdot_{(R ↾_{𝑠} U)} y = 0_{(R ↾_{𝑠} U)}$
267	266	oveq2d	$⊢ (φ \land y \in (R PrimRoots K)) \to Z \cdot_{(R ↾_{𝑠} U)} (K \cdot_{(R ↾_{𝑠} U)} y) = Z \cdot_{(R ↾_{𝑠} U)} 0_{(R ↾_{𝑠} U)}$
268	239 241 172	syl2anc	$⊢ (φ \land y \in (R PrimRoots K)) \to Z \cdot_{(R ↾_{𝑠} U)} 0_{(R ↾_{𝑠} U)} = 0_{(R ↾_{𝑠} U)}$
269	267 268	eqtrd	$⊢ (φ \land y \in (R PrimRoots K)) \to Z \cdot_{(R ↾_{𝑠} U)} (K \cdot_{(R ↾_{𝑠} U)} y) = 0_{(R ↾_{𝑠} U)}$
270	257 269	eqtrd	$⊢ (φ \land y \in (R PrimRoots K)) \to Z K \cdot_{(R ↾_{𝑠} U)} y = 0_{(R ↾_{𝑠} U)}$
271	270	fveq2d	$⊢ (φ \land y \in (R PrimRoots K)) \to {inv}_{g} (R ↾_{𝑠} U) (Z K \cdot_{(R ↾_{𝑠} U)} y) = {inv}_{g} (R ↾_{𝑠} U) (0_{(R ↾_{𝑠} U)})$
272	239 177	syl	$⊢ (φ \land y \in (R PrimRoots K)) \to {inv}_{g} (R ↾_{𝑠} U) (0_{(R ↾_{𝑠} U)}) = 0_{(R ↾_{𝑠} U)}$
273	271 272	eqtrd	$⊢ (φ \land y \in (R PrimRoots K)) \to {inv}_{g} (R ↾_{𝑠} U) (Z K \cdot_{(R ↾_{𝑠} U)} y) = 0_{(R ↾_{𝑠} U)}$
274	254 273	eqtrd	$⊢ (φ \land y \in (R PrimRoots K)) \to (- Z K) \cdot_{(R ↾_{𝑠} U)} y = 0_{(R ↾_{𝑠} U)}$
275	252 274	oveq12d	$⊢ (φ \land y \in (R PrimRoots K)) \to (1 \cdot_{(R ↾_{𝑠} U)} y) +_{(R ↾_{𝑠} U)} ((- Z K) \cdot_{(R ↾_{𝑠} U)} y) = y +_{(R ↾_{𝑠} U)} 0_{(R ↾_{𝑠} U)}$
276	156 157 171 239 247	grpridd	$⊢ (φ \land y \in (R PrimRoots K)) \to y +_{(R ↾_{𝑠} U)} 0_{(R ↾_{𝑠} U)} = y$
277	275 276	eqtrd	$⊢ (φ \land y \in (R PrimRoots K)) \to (1 \cdot_{(R ↾_{𝑠} U)} y) +_{(R ↾_{𝑠} U)} ((- Z K) \cdot_{(R ↾_{𝑠} U)} y) = y$
278	250 277	eqtrd	$⊢ (φ \land y \in (R PrimRoots K)) \to (1 + (- Z K)) \cdot_{(R ↾_{𝑠} U)} y = y$
279	238 278	eqtrd	$⊢ (φ \land y \in (R PrimRoots K)) \to I \cdot J \cdot_{(R ↾_{𝑠} U)} y = y$
280	236 279	eqtrd	$⊢ (φ \land y \in (R PrimRoots K)) \to I \cdot J \cdot_{R} y = y$
281	226 280	eqtr3d	$⊢ (φ \land y \in (R PrimRoots K)) \to I \cdot_{R} (J \cdot_{R} y) = y$
282	223 281	eqtrd	$⊢ (φ \land y \in (R PrimRoots K)) \to F (J \cdot_{R} y) = y$
283	211 282	eqtrd	$⊢ (φ \land y \in (R PrimRoots K)) \to F ((n \in (R PrimRoots K) ⟼ J \cdot_{R} n) (y)) = y$
284	283	ralrimiva	$⊢ φ \to \forall y \in (R PrimRoots K) F ((n \in (R PrimRoots K) ⟼ J \cdot_{R} n) (y)) = y$
285	19 33 197 284	2fvidf1od	$⊢ φ \to F : R PrimRoots K \underset{1-1 onto}{⟶} R PrimRoots K$

Metamath Proof Explorer

Theorem primrootscoprbij

Proof