aks6d1c6isolem1

Description: Lemma to construct the map out of the quotient for AKS. (Contributed by metakunt, 14-May-2025)

	Ref	Expression
Hypotheses	aks6d1c6isolem1.1	$⊢ φ \to R \in CMnd$
	aks6d1c6isolem1.2	$⊢ φ \to K \in ℕ$
	aks6d1c6isolem1.3	$⊢ U = \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\}$
	aks6d1c6isolem1.4	$⊢ F = (x \in ℤ ⟼ x \cdot_{(R ↾_{𝑠} U)} M)$
	aks6d1c6isolem1.5	$⊢ φ \to M \in (R PrimRoots K)$
Assertion	aks6d1c6isolem1	$⊢ φ \to (R ↾_{𝑠} U) ↾_{𝑠} ran F \in Grp$

Proof

Step	Hyp	Ref	Expression
1		aks6d1c6isolem1.1	$⊢ φ \to R \in CMnd$
2		aks6d1c6isolem1.2	$⊢ φ \to K \in ℕ$
3		aks6d1c6isolem1.3	$⊢ U = \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\}$
4		aks6d1c6isolem1.4	$⊢ F = (x \in ℤ ⟼ x \cdot_{(R ↾_{𝑠} U)} M)$
5		aks6d1c6isolem1.5	$⊢ φ \to M \in (R PrimRoots K)$
6		eqidd	$⊢ φ \to (R ↾_{𝑠} U) ↾_{𝑠} ran F = (R ↾_{𝑠} U) ↾_{𝑠} ran F$
7		eqidd	$⊢ φ \to 0_{(R ↾_{𝑠} U)} = 0_{(R ↾_{𝑠} U)}$
8		eqidd	$⊢ φ \to +_{(R ↾_{𝑠} U)} = +_{(R ↾_{𝑠} U)}$
9		eqid	$⊢ {Base}_{(R ↾_{𝑠} U)} = {Base}_{(R ↾_{𝑠} U)}$
10		eqid	$⊢ \cdot_{(R ↾_{𝑠} U)} = \cdot_{(R ↾_{𝑠} U)}$
11	1 2 3	primrootsunit	$⊢ φ \to (R PrimRoots K = (R ↾_{𝑠} U) PrimRoots K \land R ↾_{𝑠} U \in Abel)$
12	11	simprd	$⊢ φ \to R ↾_{𝑠} U \in Abel$
13	12	ablgrpd	$⊢ φ \to R ↾_{𝑠} U \in Grp$
14	13	adantr	$⊢ (φ \land x \in ℤ) \to R ↾_{𝑠} U \in Grp$
15		simpr	$⊢ (φ \land x \in ℤ) \to x \in ℤ$
16	11	simpld	$⊢ φ \to R PrimRoots K = (R ↾_{𝑠} U) PrimRoots K$
17	5 16	eleqtrd	$⊢ φ \to M \in ((R ↾_{𝑠} U) PrimRoots K)$
18	12	ablcmnd	$⊢ φ \to R ↾_{𝑠} U \in CMnd$
19	2	nnnn0d	$⊢ φ \to K \in ℕ_{0}$
20	18 19 10	isprimroot	$⊢ φ \to (M \in ((R ↾_{𝑠} U) PrimRoots K) \leftrightarrow (M \in {Base}_{(R ↾_{𝑠} U)} \land K \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \land \forall l \in ℕ_{0} (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l)))$
21	20	biimpd	$⊢ φ \to (M \in ((R ↾_{𝑠} U) PrimRoots K) \to (M \in {Base}_{(R ↾_{𝑠} U)} \land K \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \land \forall l \in ℕ_{0} (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l)))$
22	17 21	mpd	$⊢ φ \to (M \in {Base}_{(R ↾_{𝑠} U)} \land K \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \land \forall l \in ℕ_{0} (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l))$
23	22	simp1d	$⊢ φ \to M \in {Base}_{(R ↾_{𝑠} U)}$
24	23	adantr	$⊢ (φ \land x \in ℤ) \to M \in {Base}_{(R ↾_{𝑠} U)}$
25	9 10 14 15 24	mulgcld	$⊢ (φ \land x \in ℤ) \to x \cdot_{(R ↾_{𝑠} U)} M \in {Base}_{(R ↾_{𝑠} U)}$
26	25 4	fmptd	$⊢ φ \to F : ℤ ⟶ {Base}_{(R ↾_{𝑠} U)}$
27		frn	$⊢ F : ℤ ⟶ {Base}_{(R ↾_{𝑠} U)} \to ran F \subseteq {Base}_{(R ↾_{𝑠} U)}$
28	26 27	syl	$⊢ φ \to ran F \subseteq {Base}_{(R ↾_{𝑠} U)}$
29		0zd	$⊢ φ \to 0 \in ℤ$
30		simpr	$⊢ (φ \land c = 0) \to c = 0$
31	30	fveqeq2d	$⊢ (φ \land c = 0) \to (F (c) = 0_{(R ↾_{𝑠} U)} \leftrightarrow F (0) = 0_{(R ↾_{𝑠} U)})$
32	4	a1i	$⊢ φ \to F = (x \in ℤ ⟼ x \cdot_{(R ↾_{𝑠} U)} M)$
33		simpr	$⊢ (φ \land x = 0) \to x = 0$
34	33	oveq1d	$⊢ (φ \land x = 0) \to x \cdot_{(R ↾_{𝑠} U)} M = 0 \cdot_{(R ↾_{𝑠} U)} M$
35		eqid	$⊢ 0_{(R ↾_{𝑠} U)} = 0_{(R ↾_{𝑠} U)}$
36	9 35 10	mulg0	$⊢ M \in {Base}_{(R ↾_{𝑠} U)} \to 0 \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)}$
37	23 36	syl	$⊢ φ \to 0 \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)}$
38	37	adantr	$⊢ (φ \land x = 0) \to 0 \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)}$
39	34 38	eqtrd	$⊢ (φ \land x = 0) \to x \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)}$
40		fvexd	$⊢ φ \to 0_{(R ↾_{𝑠} U)} \in V$
41	32 39 29 40	fvmptd	$⊢ φ \to F (0) = 0_{(R ↾_{𝑠} U)}$
42	29 31 41	rspcedvd	$⊢ φ \to \exists c \in ℤ F (c) = 0_{(R ↾_{𝑠} U)}$
43	26	ffnd	$⊢ φ \to F Fn ℤ$
44		fvelrnb	$⊢ F Fn ℤ \to (0_{(R ↾_{𝑠} U)} \in ran F \leftrightarrow \exists c \in ℤ F (c) = 0_{(R ↾_{𝑠} U)})$
45	43 44	syl	$⊢ φ \to (0_{(R ↾_{𝑠} U)} \in ran F \leftrightarrow \exists c \in ℤ F (c) = 0_{(R ↾_{𝑠} U)})$
46	42 45	mpbird	$⊢ φ \to 0_{(R ↾_{𝑠} U)} \in ran F$
47		fvelrnb	$⊢ F Fn ℤ \to (y \in ran F \leftrightarrow \exists d \in ℤ F (d) = y)$
48	43 47	syl	$⊢ φ \to (y \in ran F \leftrightarrow \exists d \in ℤ F (d) = y)$
49	48	biimpd	$⊢ φ \to (y \in ran F \to \exists d \in ℤ F (d) = y)$
50	49	imp	$⊢ (φ \land y \in ran F) \to \exists d \in ℤ F (d) = y$
51	50	3adant3	$⊢ (φ \land y \in ran F \land z \in ran F) \to \exists d \in ℤ F (d) = y$
52		simpl1	$⊢ ((φ \land y \in ran F \land z \in ran F) \land \exists d \in ℤ F (d) = y) \to φ$
53		simpl3	$⊢ ((φ \land y \in ran F \land z \in ran F) \land \exists d \in ℤ F (d) = y) \to z \in ran F$
54	52 53	jca	$⊢ ((φ \land y \in ran F \land z \in ran F) \land \exists d \in ℤ F (d) = y) \to (φ \land z \in ran F)$
55		fvelrnb	$⊢ F Fn ℤ \to (z \in ran F \leftrightarrow \exists e \in ℤ F (e) = z)$
56	43 55	syl	$⊢ φ \to (z \in ran F \leftrightarrow \exists e \in ℤ F (e) = z)$
57	56	biimpd	$⊢ φ \to (z \in ran F \to \exists e \in ℤ F (e) = z)$
58	57	imp	$⊢ (φ \land z \in ran F) \to \exists e \in ℤ F (e) = z$
59	54 58	syl	$⊢ ((φ \land y \in ran F \land z \in ran F) \land \exists d \in ℤ F (d) = y) \to \exists e \in ℤ F (e) = z$
60		simpll1	$⊢ (((φ \land y \in ran F \land z \in ran F) \land \exists d \in ℤ F (d) = y) \land \exists e \in ℤ F (e) = z) \to φ$
61		simplr	$⊢ (((φ \land y \in ran F \land z \in ran F) \land \exists d \in ℤ F (d) = y) \land \exists e \in ℤ F (e) = z) \to \exists d \in ℤ F (d) = y$
62		simpr	$⊢ (((φ \land y \in ran F \land z \in ran F) \land \exists d \in ℤ F (d) = y) \land \exists e \in ℤ F (e) = z) \to \exists e \in ℤ F (e) = z$
63	60 61 62	3jca	$⊢ (((φ \land y \in ran F \land z \in ran F) \land \exists d \in ℤ F (d) = y) \land \exists e \in ℤ F (e) = z) \to (φ \land \exists d \in ℤ F (d) = y \land \exists e \in ℤ F (e) = z)$
64		simpr	$⊢ (((φ \land \exists d \in ℤ F (d) = y \land \exists e \in ℤ F (e) = z) \land g \in ℤ) \land F (g) = z) \to F (g) = z$
65	64	eqcomd	$⊢ (((φ \land \exists d \in ℤ F (d) = y \land \exists e \in ℤ F (e) = z) \land g \in ℤ) \land F (g) = z) \to z = F (g)$
66	65	oveq2d	$⊢ (((φ \land \exists d \in ℤ F (d) = y \land \exists e \in ℤ F (e) = z) \land g \in ℤ) \land F (g) = z) \to y +_{(R ↾_{𝑠} U)} z = y +_{(R ↾_{𝑠} U)} F (g)$
67		simpr	$⊢ ((((φ \land \exists d \in ℤ F (d) = y \land \exists e \in ℤ F (e) = z) \land g \in ℤ) \land f \in ℤ) \land F (f) = y) \to F (f) = y$
68	67	eqcomd	$⊢ ((((φ \land \exists d \in ℤ F (d) = y \land \exists e \in ℤ F (e) = z) \land g \in ℤ) \land f \in ℤ) \land F (f) = y) \to y = F (f)$
69	68	oveq1d	$⊢ ((((φ \land \exists d \in ℤ F (d) = y \land \exists e \in ℤ F (e) = z) \land g \in ℤ) \land f \in ℤ) \land F (f) = y) \to y +_{(R ↾_{𝑠} U)} F (g) = F (f) +_{(R ↾_{𝑠} U)} F (g)$
70		simpll1	$⊢ (((φ \land \exists d \in ℤ F (d) = y \land \exists e \in ℤ F (e) = z) \land g \in ℤ) \land f \in ℤ) \to φ$
71	70	adantr	$⊢ ((((φ \land \exists d \in ℤ F (d) = y \land \exists e \in ℤ F (e) = z) \land g \in ℤ) \land f \in ℤ) \land F (f) = y) \to φ$
72		simpllr	$⊢ ((((φ \land \exists d \in ℤ F (d) = y \land \exists e \in ℤ F (e) = z) \land g \in ℤ) \land f \in ℤ) \land F (f) = y) \to g \in ℤ$
73		simplr	$⊢ ((((φ \land \exists d \in ℤ F (d) = y \land \exists e \in ℤ F (e) = z) \land g \in ℤ) \land f \in ℤ) \land F (f) = y) \to f \in ℤ$
74	71 72 73	3jca	$⊢ ((((φ \land \exists d \in ℤ F (d) = y \land \exists e \in ℤ F (e) = z) \land g \in ℤ) \land f \in ℤ) \land F (f) = y) \to (φ \land g \in ℤ \land f \in ℤ)$
75	4	a1i	$⊢ (φ \land g \in ℤ \land f \in ℤ) \to F = (x \in ℤ ⟼ x \cdot_{(R ↾_{𝑠} U)} M)$
76		simpr	$⊢ ((φ \land g \in ℤ \land f \in ℤ) \land x = f) \to x = f$
77	76	oveq1d	$⊢ ((φ \land g \in ℤ \land f \in ℤ) \land x = f) \to x \cdot_{(R ↾_{𝑠} U)} M = f \cdot_{(R ↾_{𝑠} U)} M$
78		simp3	$⊢ (φ \land g \in ℤ \land f \in ℤ) \to f \in ℤ$
79		ovexd	$⊢ (φ \land g \in ℤ \land f \in ℤ) \to f \cdot_{(R ↾_{𝑠} U)} M \in V$
80	75 77 78 79	fvmptd	$⊢ (φ \land g \in ℤ \land f \in ℤ) \to F (f) = f \cdot_{(R ↾_{𝑠} U)} M$
81		simpr	$⊢ ((φ \land g \in ℤ \land f \in ℤ) \land x = g) \to x = g$
82	81	oveq1d	$⊢ ((φ \land g \in ℤ \land f \in ℤ) \land x = g) \to x \cdot_{(R ↾_{𝑠} U)} M = g \cdot_{(R ↾_{𝑠} U)} M$
83		simp2	$⊢ (φ \land g \in ℤ \land f \in ℤ) \to g \in ℤ$
84		ovexd	$⊢ (φ \land g \in ℤ \land f \in ℤ) \to g \cdot_{(R ↾_{𝑠} U)} M \in V$
85	75 82 83 84	fvmptd	$⊢ (φ \land g \in ℤ \land f \in ℤ) \to F (g) = g \cdot_{(R ↾_{𝑠} U)} M$
86	80 85	oveq12d	$⊢ (φ \land g \in ℤ \land f \in ℤ) \to F (f) +_{(R ↾_{𝑠} U)} F (g) = (f \cdot_{(R ↾_{𝑠} U)} M) +_{(R ↾_{𝑠} U)} (g \cdot_{(R ↾_{𝑠} U)} M)$
87	13	3ad2ant1	$⊢ (φ \land g \in ℤ \land f \in ℤ) \to R ↾_{𝑠} U \in Grp$
88	23	3ad2ant1	$⊢ (φ \land g \in ℤ \land f \in ℤ) \to M \in {Base}_{(R ↾_{𝑠} U)}$
89	78 83 88	3jca	$⊢ (φ \land g \in ℤ \land f \in ℤ) \to (f \in ℤ \land g \in ℤ \land M \in {Base}_{(R ↾_{𝑠} U)})$
90		eqid	$⊢ +_{(R ↾_{𝑠} U)} = +_{(R ↾_{𝑠} U)}$
91	9 10 90	mulgdir	$⊢ (R ↾_{𝑠} U \in Grp \land (f \in ℤ \land g \in ℤ \land M \in {Base}_{(R ↾_{𝑠} U)})) \to (f + g) \cdot_{(R ↾_{𝑠} U)} M = (f \cdot_{(R ↾_{𝑠} U)} M) +_{(R ↾_{𝑠} U)} (g \cdot_{(R ↾_{𝑠} U)} M)$
92	87 89 91	syl2anc	$⊢ (φ \land g \in ℤ \land f \in ℤ) \to (f + g) \cdot_{(R ↾_{𝑠} U)} M = (f \cdot_{(R ↾_{𝑠} U)} M) +_{(R ↾_{𝑠} U)} (g \cdot_{(R ↾_{𝑠} U)} M)$
93	78 83	zaddcld	$⊢ (φ \land g \in ℤ \land f \in ℤ) \to f + g \in ℤ$
94		simpr	$⊢ ((φ \land g \in ℤ \land f \in ℤ) \land h = f + g) \to h = f + g$
95	94	fveqeq2d	$⊢ ((φ \land g \in ℤ \land f \in ℤ) \land h = f + g) \to (F (h) = (f + g) \cdot_{(R ↾_{𝑠} U)} M \leftrightarrow F (f + g) = (f + g) \cdot_{(R ↾_{𝑠} U)} M)$
96		simpr	$⊢ ((φ \land g \in ℤ \land f \in ℤ) \land x = f + g) \to x = f + g$
97	96	oveq1d	$⊢ ((φ \land g \in ℤ \land f \in ℤ) \land x = f + g) \to x \cdot_{(R ↾_{𝑠} U)} M = (f + g) \cdot_{(R ↾_{𝑠} U)} M$
98		ovexd	$⊢ (φ \land g \in ℤ \land f \in ℤ) \to (f + g) \cdot_{(R ↾_{𝑠} U)} M \in V$
99	75 97 93 98	fvmptd	$⊢ (φ \land g \in ℤ \land f \in ℤ) \to F (f + g) = (f + g) \cdot_{(R ↾_{𝑠} U)} M$
100	93 95 99	rspcedvd	$⊢ (φ \land g \in ℤ \land f \in ℤ) \to \exists h \in ℤ F (h) = (f + g) \cdot_{(R ↾_{𝑠} U)} M$
101		fvelrnb	$⊢ F Fn ℤ \to ((f + g) \cdot_{(R ↾_{𝑠} U)} M \in ran F \leftrightarrow \exists h \in ℤ F (h) = (f + g) \cdot_{(R ↾_{𝑠} U)} M)$
102	43 101	syl	$⊢ φ \to ((f + g) \cdot_{(R ↾_{𝑠} U)} M \in ran F \leftrightarrow \exists h \in ℤ F (h) = (f + g) \cdot_{(R ↾_{𝑠} U)} M)$
103	102	3ad2ant1	$⊢ (φ \land g \in ℤ \land f \in ℤ) \to ((f + g) \cdot_{(R ↾_{𝑠} U)} M \in ran F \leftrightarrow \exists h \in ℤ F (h) = (f + g) \cdot_{(R ↾_{𝑠} U)} M)$
104	100 103	mpbird	$⊢ (φ \land g \in ℤ \land f \in ℤ) \to (f + g) \cdot_{(R ↾_{𝑠} U)} M \in ran F$
105	92 104	eqeltrrd	$⊢ (φ \land g \in ℤ \land f \in ℤ) \to (f \cdot_{(R ↾_{𝑠} U)} M) +_{(R ↾_{𝑠} U)} (g \cdot_{(R ↾_{𝑠} U)} M) \in ran F$
106	86 105	eqeltrd	$⊢ (φ \land g \in ℤ \land f \in ℤ) \to F (f) +_{(R ↾_{𝑠} U)} F (g) \in ran F$
107	74 106	syl	$⊢ ((((φ \land \exists d \in ℤ F (d) = y \land \exists e \in ℤ F (e) = z) \land g \in ℤ) \land f \in ℤ) \land F (f) = y) \to F (f) +_{(R ↾_{𝑠} U)} F (g) \in ran F$
108	69 107	eqeltrd	$⊢ ((((φ \land \exists d \in ℤ F (d) = y \land \exists e \in ℤ F (e) = z) \land g \in ℤ) \land f \in ℤ) \land F (f) = y) \to y +_{(R ↾_{𝑠} U)} F (g) \in ran F$
109		simpl2	$⊢ ((φ \land \exists d \in ℤ F (d) = y \land \exists e \in ℤ F (e) = z) \land g \in ℤ) \to \exists d \in ℤ F (d) = y$
110		nfv	$⊢ Ⅎ f F (d) = y$
111		nfv	$⊢ Ⅎ d F (f) = y$
112		fveqeq2	$⊢ d = f \to (F (d) = y \leftrightarrow F (f) = y)$
113	110 111 112	cbvrexw	$⊢ \exists d \in ℤ F (d) = y \leftrightarrow \exists f \in ℤ F (f) = y$
114	113	biimpi	$⊢ \exists d \in ℤ F (d) = y \to \exists f \in ℤ F (f) = y$
115	109 114	syl	$⊢ ((φ \land \exists d \in ℤ F (d) = y \land \exists e \in ℤ F (e) = z) \land g \in ℤ) \to \exists f \in ℤ F (f) = y$
116	108 115	r19.29a	$⊢ ((φ \land \exists d \in ℤ F (d) = y \land \exists e \in ℤ F (e) = z) \land g \in ℤ) \to y +_{(R ↾_{𝑠} U)} F (g) \in ran F$
117	116	adantr	$⊢ (((φ \land \exists d \in ℤ F (d) = y \land \exists e \in ℤ F (e) = z) \land g \in ℤ) \land F (g) = z) \to y +_{(R ↾_{𝑠} U)} F (g) \in ran F$
118	66 117	eqeltrd	$⊢ (((φ \land \exists d \in ℤ F (d) = y \land \exists e \in ℤ F (e) = z) \land g \in ℤ) \land F (g) = z) \to y +_{(R ↾_{𝑠} U)} z \in ran F$
119		simp3	$⊢ (φ \land \exists d \in ℤ F (d) = y \land \exists e \in ℤ F (e) = z) \to \exists e \in ℤ F (e) = z$
120		nfv	$⊢ Ⅎ g F (e) = z$
121		nfv	$⊢ Ⅎ e F (g) = z$
122		fveqeq2	$⊢ e = g \to (F (e) = z \leftrightarrow F (g) = z)$
123	120 121 122	cbvrexw	$⊢ \exists e \in ℤ F (e) = z \leftrightarrow \exists g \in ℤ F (g) = z$
124	123	biimpi	$⊢ \exists e \in ℤ F (e) = z \to \exists g \in ℤ F (g) = z$
125	119 124	syl	$⊢ (φ \land \exists d \in ℤ F (d) = y \land \exists e \in ℤ F (e) = z) \to \exists g \in ℤ F (g) = z$
126	118 125	r19.29a	$⊢ (φ \land \exists d \in ℤ F (d) = y \land \exists e \in ℤ F (e) = z) \to y +_{(R ↾_{𝑠} U)} z \in ran F$
127	63 126	syl	$⊢ (((φ \land y \in ran F \land z \in ran F) \land \exists d \in ℤ F (d) = y) \land \exists e \in ℤ F (e) = z) \to y +_{(R ↾_{𝑠} U)} z \in ran F$
128	127	ex	$⊢ ((φ \land y \in ran F \land z \in ran F) \land \exists d \in ℤ F (d) = y) \to (\exists e \in ℤ F (e) = z \to y +_{(R ↾_{𝑠} U)} z \in ran F)$
129	59 128	mpd	$⊢ ((φ \land y \in ran F \land z \in ran F) \land \exists d \in ℤ F (d) = y) \to y +_{(R ↾_{𝑠} U)} z \in ran F$
130	51 129	mpdan	$⊢ (φ \land y \in ran F \land z \in ran F) \to y +_{(R ↾_{𝑠} U)} z \in ran F$
131		simpr	$⊢ (((φ \land \exists d \in ℤ F (d) = y) \land f \in ℤ) \land F (f) = y) \to F (f) = y$
132	131	eqcomd	$⊢ (((φ \land \exists d \in ℤ F (d) = y) \land f \in ℤ) \land F (f) = y) \to y = F (f)$
133	132	fveq2d	$⊢ (((φ \land \exists d \in ℤ F (d) = y) \land f \in ℤ) \land F (f) = y) \to {inv}_{g} (R ↾_{𝑠} U) (y) = {inv}_{g} (R ↾_{𝑠} U) (F (f))$
134		simplll	$⊢ (((φ \land \exists d \in ℤ F (d) = y) \land f \in ℤ) \land F (f) = y) \to φ$
135		simplr	$⊢ (((φ \land \exists d \in ℤ F (d) = y) \land f \in ℤ) \land F (f) = y) \to f \in ℤ$
136	134 135	jca	$⊢ (((φ \land \exists d \in ℤ F (d) = y) \land f \in ℤ) \land F (f) = y) \to (φ \land f \in ℤ)$
137		simpr	$⊢ (φ \land f \in ℤ) \to f \in ℤ$
138	137	znegcld	$⊢ (φ \land f \in ℤ) \to - f \in ℤ$
139		simpr	$⊢ ((φ \land f \in ℤ) \land h = - f) \to h = - f$
140	139	fveqeq2d	$⊢ ((φ \land f \in ℤ) \land h = - f) \to (F (h) = {inv}_{g} (R ↾_{𝑠} U) (F (f)) \leftrightarrow F (- f) = {inv}_{g} (R ↾_{𝑠} U) (F (f)))$
141	4	a1i	$⊢ (φ \land f \in ℤ) \to F = (x \in ℤ ⟼ x \cdot_{(R ↾_{𝑠} U)} M)$
142		simpr	$⊢ ((φ \land f \in ℤ) \land x = - f) \to x = - f$
143	142	oveq1d	$⊢ ((φ \land f \in ℤ) \land x = - f) \to x \cdot_{(R ↾_{𝑠} U)} M = (- f) \cdot_{(R ↾_{𝑠} U)} M$
144		ovexd	$⊢ (φ \land f \in ℤ) \to (- f) \cdot_{(R ↾_{𝑠} U)} M \in V$
145	141 143 138 144	fvmptd	$⊢ (φ \land f \in ℤ) \to F (- f) = (- f) \cdot_{(R ↾_{𝑠} U)} M$
146	13	adantr	$⊢ (φ \land f \in ℤ) \to R ↾_{𝑠} U \in Grp$
147	23	adantr	$⊢ (φ \land f \in ℤ) \to M \in {Base}_{(R ↾_{𝑠} U)}$
148		eqid	$⊢ {inv}_{g} (R ↾_{𝑠} U) = {inv}_{g} (R ↾_{𝑠} U)$
149	9 10 148	mulgneg	$⊢ (R ↾_{𝑠} U \in Grp \land f \in ℤ \land M \in {Base}_{(R ↾_{𝑠} U)}) \to (- f) \cdot_{(R ↾_{𝑠} U)} M = {inv}_{g} (R ↾_{𝑠} U) (f \cdot_{(R ↾_{𝑠} U)} M)$
150	146 137 147 149	syl3anc	$⊢ (φ \land f \in ℤ) \to (- f) \cdot_{(R ↾_{𝑠} U)} M = {inv}_{g} (R ↾_{𝑠} U) (f \cdot_{(R ↾_{𝑠} U)} M)$
151		simpr	$⊢ ((φ \land f \in ℤ) \land x = f) \to x = f$
152	151	oveq1d	$⊢ ((φ \land f \in ℤ) \land x = f) \to x \cdot_{(R ↾_{𝑠} U)} M = f \cdot_{(R ↾_{𝑠} U)} M$
153		ovexd	$⊢ (φ \land f \in ℤ) \to f \cdot_{(R ↾_{𝑠} U)} M \in V$
154	141 152 137 153	fvmptd	$⊢ (φ \land f \in ℤ) \to F (f) = f \cdot_{(R ↾_{𝑠} U)} M$
155	154	eqcomd	$⊢ (φ \land f \in ℤ) \to f \cdot_{(R ↾_{𝑠} U)} M = F (f)$
156	155	fveq2d	$⊢ (φ \land f \in ℤ) \to {inv}_{g} (R ↾_{𝑠} U) (f \cdot_{(R ↾_{𝑠} U)} M) = {inv}_{g} (R ↾_{𝑠} U) (F (f))$
157	150 156	eqtrd	$⊢ (φ \land f \in ℤ) \to (- f) \cdot_{(R ↾_{𝑠} U)} M = {inv}_{g} (R ↾_{𝑠} U) (F (f))$
158	145 157	eqtrd	$⊢ (φ \land f \in ℤ) \to F (- f) = {inv}_{g} (R ↾_{𝑠} U) (F (f))$
159	138 140 158	rspcedvd	$⊢ (φ \land f \in ℤ) \to \exists h \in ℤ F (h) = {inv}_{g} (R ↾_{𝑠} U) (F (f))$
160		fvelrnb	$⊢ F Fn ℤ \to ({inv}_{g} (R ↾_{𝑠} U) (F (f)) \in ran F \leftrightarrow \exists h \in ℤ F (h) = {inv}_{g} (R ↾_{𝑠} U) (F (f)))$
161	43 160	syl	$⊢ φ \to ({inv}_{g} (R ↾_{𝑠} U) (F (f)) \in ran F \leftrightarrow \exists h \in ℤ F (h) = {inv}_{g} (R ↾_{𝑠} U) (F (f)))$
162	161	adantr	$⊢ (φ \land f \in ℤ) \to ({inv}_{g} (R ↾_{𝑠} U) (F (f)) \in ran F \leftrightarrow \exists h \in ℤ F (h) = {inv}_{g} (R ↾_{𝑠} U) (F (f)))$
163	159 162	mpbird	$⊢ (φ \land f \in ℤ) \to {inv}_{g} (R ↾_{𝑠} U) (F (f)) \in ran F$
164	163	a1i	$⊢ (((φ \land \exists d \in ℤ F (d) = y) \land f \in ℤ) \land F (f) = y) \to ((φ \land f \in ℤ) \to {inv}_{g} (R ↾_{𝑠} U) (F (f)) \in ran F)$
165	136 164	mpd	$⊢ (((φ \land \exists d \in ℤ F (d) = y) \land f \in ℤ) \land F (f) = y) \to {inv}_{g} (R ↾_{𝑠} U) (F (f)) \in ran F$
166	133 165	eqeltrd	$⊢ (((φ \land \exists d \in ℤ F (d) = y) \land f \in ℤ) \land F (f) = y) \to {inv}_{g} (R ↾_{𝑠} U) (y) \in ran F$
167	113	bilani	$⊢ (φ \land \exists d \in ℤ F (d) = y) \to \exists f \in ℤ F (f) = y$
168	166 167	r19.29a	$⊢ (φ \land \exists d \in ℤ F (d) = y) \to {inv}_{g} (R ↾_{𝑠} U) (y) \in ran F$
169	168	ex	$⊢ φ \to (\exists d \in ℤ F (d) = y \to {inv}_{g} (R ↾_{𝑠} U) (y) \in ran F)$
170	169	adantr	$⊢ (φ \land y \in ran F) \to (\exists d \in ℤ F (d) = y \to {inv}_{g} (R ↾_{𝑠} U) (y) \in ran F)$
171	170	imp	$⊢ ((φ \land y \in ran F) \land \exists d \in ℤ F (d) = y) \to {inv}_{g} (R ↾_{𝑠} U) (y) \in ran F$
172	50 171	mpdan	$⊢ (φ \land y \in ran F) \to {inv}_{g} (R ↾_{𝑠} U) (y) \in ran F$
173	6 7 8 28 46 130 172 13	issubgrpd	$⊢ φ \to (R ↾_{𝑠} U) ↾_{𝑠} ran F \in Grp$

Metamath Proof Explorer

Theorem aks6d1c6isolem1

Proof