Theorem primrootscoprmpow

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

	Ref	Expression
Hypotheses	primrootscoprmpow.1	⊢ ( 𝜑 → 𝑅 ∈ CMnd )
	primrootscoprmpow.2	⊢ ( 𝜑 → 𝐾 ∈ ℕ )
	primrootscoprmpow.3	⊢ ( 𝜑 → 𝐸 ∈ ℕ )
	primrootscoprmpow.4	⊢ ( 𝜑 → ( 𝐸 gcd 𝐾 ) = 1 )
	primrootscoprmpow.5	⊢ ( 𝜑 → 𝑀 ∈ ( 𝑅 PrimRoots 𝐾 ) )
	primrootscoprmpow.6	⊢ 𝑈 = { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) }
Assertion	primrootscoprmpow	⊢ ( 𝜑 → ( 𝐸 ( .g ‘ 𝑅 ) 𝑀 ) ∈ ( 𝑅 PrimRoots 𝐾 ) )

Proof

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