primrootscoprmpow

Description: Coprime powers of primitive roots are primitive roots. (Contributed by metakunt, 25-Apr-2025)

	Ref	Expression
Hypotheses	primrootscoprmpow.1	$⊢ φ \to R \in CMnd$
	primrootscoprmpow.2	$⊢ φ \to K \in ℕ$
	primrootscoprmpow.3	$⊢ φ \to E \in ℕ$
	primrootscoprmpow.4	$⊢ φ \to E \gcd K = 1$
	primrootscoprmpow.5	$⊢ φ \to M \in (R PrimRoots K)$
	primrootscoprmpow.6	$⊢ U = \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\}$
Assertion	primrootscoprmpow	$⊢ φ \to E \cdot_{R} M \in (R PrimRoots K)$

Proof

Step	Hyp	Ref	Expression
1		primrootscoprmpow.1	$⊢ φ \to R \in CMnd$
2		primrootscoprmpow.2	$⊢ φ \to K \in ℕ$
3		primrootscoprmpow.3	$⊢ φ \to E \in ℕ$
4		primrootscoprmpow.4	$⊢ φ \to E \gcd K = 1$
5		primrootscoprmpow.5	$⊢ φ \to M \in (R PrimRoots K)$
6		primrootscoprmpow.6	$⊢ U = \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\}$
7		eqid	$⊢ {Base}_{(R ↾_{𝑠} U)} = {Base}_{(R ↾_{𝑠} U)}$
8		eqid	$⊢ \cdot_{(R ↾_{𝑠} U)} = \cdot_{(R ↾_{𝑠} U)}$
9	1 2 6	primrootsunit	$⊢ φ \to (R PrimRoots K = (R ↾_{𝑠} U) PrimRoots K \land R ↾_{𝑠} U \in Abel)$
10	9	simprd	$⊢ φ \to R ↾_{𝑠} U \in Abel$
11	10	ablcmnd	$⊢ φ \to R ↾_{𝑠} U \in CMnd$
12	11	cmnmndd	$⊢ φ \to R ↾_{𝑠} U \in Mnd$
13	3	nnnn0d	$⊢ φ \to E \in ℕ_{0}$
14	9	simpld	$⊢ φ \to R PrimRoots K = (R ↾_{𝑠} U) PrimRoots K$
15	14	eleq2d	$⊢ φ \to (M \in (R PrimRoots K) \leftrightarrow M \in ((R ↾_{𝑠} U) PrimRoots K))$
16	5 15	mpbid	$⊢ φ \to M \in ((R ↾_{𝑠} U) PrimRoots K)$
17	2	nnnn0d	$⊢ φ \to K \in ℕ_{0}$
18	11 17 8	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)))$
19	18	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)))$
20	16 19	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))$
21	20	simp1d	$⊢ φ \to M \in {Base}_{(R ↾_{𝑠} U)}$
22	7 8 12 13 21	mulgnn0cld	$⊢ φ \to E \cdot_{(R ↾_{𝑠} U)} M \in {Base}_{(R ↾_{𝑠} U)}$
23	6	eleq2i	$⊢ c \in U \leftrightarrow c \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\}$
24		oveq2	$⊢ a = c \to i +_{R} a = i +_{R} c$
25	24	eqeq1d	$⊢ a = c \to (i +_{R} a = 0_{R} \leftrightarrow i +_{R} c = 0_{R})$
26	25	rexbidv	$⊢ a = c \to (\exists i \in {Base}_{R} i +_{R} a = 0_{R} \leftrightarrow \exists i \in {Base}_{R} i +_{R} c = 0_{R})$
27	26	elrab	$⊢ c \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\} \leftrightarrow (c \in {Base}_{R} \land \exists i \in {Base}_{R} i +_{R} c = 0_{R})$
28	23 27	bitri	$⊢ c \in U \leftrightarrow (c \in {Base}_{R} \land \exists i \in {Base}_{R} i +_{R} c = 0_{R})$
29	28	biimpi	$⊢ c \in U \to (c \in {Base}_{R} \land \exists i \in {Base}_{R} i +_{R} c = 0_{R})$
30	29	simpld	$⊢ c \in U \to c \in {Base}_{R}$
31	30	adantl	$⊢ (φ \land c \in U) \to c \in {Base}_{R}$
32	31	ex	$⊢ φ \to (c \in U \to c \in {Base}_{R})$
33	32	ssrdv	$⊢ φ \to U \subseteq {Base}_{R}$
34		oveq2	$⊢ a = 0_{R} \to i +_{R} a = i +_{R} 0_{R}$
35	34	eqeq1d	$⊢ a = 0_{R} \to (i +_{R} a = 0_{R} \leftrightarrow i +_{R} 0_{R} = 0_{R})$
36	35	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})$
37	1	cmnmndd	$⊢ φ \to R \in Mnd$
38		eqid	$⊢ {Base}_{R} = {Base}_{R}$
39		eqid	$⊢ 0_{R} = 0_{R}$
40	38 39	mndidcl	$⊢ R \in Mnd \to 0_{R} \in {Base}_{R}$
41	37 40	syl	$⊢ φ \to 0_{R} \in {Base}_{R}$
42		simpr	$⊢ (φ \land i = 0_{R}) \to i = 0_{R}$
43	42	oveq1d	$⊢ (φ \land i = 0_{R}) \to i +_{R} 0_{R} = 0_{R} +_{R} 0_{R}$
44	43	eqeq1d	$⊢ (φ \land i = 0_{R}) \to (i +_{R} 0_{R} = 0_{R} \leftrightarrow 0_{R} +_{R} 0_{R} = 0_{R})$
45		eqid	$⊢ +_{R} = +_{R}$
46	38 45 39	mndlid	$⊢ (R \in Mnd \land 0_{R} \in {Base}_{R}) \to 0_{R} +_{R} 0_{R} = 0_{R}$
47	37 41 46	syl2anc	$⊢ φ \to 0_{R} +_{R} 0_{R} = 0_{R}$
48	41 44 47	rspcedvd	$⊢ φ \to \exists i \in {Base}_{R} i +_{R} 0_{R} = 0_{R}$
49	36 41 48	elrabd	$⊢ φ \to 0_{R} \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\}$
50	6	a1i	$⊢ φ \to U = \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\}$
51	50	eleq2d	$⊢ φ \to (0_{R} \in U \leftrightarrow 0_{R} \in \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\})$
52	49 51	mpbird	$⊢ φ \to 0_{R} \in U$
53	33 52 12	3jca	$⊢ φ \to (U \subseteq {Base}_{R} \land 0_{R} \in U \land R ↾_{𝑠} U \in Mnd)$
54		eqid	$⊢ R ↾_{𝑠} U = R ↾_{𝑠} U$
55	38 39 54	issubm2	$⊢ R \in Mnd \to (U \in SubMnd (R) \leftrightarrow (U \subseteq {Base}_{R} \land 0_{R} \in U \land R ↾_{𝑠} U \in Mnd))$
56	37 55	syl	$⊢ φ \to (U \in SubMnd (R) \leftrightarrow (U \subseteq {Base}_{R} \land 0_{R} \in U \land R ↾_{𝑠} U \in Mnd))$
57	53 56	mpbird	$⊢ φ \to U \in SubMnd (R)$
58	54 38	ressbas2	$⊢ U \subseteq {Base}_{R} \to U = {Base}_{(R ↾_{𝑠} U)}$
59	33 58	syl	$⊢ φ \to U = {Base}_{(R ↾_{𝑠} U)}$
60	59	eleq2d	$⊢ φ \to (M \in U \leftrightarrow M \in {Base}_{(R ↾_{𝑠} U)})$
61	21 60	mpbird	$⊢ φ \to M \in U$
62		eqid	$⊢ \cdot_{R} = \cdot_{R}$
63	62 54 8	submmulg	$⊢ (U \in SubMnd (R) \land E \in ℕ_{0} \land M \in U) \to E \cdot_{R} M = E \cdot_{(R ↾_{𝑠} U)} M$
64	57 13 61 63	syl3anc	$⊢ φ \to E \cdot_{R} M = E \cdot_{(R ↾_{𝑠} U)} M$
65	64	eleq1d	$⊢ φ \to (E \cdot_{R} M \in {Base}_{(R ↾_{𝑠} U)} \leftrightarrow E \cdot_{(R ↾_{𝑠} U)} M \in {Base}_{(R ↾_{𝑠} U)})$
66	22 65	mpbird	$⊢ φ \to E \cdot_{R} M \in {Base}_{(R ↾_{𝑠} U)}$
67	64	oveq2d	$⊢ φ \to K \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = K \cdot_{(R ↾_{𝑠} U)} (E \cdot_{(R ↾_{𝑠} U)} M)$
68	10	ablgrpd	$⊢ φ \to R ↾_{𝑠} U \in Grp$
69	17	nn0zd	$⊢ φ \to K \in ℤ$
70	13	nn0zd	$⊢ φ \to E \in ℤ$
71	69 70 21	3jca	$⊢ φ \to (K \in ℤ \land E \in ℤ \land M \in {Base}_{(R ↾_{𝑠} U)})$
72	7 8	mulgass	$⊢ (R ↾_{𝑠} U \in Grp \land (K \in ℤ \land E \in ℤ \land M \in {Base}_{(R ↾_{𝑠} U)})) \to K E \cdot_{(R ↾_{𝑠} U)} M = K \cdot_{(R ↾_{𝑠} U)} (E \cdot_{(R ↾_{𝑠} U)} M)$
73	68 71 72	syl2anc	$⊢ φ \to K E \cdot_{(R ↾_{𝑠} U)} M = K \cdot_{(R ↾_{𝑠} U)} (E \cdot_{(R ↾_{𝑠} U)} M)$
74	2	nncnd	$⊢ φ \to K \in ℂ$
75	3	nncnd	$⊢ φ \to E \in ℂ$
76	74 75	mulcomd	$⊢ φ \to K E = E K$
77	76	oveq1d	$⊢ φ \to K E \cdot_{(R ↾_{𝑠} U)} M = E K \cdot_{(R ↾_{𝑠} U)} M$
78	70 69 21	3jca	$⊢ φ \to (E \in ℤ \land K \in ℤ \land M \in {Base}_{(R ↾_{𝑠} U)})$
79	7 8	mulgass	$⊢ (R ↾_{𝑠} U \in Grp \land (E \in ℤ \land K \in ℤ \land M \in {Base}_{(R ↾_{𝑠} U)})) \to E K \cdot_{(R ↾_{𝑠} U)} M = E \cdot_{(R ↾_{𝑠} U)} (K \cdot_{(R ↾_{𝑠} U)} M)$
80	68 78 79	syl2anc	$⊢ φ \to E K \cdot_{(R ↾_{𝑠} U)} M = E \cdot_{(R ↾_{𝑠} U)} (K \cdot_{(R ↾_{𝑠} U)} M)$
81	20	simp2d	$⊢ φ \to K \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)}$
82	81	oveq2d	$⊢ φ \to E \cdot_{(R ↾_{𝑠} U)} (K \cdot_{(R ↾_{𝑠} U)} M) = E \cdot_{(R ↾_{𝑠} U)} 0_{(R ↾_{𝑠} U)}$
83		eqid	$⊢ 0_{(R ↾_{𝑠} U)} = 0_{(R ↾_{𝑠} U)}$
84	7 8 83	mulgz	$⊢ (R ↾_{𝑠} U \in Grp \land E \in ℤ) \to E \cdot_{(R ↾_{𝑠} U)} 0_{(R ↾_{𝑠} U)} = 0_{(R ↾_{𝑠} U)}$
85	68 70 84	syl2anc	$⊢ φ \to E \cdot_{(R ↾_{𝑠} U)} 0_{(R ↾_{𝑠} U)} = 0_{(R ↾_{𝑠} U)}$
86	82 85	eqtrd	$⊢ φ \to E \cdot_{(R ↾_{𝑠} U)} (K \cdot_{(R ↾_{𝑠} U)} M) = 0_{(R ↾_{𝑠} U)}$
87	80 86	eqtrd	$⊢ φ \to E K \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)}$
88	77 87	eqtrd	$⊢ φ \to K E \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)}$
89	73 88	eqtr3d	$⊢ φ \to K \cdot_{(R ↾_{𝑠} U)} (E \cdot_{(R ↾_{𝑠} U)} M) = 0_{(R ↾_{𝑠} U)}$
90	67 89	eqtrd	$⊢ φ \to K \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}$
91	20	simp3d	$⊢ φ \to \forall l \in ℕ_{0} (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l)$
92		simp-6r	$⊢ ((((((φ \land l \in ℕ_{0}) \land (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l)) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \land E \gcd K = E x + K y) \to l \in ℕ_{0}$
93	92	nn0cnd	$⊢ ((((((φ \land l \in ℕ_{0}) \land (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l)) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \land E \gcd K = E x + K y) \to l \in ℂ$
94	93	mullidd	$⊢ ((((((φ \land l \in ℕ_{0}) \land (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l)) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \land E \gcd K = E x + K y) \to 1 l = l$
95	94	eqcomd	$⊢ ((((((φ \land l \in ℕ_{0}) \land (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l)) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \land E \gcd K = E x + K y) \to l = 1 l$
96		simpr	$⊢ ((((((φ \land l \in ℕ_{0}) \land (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l)) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \land E \gcd K = E x + K y) \to E \gcd K = E x + K y$
97	4	ad6antr	$⊢ ((((((φ \land l \in ℕ_{0}) \land (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l)) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \land E \gcd K = E x + K y) \to E \gcd K = 1$
98	96 97	eqtr3d	$⊢ ((((((φ \land l \in ℕ_{0}) \land (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l)) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \land E \gcd K = E x + K y) \to E x + K y = 1$
99	96 98	eqtr2d	$⊢ ((((((φ \land l \in ℕ_{0}) \land (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l)) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \land E \gcd K = E x + K y) \to 1 = E \gcd K$
100	99	oveq1d	$⊢ ((((((φ \land l \in ℕ_{0}) \land (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l)) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \land E \gcd K = E x + K y) \to 1 l = (E \gcd K) l$
101	95 100	eqtrd	$⊢ ((((((φ \land l \in ℕ_{0}) \land (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l)) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \land E \gcd K = E x + K y) \to l = (E \gcd K) l$
102	101	oveq1d	$⊢ ((((((φ \land l \in ℕ_{0}) \land (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l)) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \land E \gcd K = E x + K y) \to l \cdot_{(R ↾_{𝑠} U)} M = (E \gcd K) l \cdot_{(R ↾_{𝑠} U)} M$
103	96	oveq1d	$⊢ ((((((φ \land l \in ℕ_{0}) \land (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l)) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \land E \gcd K = E x + K y) \to (E \gcd K) l = (E x + K y) l$
104	103	oveq1d	$⊢ ((((((φ \land l \in ℕ_{0}) \land (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l)) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \land E \gcd K = E x + K y) \to (E \gcd K) l \cdot_{(R ↾_{𝑠} U)} M = (E x + K y) l \cdot_{(R ↾_{𝑠} U)} M$
105		simp-4l	$⊢ (((((φ \land l \in ℕ_{0}) \land (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l)) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to (φ \land l \in ℕ_{0})$
106		simpllr	$⊢ (((((φ \land l \in ℕ_{0}) \land (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l)) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}$
107		simplr	$⊢ (((((φ \land l \in ℕ_{0}) \land (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l)) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to x \in ℤ$
108	105 106 107	jca31	$⊢ (((((φ \land l \in ℕ_{0}) \land (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l)) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to (((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ)$
109		simpr	$⊢ (((((φ \land l \in ℕ_{0}) \land (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l)) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to y \in ℤ$
110	108 109	jca	$⊢ (((((φ \land l \in ℕ_{0}) \land (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l)) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to ((((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ)$
111	75	ad4antr	$⊢ ((((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to E \in ℂ$
112		simplr	$⊢ ((((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to x \in ℤ$
113	112	zcnd	$⊢ ((((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to x \in ℂ$
114	111 113	mulcld	$⊢ ((((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to E x \in ℂ$
115	74	ad4antr	$⊢ ((((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to K \in ℂ$
116		simpr	$⊢ ((((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to y \in ℤ$
117	116	zcnd	$⊢ ((((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to y \in ℂ$
118	115 117	mulcld	$⊢ ((((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to K y \in ℂ$
119		simp-4r	$⊢ ((((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to l \in ℕ_{0}$
120	119	nn0cnd	$⊢ ((((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to l \in ℂ$
121	114 118 120	adddird	$⊢ ((((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to (E x + K y) l = E x l + K y l$
122	121	oveq1d	$⊢ ((((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to (E x + K y) l \cdot_{(R ↾_{𝑠} U)} M = (E x l + K y l) \cdot_{(R ↾_{𝑠} U)} M$
123	68	ad4antr	$⊢ ((((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to R ↾_{𝑠} U \in Grp$
124	70	ad4antr	$⊢ ((((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to E \in ℤ$
125	124 112	zmulcld	$⊢ ((((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to E x \in ℤ$
126	119	nn0zd	$⊢ ((((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to l \in ℤ$
127	125 126	zmulcld	$⊢ ((((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to E x l \in ℤ$
128	69	ad4antr	$⊢ ((((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to K \in ℤ$
129	128 116	zmulcld	$⊢ ((((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to K y \in ℤ$
130	129 126	zmulcld	$⊢ ((((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to K y l \in ℤ$
131	21	ad4antr	$⊢ ((((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to M \in {Base}_{(R ↾_{𝑠} U)}$
132	127 130 131	3jca	$⊢ ((((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to (E x l \in ℤ \land K y l \in ℤ \land M \in {Base}_{(R ↾_{𝑠} U)})$
133		eqid	$⊢ +_{(R ↾_{𝑠} U)} = +_{(R ↾_{𝑠} U)}$
134	7 8 133	mulgdir	$⊢ (R ↾_{𝑠} U \in Grp \land (E x l \in ℤ \land K y l \in ℤ \land M \in {Base}_{(R ↾_{𝑠} U)})) \to (E x l + K y l) \cdot_{(R ↾_{𝑠} U)} M = (E x l \cdot_{(R ↾_{𝑠} U)} M) +_{(R ↾_{𝑠} U)} (K y l \cdot_{(R ↾_{𝑠} U)} M)$
135	123 132 134	syl2anc	$⊢ ((((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to (E x l + K y l) \cdot_{(R ↾_{𝑠} U)} M = (E x l \cdot_{(R ↾_{𝑠} U)} M) +_{(R ↾_{𝑠} U)} (K y l \cdot_{(R ↾_{𝑠} U)} M)$
136	75	ad3antrrr	$⊢ (((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \to E \in ℂ$
137		simpr	$⊢ (((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \to x \in ℤ$
138	137	zcnd	$⊢ (((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \to x \in ℂ$
139		simpllr	$⊢ (((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \to l \in ℕ_{0}$
140	139	nn0cnd	$⊢ (((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \to l \in ℂ$
141	136 138 140	mulassd	$⊢ (((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \to E x l = E x l$
142	138 140	mulcld	$⊢ (((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \to x l \in ℂ$
143	136 142	mulcomd	$⊢ (((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \to E x l = x l E$
144	141 143	eqtrd	$⊢ (((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \to E x l = x l E$
145	144	oveq1d	$⊢ (((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \to E x l \cdot_{(R ↾_{𝑠} U)} M = x l E \cdot_{(R ↾_{𝑠} U)} M$
146	68	ad3antrrr	$⊢ (((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \to R ↾_{𝑠} U \in Grp$
147	139	nn0zd	$⊢ (((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \to l \in ℤ$
148	137 147	zmulcld	$⊢ (((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \to x l \in ℤ$
149	70	ad3antrrr	$⊢ (((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \to E \in ℤ$
150	21	ad3antrrr	$⊢ (((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \to M \in {Base}_{(R ↾_{𝑠} U)}$
151	148 149 150	3jca	$⊢ (((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \to (x l \in ℤ \land E \in ℤ \land M \in {Base}_{(R ↾_{𝑠} U)})$
152	7 8	mulgass	$⊢ (R ↾_{𝑠} U \in Grp \land (x l \in ℤ \land E \in ℤ \land M \in {Base}_{(R ↾_{𝑠} U)})) \to x l E \cdot_{(R ↾_{𝑠} U)} M = x l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{(R ↾_{𝑠} U)} M)$
153	146 151 152	syl2anc	$⊢ (((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \to x l E \cdot_{(R ↾_{𝑠} U)} M = x l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{(R ↾_{𝑠} U)} M)$
154	22	ad3antrrr	$⊢ (((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \to E \cdot_{(R ↾_{𝑠} U)} M \in {Base}_{(R ↾_{𝑠} U)}$
155	137 147 154	3jca	$⊢ (((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \to (x \in ℤ \land l \in ℤ \land E \cdot_{(R ↾_{𝑠} U)} M \in {Base}_{(R ↾_{𝑠} U)})$
156	7 8	mulgass	$⊢ (R ↾_{𝑠} U \in Grp \land (x \in ℤ \land l \in ℤ \land E \cdot_{(R ↾_{𝑠} U)} M \in {Base}_{(R ↾_{𝑠} U)})) \to x l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{(R ↾_{𝑠} U)} M) = x \cdot_{(R ↾_{𝑠} U)} (l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{(R ↾_{𝑠} U)} M))$
157	146 155 156	syl2anc	$⊢ (((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \to x l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{(R ↾_{𝑠} U)} M) = x \cdot_{(R ↾_{𝑠} U)} (l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{(R ↾_{𝑠} U)} M))$
158	57	adantr	$⊢ (φ \land l \in ℕ_{0}) \to U \in SubMnd (R)$
159	13	adantr	$⊢ (φ \land l \in ℕ_{0}) \to E \in ℕ_{0}$
160	61	adantr	$⊢ (φ \land l \in ℕ_{0}) \to M \in U$
161	158 159 160 63	syl3anc	$⊢ (φ \land l \in ℕ_{0}) \to E \cdot_{R} M = E \cdot_{(R ↾_{𝑠} U)} M$
162	161	ad2antrr	$⊢ (((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \to E \cdot_{R} M = E \cdot_{(R ↾_{𝑠} U)} M$
163	162	eqcomd	$⊢ (((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \to E \cdot_{(R ↾_{𝑠} U)} M = E \cdot_{R} M$
164	163	oveq2d	$⊢ (((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \to l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{(R ↾_{𝑠} U)} M) = l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M)$
165		simplr	$⊢ (((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \to l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}$
166	164 165	eqtrd	$⊢ (((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \to l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{(R ↾_{𝑠} U)} M) = 0_{(R ↾_{𝑠} U)}$
167	166	oveq2d	$⊢ (((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \to x \cdot_{(R ↾_{𝑠} U)} (l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{(R ↾_{𝑠} U)} M)) = x \cdot_{(R ↾_{𝑠} U)} 0_{(R ↾_{𝑠} U)}$
168	7 8 83	mulgz	$⊢ (R ↾_{𝑠} U \in Grp \land x \in ℤ) \to x \cdot_{(R ↾_{𝑠} U)} 0_{(R ↾_{𝑠} U)} = 0_{(R ↾_{𝑠} U)}$
169	146 137 168	syl2anc	$⊢ (((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \to x \cdot_{(R ↾_{𝑠} U)} 0_{(R ↾_{𝑠} U)} = 0_{(R ↾_{𝑠} U)}$
170	167 169	eqtrd	$⊢ (((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \to x \cdot_{(R ↾_{𝑠} U)} (l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{(R ↾_{𝑠} U)} M)) = 0_{(R ↾_{𝑠} U)}$
171	157 170	eqtrd	$⊢ (((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \to x l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{(R ↾_{𝑠} U)} M) = 0_{(R ↾_{𝑠} U)}$
172	153 171	eqtrd	$⊢ (((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \to x l E \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)}$
173	145 172	eqtrd	$⊢ (((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \to E x l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)}$
174	173	adantr	$⊢ ((((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to E x l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)}$
175		simplll	$⊢ ((((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to (φ \land l \in ℕ_{0})$
176	175 116	jca	$⊢ ((((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to ((φ \land l \in ℕ_{0}) \land y \in ℤ)$
177	74	ad2antrr	$⊢ ((φ \land l \in ℕ_{0}) \land y \in ℤ) \to K \in ℂ$
178		simpr	$⊢ ((φ \land l \in ℕ_{0}) \land y \in ℤ) \to y \in ℤ$
179	178	zcnd	$⊢ ((φ \land l \in ℕ_{0}) \land y \in ℤ) \to y \in ℂ$
180		simplr	$⊢ ((φ \land l \in ℕ_{0}) \land y \in ℤ) \to l \in ℕ_{0}$
181	180	nn0cnd	$⊢ ((φ \land l \in ℕ_{0}) \land y \in ℤ) \to l \in ℂ$
182	177 179 181	mulassd	$⊢ ((φ \land l \in ℕ_{0}) \land y \in ℤ) \to K y l = K y l$
183	179 181	mulcld	$⊢ ((φ \land l \in ℕ_{0}) \land y \in ℤ) \to y l \in ℂ$
184	177 183	mulcomd	$⊢ ((φ \land l \in ℕ_{0}) \land y \in ℤ) \to K y l = y l K$
185	182 184	eqtrd	$⊢ ((φ \land l \in ℕ_{0}) \land y \in ℤ) \to K y l = y l K$
186	185	oveq1d	$⊢ ((φ \land l \in ℕ_{0}) \land y \in ℤ) \to K y l \cdot_{(R ↾_{𝑠} U)} M = y l K \cdot_{(R ↾_{𝑠} U)} M$
187	68	ad2antrr	$⊢ ((φ \land l \in ℕ_{0}) \land y \in ℤ) \to R ↾_{𝑠} U \in Grp$
188	180	nn0zd	$⊢ ((φ \land l \in ℕ_{0}) \land y \in ℤ) \to l \in ℤ$
189	178 188	zmulcld	$⊢ ((φ \land l \in ℕ_{0}) \land y \in ℤ) \to y l \in ℤ$
190	69	ad2antrr	$⊢ ((φ \land l \in ℕ_{0}) \land y \in ℤ) \to K \in ℤ$
191	21	ad2antrr	$⊢ ((φ \land l \in ℕ_{0}) \land y \in ℤ) \to M \in {Base}_{(R ↾_{𝑠} U)}$
192	189 190 191	3jca	$⊢ ((φ \land l \in ℕ_{0}) \land y \in ℤ) \to (y l \in ℤ \land K \in ℤ \land M \in {Base}_{(R ↾_{𝑠} U)})$
193	7 8	mulgass	$⊢ (R ↾_{𝑠} U \in Grp \land (y l \in ℤ \land K \in ℤ \land M \in {Base}_{(R ↾_{𝑠} U)})) \to y l K \cdot_{(R ↾_{𝑠} U)} M = y l \cdot_{(R ↾_{𝑠} U)} (K \cdot_{(R ↾_{𝑠} U)} M)$
194	187 192 193	syl2anc	$⊢ ((φ \land l \in ℕ_{0}) \land y \in ℤ) \to y l K \cdot_{(R ↾_{𝑠} U)} M = y l \cdot_{(R ↾_{𝑠} U)} (K \cdot_{(R ↾_{𝑠} U)} M)$
195	81	ad2antrr	$⊢ ((φ \land l \in ℕ_{0}) \land y \in ℤ) \to K \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)}$
196	195	oveq2d	$⊢ ((φ \land l \in ℕ_{0}) \land y \in ℤ) \to y l \cdot_{(R ↾_{𝑠} U)} (K \cdot_{(R ↾_{𝑠} U)} M) = y l \cdot_{(R ↾_{𝑠} U)} 0_{(R ↾_{𝑠} U)}$
197	7 8 83	mulgz	$⊢ (R ↾_{𝑠} U \in Grp \land y l \in ℤ) \to y l \cdot_{(R ↾_{𝑠} U)} 0_{(R ↾_{𝑠} U)} = 0_{(R ↾_{𝑠} U)}$
198	187 189 197	syl2anc	$⊢ ((φ \land l \in ℕ_{0}) \land y \in ℤ) \to y l \cdot_{(R ↾_{𝑠} U)} 0_{(R ↾_{𝑠} U)} = 0_{(R ↾_{𝑠} U)}$
199	196 198	eqtrd	$⊢ ((φ \land l \in ℕ_{0}) \land y \in ℤ) \to y l \cdot_{(R ↾_{𝑠} U)} (K \cdot_{(R ↾_{𝑠} U)} M) = 0_{(R ↾_{𝑠} U)}$
200	194 199	eqtrd	$⊢ ((φ \land l \in ℕ_{0}) \land y \in ℤ) \to y l K \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)}$
201	186 200	eqtrd	$⊢ ((φ \land l \in ℕ_{0}) \land y \in ℤ) \to K y l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)}$
202	176 201	syl	$⊢ ((((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to K y l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)}$
203	174 202	oveq12d	$⊢ ((((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to (E x l \cdot_{(R ↾_{𝑠} U)} M) +_{(R ↾_{𝑠} U)} (K y l \cdot_{(R ↾_{𝑠} U)} M) = 0_{(R ↾_{𝑠} U)} +_{(R ↾_{𝑠} U)} 0_{(R ↾_{𝑠} U)}$
204	7 83	grpidcl	$⊢ R ↾_{𝑠} U \in Grp \to 0_{(R ↾_{𝑠} U)} \in {Base}_{(R ↾_{𝑠} U)}$
205	123 204	syl	$⊢ ((((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to 0_{(R ↾_{𝑠} U)} \in {Base}_{(R ↾_{𝑠} U)}$
206	7 133 83 123 205	grpridd	$⊢ ((((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to 0_{(R ↾_{𝑠} U)} +_{(R ↾_{𝑠} U)} 0_{(R ↾_{𝑠} U)} = 0_{(R ↾_{𝑠} U)}$
207	203 206	eqtrd	$⊢ ((((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to (E x l \cdot_{(R ↾_{𝑠} U)} M) +_{(R ↾_{𝑠} U)} (K y l \cdot_{(R ↾_{𝑠} U)} M) = 0_{(R ↾_{𝑠} U)}$
208	135 207	eqtrd	$⊢ ((((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to (E x l + K y l) \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)}$
209	122 208	eqtrd	$⊢ ((((φ \land l \in ℕ_{0}) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to (E x + K y) l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)}$
210	110 209	syl	$⊢ (((((φ \land l \in ℕ_{0}) \land (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l)) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \to (E x + K y) l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)}$
211	210	adantr	$⊢ ((((((φ \land l \in ℕ_{0}) \land (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l)) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \land E \gcd K = E x + K y) \to (E x + K y) l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)}$
212	104 211	eqtrd	$⊢ ((((((φ \land l \in ℕ_{0}) \land (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l)) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \land E \gcd K = E x + K y) \to (E \gcd K) l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)}$
213	102 212	eqtrd	$⊢ ((((((φ \land l \in ℕ_{0}) \land (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l)) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \land E \gcd K = E x + K y) \to l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)}$
214		simp-5r	$⊢ ((((((φ \land l \in ℕ_{0}) \land (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l)) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \land E \gcd K = E x + K y) \to (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l)$
215	213 214	mpd	$⊢ ((((((φ \land l \in ℕ_{0}) \land (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l)) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \land x \in ℤ) \land y \in ℤ) \land E \gcd K = E x + K y) \to K ∥ l$
216		bezout	$⊢ (E \in ℤ \land K \in ℤ) \to \exists x \in ℤ \exists y \in ℤ E \gcd K = E x + K y$
217	70 69 216	syl2anc	$⊢ φ \to \exists x \in ℤ \exists y \in ℤ E \gcd K = E x + K y$
218	217	ad3antrrr	$⊢ (((φ \land l \in ℕ_{0}) \land (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l)) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \to \exists x \in ℤ \exists y \in ℤ E \gcd K = E x + K y$
219	215 218	r19.29vva	$⊢ (((φ \land l \in ℕ_{0}) \land (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l)) \land l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)}) \to K ∥ l$
220	219	ex	$⊢ ((φ \land l \in ℕ_{0}) \land (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l)) \to (l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)} \to K ∥ l)$
221	220	ex	$⊢ (φ \land l \in ℕ_{0}) \to ((l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l) \to (l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)} \to K ∥ l))$
222	221	ralimdva	$⊢ φ \to (\forall l \in ℕ_{0} (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l) \to \forall l \in ℕ_{0} (l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)} \to K ∥ l))$
223	91 222	mpd	$⊢ φ \to \forall l \in ℕ_{0} (l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)} \to K ∥ l)$
224	66 90 223	3jca	$⊢ φ \to (E \cdot_{R} M \in {Base}_{(R ↾_{𝑠} U)} \land K \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)} \land \forall l \in ℕ_{0} (l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)} \to K ∥ l))$
225		nnnn0	$⊢ K \in ℕ \to K \in ℕ_{0}$
226	2 225	syl	$⊢ φ \to K \in ℕ_{0}$
227	11 226 8	isprimroot	$⊢ φ \to (E \cdot_{R} M \in ((R ↾_{𝑠} U) PrimRoots K) \leftrightarrow (E \cdot_{R} M \in {Base}_{(R ↾_{𝑠} U)} \land K \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)} \land \forall l \in ℕ_{0} (l \cdot_{(R ↾_{𝑠} U)} (E \cdot_{R} M) = 0_{(R ↾_{𝑠} U)} \to K ∥ l)))$
228	224 227	mpbird	$⊢ φ \to E \cdot_{R} M \in ((R ↾_{𝑠} U) PrimRoots K)$
229	14	eleq2d	$⊢ φ \to (E \cdot_{R} M \in (R PrimRoots K) \leftrightarrow E \cdot_{R} M \in ((R ↾_{𝑠} U) PrimRoots K))$
230	228 229	mpbird	$⊢ φ \to E \cdot_{R} M \in (R PrimRoots K)$

Metamath Proof Explorer

Theorem primrootscoprmpow

Proof