Step |
Hyp |
Ref |
Expression |
1 |
|
uc1pmon1p.c |
⊢ 𝐶 = ( Unic1p ‘ 𝑅 ) |
2 |
|
uc1pmon1p.m |
⊢ 𝑀 = ( Monic1p ‘ 𝑅 ) |
3 |
|
uc1pmon1p.p |
⊢ 𝑃 = ( Poly1 ‘ 𝑅 ) |
4 |
|
uc1pmon1p.t |
⊢ · = ( .r ‘ 𝑃 ) |
5 |
|
uc1pmon1p.a |
⊢ 𝐴 = ( algSc ‘ 𝑃 ) |
6 |
|
uc1pmon1p.d |
⊢ 𝐷 = ( deg1 ‘ 𝑅 ) |
7 |
|
uc1pmon1p.i |
⊢ 𝐼 = ( invr ‘ 𝑅 ) |
8 |
3
|
ply1ring |
⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring ) |
9 |
8
|
adantr |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → 𝑃 ∈ Ring ) |
10 |
|
eqid |
⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) |
11 |
|
eqid |
⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 ) |
12 |
3 5 10 11
|
ply1sclf |
⊢ ( 𝑅 ∈ Ring → 𝐴 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑃 ) ) |
13 |
12
|
adantr |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → 𝐴 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑃 ) ) |
14 |
|
eqid |
⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 ) |
15 |
6 14 1
|
uc1pldg |
⊢ ( 𝑋 ∈ 𝐶 → ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ∈ ( Unit ‘ 𝑅 ) ) |
16 |
14 7 10
|
ringinvcl |
⊢ ( ( 𝑅 ∈ Ring ∧ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ∈ ( Unit ‘ 𝑅 ) ) → ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ∈ ( Base ‘ 𝑅 ) ) |
17 |
15 16
|
sylan2 |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ∈ ( Base ‘ 𝑅 ) ) |
18 |
13 17
|
ffvelrnd |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) ∈ ( Base ‘ 𝑃 ) ) |
19 |
3 11 1
|
uc1pcl |
⊢ ( 𝑋 ∈ 𝐶 → 𝑋 ∈ ( Base ‘ 𝑃 ) ) |
20 |
19
|
adantl |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → 𝑋 ∈ ( Base ‘ 𝑃 ) ) |
21 |
11 4
|
ringcl |
⊢ ( ( 𝑃 ∈ Ring ∧ ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) ∈ ( Base ‘ 𝑃 ) ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ) → ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) |
22 |
9 18 20 21
|
syl3anc |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) |
23 |
|
simpl |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → 𝑅 ∈ Ring ) |
24 |
|
eqid |
⊢ ( RLReg ‘ 𝑅 ) = ( RLReg ‘ 𝑅 ) |
25 |
24 14
|
unitrrg |
⊢ ( 𝑅 ∈ Ring → ( Unit ‘ 𝑅 ) ⊆ ( RLReg ‘ 𝑅 ) ) |
26 |
25
|
adantr |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( Unit ‘ 𝑅 ) ⊆ ( RLReg ‘ 𝑅 ) ) |
27 |
14 7
|
unitinvcl |
⊢ ( ( 𝑅 ∈ Ring ∧ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ∈ ( Unit ‘ 𝑅 ) ) → ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ∈ ( Unit ‘ 𝑅 ) ) |
28 |
15 27
|
sylan2 |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ∈ ( Unit ‘ 𝑅 ) ) |
29 |
26 28
|
sseldd |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ∈ ( RLReg ‘ 𝑅 ) ) |
30 |
6 3 24 11 4 5
|
deg1mul3 |
⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ∈ ( RLReg ‘ 𝑅 ) ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ) → ( 𝐷 ‘ ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ) = ( 𝐷 ‘ 𝑋 ) ) |
31 |
23 29 20 30
|
syl3anc |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( 𝐷 ‘ ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ) = ( 𝐷 ‘ 𝑋 ) ) |
32 |
6 1
|
uc1pdeg |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( 𝐷 ‘ 𝑋 ) ∈ ℕ0 ) |
33 |
31 32
|
eqeltrd |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( 𝐷 ‘ ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ) ∈ ℕ0 ) |
34 |
|
eqid |
⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 ) |
35 |
6 3 34 11
|
deg1nn0clb |
⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) → ( ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ≠ ( 0g ‘ 𝑃 ) ↔ ( 𝐷 ‘ ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ) ∈ ℕ0 ) ) |
36 |
22 35
|
syldan |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ≠ ( 0g ‘ 𝑃 ) ↔ ( 𝐷 ‘ ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ) ∈ ℕ0 ) ) |
37 |
33 36
|
mpbird |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ≠ ( 0g ‘ 𝑃 ) ) |
38 |
31
|
fveq2d |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( ( coe1 ‘ ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ) ‘ ( 𝐷 ‘ ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ) ) = ( ( coe1 ‘ ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) |
39 |
|
eqid |
⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 ) |
40 |
3 11 10 5 4 39
|
coe1sclmul |
⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ) → ( coe1 ‘ ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ) = ( ( ℕ0 × { ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) } ) ∘f ( .r ‘ 𝑅 ) ( coe1 ‘ 𝑋 ) ) ) |
41 |
23 17 20 40
|
syl3anc |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( coe1 ‘ ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ) = ( ( ℕ0 × { ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) } ) ∘f ( .r ‘ 𝑅 ) ( coe1 ‘ 𝑋 ) ) ) |
42 |
41
|
fveq1d |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( ( coe1 ‘ ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ) ‘ ( 𝐷 ‘ 𝑋 ) ) = ( ( ( ℕ0 × { ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) } ) ∘f ( .r ‘ 𝑅 ) ( coe1 ‘ 𝑋 ) ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) |
43 |
|
nn0ex |
⊢ ℕ0 ∈ V |
44 |
43
|
a1i |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ℕ0 ∈ V ) |
45 |
|
fvexd |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ∈ V ) |
46 |
|
eqid |
⊢ ( coe1 ‘ 𝑋 ) = ( coe1 ‘ 𝑋 ) |
47 |
46 11 3 10
|
coe1f |
⊢ ( 𝑋 ∈ ( Base ‘ 𝑃 ) → ( coe1 ‘ 𝑋 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) ) |
48 |
|
ffn |
⊢ ( ( coe1 ‘ 𝑋 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) → ( coe1 ‘ 𝑋 ) Fn ℕ0 ) |
49 |
20 47 48
|
3syl |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( coe1 ‘ 𝑋 ) Fn ℕ0 ) |
50 |
|
eqidd |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ℕ0 ) → ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) = ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) |
51 |
44 45 49 50
|
ofc1 |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ℕ0 ) → ( ( ( ℕ0 × { ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) } ) ∘f ( .r ‘ 𝑅 ) ( coe1 ‘ 𝑋 ) ) ‘ ( 𝐷 ‘ 𝑋 ) ) = ( ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) |
52 |
32 51
|
mpdan |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( ( ( ℕ0 × { ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) } ) ∘f ( .r ‘ 𝑅 ) ( coe1 ‘ 𝑋 ) ) ‘ ( 𝐷 ‘ 𝑋 ) ) = ( ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) |
53 |
|
eqid |
⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 ) |
54 |
14 7 39 53
|
unitlinv |
⊢ ( ( 𝑅 ∈ Ring ∧ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ∈ ( Unit ‘ 𝑅 ) ) → ( ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) = ( 1r ‘ 𝑅 ) ) |
55 |
15 54
|
sylan2 |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) = ( 1r ‘ 𝑅 ) ) |
56 |
52 55
|
eqtrd |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( ( ( ℕ0 × { ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) } ) ∘f ( .r ‘ 𝑅 ) ( coe1 ‘ 𝑋 ) ) ‘ ( 𝐷 ‘ 𝑋 ) ) = ( 1r ‘ 𝑅 ) ) |
57 |
38 42 56
|
3eqtrd |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( ( coe1 ‘ ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ) ‘ ( 𝐷 ‘ ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ) ) = ( 1r ‘ 𝑅 ) ) |
58 |
3 11 34 6 2 53
|
ismon1p |
⊢ ( ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ∈ 𝑀 ↔ ( ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ∈ ( Base ‘ 𝑃 ) ∧ ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ≠ ( 0g ‘ 𝑃 ) ∧ ( ( coe1 ‘ ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ) ‘ ( 𝐷 ‘ ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ) ) = ( 1r ‘ 𝑅 ) ) ) |
59 |
22 37 57 58
|
syl3anbrc |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ∈ 𝑀 ) |