Proof of Theorem fta1blem
Step | Hyp | Ref
| Expression |
1 | | fta1blem.3 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ 𝐾) |
2 | | fta1b.o |
. . . . . . 7
⊢ 𝑂 = (eval1‘𝑅) |
3 | | fta1b.p |
. . . . . . 7
⊢ 𝑃 = (Poly1‘𝑅) |
4 | | fta1blem.k |
. . . . . . 7
⊢ 𝐾 = (Base‘𝑅) |
5 | | fta1b.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑃) |
6 | | fta1blem.1 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ CRing) |
7 | | fta1blem.x |
. . . . . . . 8
⊢ 𝑋 = (var1‘𝑅) |
8 | 2, 7, 4, 3, 5, 6, 1 | evl1vard 19701 |
. . . . . . 7
⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ ((𝑂‘𝑋)‘𝑁) = 𝑁)) |
9 | | fta1blem.2 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ 𝐾) |
10 | | fta1blem.s |
. . . . . . 7
⊢ · = (
·𝑠 ‘𝑃) |
11 | | fta1blem.t |
. . . . . . 7
⊢ × =
(.r‘𝑅) |
12 | 2, 3, 4, 5, 6, 1, 8, 9, 10, 11 | evl1vsd 19708 |
. . . . . 6
⊢ (𝜑 → ((𝑀 · 𝑋) ∈ 𝐵 ∧ ((𝑂‘(𝑀 · 𝑋))‘𝑁) = (𝑀 × 𝑁))) |
13 | 12 | simprd 479 |
. . . . 5
⊢ (𝜑 → ((𝑂‘(𝑀 · 𝑋))‘𝑁) = (𝑀 × 𝑁)) |
14 | | fta1blem.4 |
. . . . 5
⊢ (𝜑 → (𝑀 × 𝑁) = 𝑊) |
15 | 13, 14 | eqtrd 2656 |
. . . 4
⊢ (𝜑 → ((𝑂‘(𝑀 · 𝑋))‘𝑁) = 𝑊) |
16 | | eqid 2622 |
. . . . . . 7
⊢ (𝑅 ↑s 𝐾) = (𝑅 ↑s 𝐾) |
17 | | eqid 2622 |
. . . . . . 7
⊢
(Base‘(𝑅
↑s 𝐾)) = (Base‘(𝑅 ↑s 𝐾)) |
18 | | fvex 6201 |
. . . . . . . . 9
⊢
(Base‘𝑅)
∈ V |
19 | 4, 18 | eqeltri 2697 |
. . . . . . . 8
⊢ 𝐾 ∈ V |
20 | 19 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ V) |
21 | 2, 3, 16, 4 | evl1rhm 19696 |
. . . . . . . . . 10
⊢ (𝑅 ∈ CRing → 𝑂 ∈ (𝑃 RingHom (𝑅 ↑s 𝐾))) |
22 | 6, 21 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑂 ∈ (𝑃 RingHom (𝑅 ↑s 𝐾))) |
23 | 5, 17 | rhmf 18726 |
. . . . . . . . 9
⊢ (𝑂 ∈ (𝑃 RingHom (𝑅 ↑s 𝐾)) → 𝑂:𝐵⟶(Base‘(𝑅 ↑s 𝐾))) |
24 | 22, 23 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑂:𝐵⟶(Base‘(𝑅 ↑s 𝐾))) |
25 | 12 | simpld 475 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 · 𝑋) ∈ 𝐵) |
26 | 24, 25 | ffvelrnd 6360 |
. . . . . . 7
⊢ (𝜑 → (𝑂‘(𝑀 · 𝑋)) ∈ (Base‘(𝑅 ↑s 𝐾))) |
27 | 16, 4, 17, 6, 20, 26 | pwselbas 16149 |
. . . . . 6
⊢ (𝜑 → (𝑂‘(𝑀 · 𝑋)):𝐾⟶𝐾) |
28 | 27 | ffnd 6046 |
. . . . 5
⊢ (𝜑 → (𝑂‘(𝑀 · 𝑋)) Fn 𝐾) |
29 | | fniniseg 6338 |
. . . . 5
⊢ ((𝑂‘(𝑀 · 𝑋)) Fn 𝐾 → (𝑁 ∈ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}) ↔ (𝑁 ∈ 𝐾 ∧ ((𝑂‘(𝑀 · 𝑋))‘𝑁) = 𝑊))) |
30 | 28, 29 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑁 ∈ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}) ↔ (𝑁 ∈ 𝐾 ∧ ((𝑂‘(𝑀 · 𝑋))‘𝑁) = 𝑊))) |
31 | 1, 15, 30 | mpbir2and 957 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) |
32 | | fvex 6201 |
. . . . . . . 8
⊢ (𝑂‘(𝑀 · 𝑋)) ∈ V |
33 | 32 | cnvex 7113 |
. . . . . . 7
⊢ ◡(𝑂‘(𝑀 · 𝑋)) ∈ V |
34 | 33 | imaex 7104 |
. . . . . 6
⊢ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}) ∈ V |
35 | 34 | a1i 11 |
. . . . 5
⊢ (𝜑 → (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}) ∈ V) |
36 | | 1nn0 11308 |
. . . . . 6
⊢ 1 ∈
ℕ0 |
37 | 36 | a1i 11 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℕ0) |
38 | | crngring 18558 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
39 | 6, 38 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 ∈ Ring) |
40 | 7, 3, 5 | vr1cl 19587 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring → 𝑋 ∈ 𝐵) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
42 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
(mulGrp‘𝑃) =
(mulGrp‘𝑃) |
43 | 42, 5 | mgpbas 18495 |
. . . . . . . . . . . 12
⊢ 𝐵 =
(Base‘(mulGrp‘𝑃)) |
44 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(.g‘(mulGrp‘𝑃)) =
(.g‘(mulGrp‘𝑃)) |
45 | 43, 44 | mulg1 17548 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ 𝐵 →
(1(.g‘(mulGrp‘𝑃))𝑋) = 𝑋) |
46 | 41, 45 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 →
(1(.g‘(mulGrp‘𝑃))𝑋) = 𝑋) |
47 | 46 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 ·
(1(.g‘(mulGrp‘𝑃))𝑋)) = (𝑀 · 𝑋)) |
48 | | fta1blem.5 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ≠ 𝑊) |
49 | | fta1b.w |
. . . . . . . . . . . . 13
⊢ 𝑊 = (0g‘𝑅) |
50 | 49, 4, 3, 7, 10, 42, 44 | coe1tmfv1 19644 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ∧ 1 ∈ ℕ0) →
((coe1‘(𝑀
·
(1(.g‘(mulGrp‘𝑃))𝑋)))‘1) = 𝑀) |
51 | 39, 9, 37, 50 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (𝜑 →
((coe1‘(𝑀
·
(1(.g‘(mulGrp‘𝑃))𝑋)))‘1) = 𝑀) |
52 | | fta1b.z |
. . . . . . . . . . . . . . 15
⊢ 0 =
(0g‘𝑃) |
53 | 3, 52, 49 | coe1z 19633 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ Ring →
(coe1‘ 0 ) = (ℕ0
× {𝑊})) |
54 | 39, 53 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (coe1‘
0 ) =
(ℕ0 × {𝑊})) |
55 | 54 | fveq1d 6193 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((coe1‘
0
)‘1) = ((ℕ0 × {𝑊})‘1)) |
56 | | fvex 6201 |
. . . . . . . . . . . . . . 15
⊢
(0g‘𝑅) ∈ V |
57 | 49, 56 | eqeltri 2697 |
. . . . . . . . . . . . . 14
⊢ 𝑊 ∈ V |
58 | 57 | fvconst2 6469 |
. . . . . . . . . . . . 13
⊢ (1 ∈
ℕ0 → ((ℕ0 × {𝑊})‘1) = 𝑊) |
59 | 36, 58 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
((ℕ0 × {𝑊})‘1) = 𝑊 |
60 | 55, 59 | syl6eq 2672 |
. . . . . . . . . . 11
⊢ (𝜑 → ((coe1‘
0
)‘1) = 𝑊) |
61 | 48, 51, 60 | 3netr4d 2871 |
. . . . . . . . . 10
⊢ (𝜑 →
((coe1‘(𝑀
·
(1(.g‘(mulGrp‘𝑃))𝑋)))‘1) ≠ ((coe1‘
0
)‘1)) |
62 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ ((𝑀 ·
(1(.g‘(mulGrp‘𝑃))𝑋)) = 0 →
(coe1‘(𝑀
·
(1(.g‘(mulGrp‘𝑃))𝑋))) = (coe1‘ 0
)) |
63 | 62 | fveq1d 6193 |
. . . . . . . . . . 11
⊢ ((𝑀 ·
(1(.g‘(mulGrp‘𝑃))𝑋)) = 0 →
((coe1‘(𝑀
·
(1(.g‘(mulGrp‘𝑃))𝑋)))‘1) = ((coe1‘
0
)‘1)) |
64 | 63 | necon3i 2826 |
. . . . . . . . . 10
⊢
(((coe1‘(𝑀 ·
(1(.g‘(mulGrp‘𝑃))𝑋)))‘1) ≠ ((coe1‘
0
)‘1) → (𝑀 ·
(1(.g‘(mulGrp‘𝑃))𝑋)) ≠ 0 ) |
65 | 61, 64 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 ·
(1(.g‘(mulGrp‘𝑃))𝑋)) ≠ 0 ) |
66 | 47, 65 | eqnetrrd 2862 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 · 𝑋) ≠ 0 ) |
67 | | eldifsn 4317 |
. . . . . . . 8
⊢ ((𝑀 · 𝑋) ∈ (𝐵 ∖ { 0 }) ↔ ((𝑀 · 𝑋) ∈ 𝐵 ∧ (𝑀 · 𝑋) ≠ 0 )) |
68 | 25, 66, 67 | sylanbrc 698 |
. . . . . . 7
⊢ (𝜑 → (𝑀 · 𝑋) ∈ (𝐵 ∖ { 0 })) |
69 | | fta1blem.6 |
. . . . . . 7
⊢ (𝜑 → ((𝑀 · 𝑋) ∈ (𝐵 ∖ { 0 }) → (#‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) ≤ (𝐷‘(𝑀 · 𝑋)))) |
70 | 68, 69 | mpd 15 |
. . . . . 6
⊢ (𝜑 → (#‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) ≤ (𝐷‘(𝑀 · 𝑋))) |
71 | 47 | fveq2d 6195 |
. . . . . . 7
⊢ (𝜑 → (𝐷‘(𝑀 ·
(1(.g‘(mulGrp‘𝑃))𝑋))) = (𝐷‘(𝑀 · 𝑋))) |
72 | | fta1b.d |
. . . . . . . . 9
⊢ 𝐷 = ( deg1
‘𝑅) |
73 | 72, 4, 3, 7, 10, 42, 44, 49 | deg1tm 23878 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝑀 ∈ 𝐾 ∧ 𝑀 ≠ 𝑊) ∧ 1 ∈ ℕ0) →
(𝐷‘(𝑀 ·
(1(.g‘(mulGrp‘𝑃))𝑋))) = 1) |
74 | 39, 9, 48, 37, 73 | syl121anc 1331 |
. . . . . . 7
⊢ (𝜑 → (𝐷‘(𝑀 ·
(1(.g‘(mulGrp‘𝑃))𝑋))) = 1) |
75 | 71, 74 | eqtr3d 2658 |
. . . . . 6
⊢ (𝜑 → (𝐷‘(𝑀 · 𝑋)) = 1) |
76 | 70, 75 | breqtrd 4679 |
. . . . 5
⊢ (𝜑 → (#‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) ≤ 1) |
77 | | hashbnd 13123 |
. . . . 5
⊢ (((◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}) ∈ V ∧ 1 ∈
ℕ0 ∧ (#‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) ≤ 1) → (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}) ∈ Fin) |
78 | 35, 37, 76, 77 | syl3anc 1326 |
. . . 4
⊢ (𝜑 → (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}) ∈ Fin) |
79 | 4, 49 | ring0cl 18569 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑊 ∈ 𝐾) |
80 | 39, 79 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ 𝐾) |
81 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
(algSc‘𝑃) =
(algSc‘𝑃) |
82 | 3, 81, 4, 5 | ply1sclf 19655 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring →
(algSc‘𝑃):𝐾⟶𝐵) |
83 | 39, 82 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (algSc‘𝑃):𝐾⟶𝐵) |
84 | 83, 9 | ffvelrnd 6360 |
. . . . . . . . . 10
⊢ (𝜑 → ((algSc‘𝑃)‘𝑀) ∈ 𝐵) |
85 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(.r‘𝑃) = (.r‘𝑃) |
86 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(.r‘(𝑅 ↑s 𝐾)) = (.r‘(𝑅 ↑s 𝐾)) |
87 | 5, 85, 86 | rhmmul 18727 |
. . . . . . . . . 10
⊢ ((𝑂 ∈ (𝑃 RingHom (𝑅 ↑s 𝐾)) ∧ ((algSc‘𝑃)‘𝑀) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑂‘(((algSc‘𝑃)‘𝑀)(.r‘𝑃)𝑋)) = ((𝑂‘((algSc‘𝑃)‘𝑀))(.r‘(𝑅 ↑s 𝐾))(𝑂‘𝑋))) |
88 | 22, 84, 41, 87 | syl3anc 1326 |
. . . . . . . . 9
⊢ (𝜑 → (𝑂‘(((algSc‘𝑃)‘𝑀)(.r‘𝑃)𝑋)) = ((𝑂‘((algSc‘𝑃)‘𝑀))(.r‘(𝑅 ↑s 𝐾))(𝑂‘𝑋))) |
89 | 3 | ply1assa 19569 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ CRing → 𝑃 ∈ AssAlg) |
90 | 6, 89 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈ AssAlg) |
91 | 3 | ply1sca 19623 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ CRing → 𝑅 = (Scalar‘𝑃)) |
92 | 6, 91 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑅 = (Scalar‘𝑃)) |
93 | 92 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (Base‘𝑅) =
(Base‘(Scalar‘𝑃))) |
94 | 4, 93 | syl5eq 2668 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 = (Base‘(Scalar‘𝑃))) |
95 | 9, 94 | eleqtrd 2703 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ (Base‘(Scalar‘𝑃))) |
96 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) |
97 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃)) |
98 | 81, 96, 97, 5, 85, 10 | asclmul1 19339 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ AssAlg ∧ 𝑀 ∈
(Base‘(Scalar‘𝑃)) ∧ 𝑋 ∈ 𝐵) → (((algSc‘𝑃)‘𝑀)(.r‘𝑃)𝑋) = (𝑀 · 𝑋)) |
99 | 90, 95, 41, 98 | syl3anc 1326 |
. . . . . . . . . 10
⊢ (𝜑 → (((algSc‘𝑃)‘𝑀)(.r‘𝑃)𝑋) = (𝑀 · 𝑋)) |
100 | 99 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝜑 → (𝑂‘(((algSc‘𝑃)‘𝑀)(.r‘𝑃)𝑋)) = (𝑂‘(𝑀 · 𝑋))) |
101 | 24, 84 | ffvelrnd 6360 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑂‘((algSc‘𝑃)‘𝑀)) ∈ (Base‘(𝑅 ↑s 𝐾))) |
102 | 24, 41 | ffvelrnd 6360 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑂‘𝑋) ∈ (Base‘(𝑅 ↑s 𝐾))) |
103 | 16, 17, 6, 20, 101, 102, 11, 86 | pwsmulrval 16151 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑂‘((algSc‘𝑃)‘𝑀))(.r‘(𝑅 ↑s 𝐾))(𝑂‘𝑋)) = ((𝑂‘((algSc‘𝑃)‘𝑀)) ∘𝑓 × (𝑂‘𝑋))) |
104 | 2, 3, 4, 81 | evl1sca 19698 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐾) → (𝑂‘((algSc‘𝑃)‘𝑀)) = (𝐾 × {𝑀})) |
105 | 6, 9, 104 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑂‘((algSc‘𝑃)‘𝑀)) = (𝐾 × {𝑀})) |
106 | 2, 7, 4 | evl1var 19700 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ CRing → (𝑂‘𝑋) = ( I ↾ 𝐾)) |
107 | 6, 106 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑂‘𝑋) = ( I ↾ 𝐾)) |
108 | 105, 107 | oveq12d 6668 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑂‘((algSc‘𝑃)‘𝑀)) ∘𝑓 × (𝑂‘𝑋)) = ((𝐾 × {𝑀}) ∘𝑓 × ( I
↾ 𝐾))) |
109 | 103, 108 | eqtrd 2656 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑂‘((algSc‘𝑃)‘𝑀))(.r‘(𝑅 ↑s 𝐾))(𝑂‘𝑋)) = ((𝐾 × {𝑀}) ∘𝑓 × ( I
↾ 𝐾))) |
110 | 88, 100, 109 | 3eqtr3d 2664 |
. . . . . . . 8
⊢ (𝜑 → (𝑂‘(𝑀 · 𝑋)) = ((𝐾 × {𝑀}) ∘𝑓 × ( I
↾ 𝐾))) |
111 | 110 | fveq1d 6193 |
. . . . . . 7
⊢ (𝜑 → ((𝑂‘(𝑀 · 𝑋))‘𝑊) = (((𝐾 × {𝑀}) ∘𝑓 × ( I
↾ 𝐾))‘𝑊)) |
112 | | fnconstg 6093 |
. . . . . . . . . 10
⊢ (𝑀 ∈ 𝐾 → (𝐾 × {𝑀}) Fn 𝐾) |
113 | 9, 112 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐾 × {𝑀}) Fn 𝐾) |
114 | | fnresi 6008 |
. . . . . . . . . 10
⊢ ( I
↾ 𝐾) Fn 𝐾 |
115 | 114 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ( I ↾ 𝐾) Fn 𝐾) |
116 | | fnfvof 6911 |
. . . . . . . . 9
⊢ ((((𝐾 × {𝑀}) Fn 𝐾 ∧ ( I ↾ 𝐾) Fn 𝐾) ∧ (𝐾 ∈ V ∧ 𝑊 ∈ 𝐾)) → (((𝐾 × {𝑀}) ∘𝑓 × ( I
↾ 𝐾))‘𝑊) = (((𝐾 × {𝑀})‘𝑊) × (( I ↾ 𝐾)‘𝑊))) |
117 | 113, 115,
20, 80, 116 | syl22anc 1327 |
. . . . . . . 8
⊢ (𝜑 → (((𝐾 × {𝑀}) ∘𝑓 × ( I
↾ 𝐾))‘𝑊) = (((𝐾 × {𝑀})‘𝑊) × (( I ↾ 𝐾)‘𝑊))) |
118 | | fvconst2g 6467 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ 𝐾 ∧ 𝑊 ∈ 𝐾) → ((𝐾 × {𝑀})‘𝑊) = 𝑀) |
119 | 9, 80, 118 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐾 × {𝑀})‘𝑊) = 𝑀) |
120 | | fvresi 6439 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ 𝐾 → (( I ↾ 𝐾)‘𝑊) = 𝑊) |
121 | 80, 120 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (( I ↾ 𝐾)‘𝑊) = 𝑊) |
122 | 119, 121 | oveq12d 6668 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐾 × {𝑀})‘𝑊) × (( I ↾ 𝐾)‘𝑊)) = (𝑀 × 𝑊)) |
123 | 4, 11, 49 | ringrz 18588 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾) → (𝑀 × 𝑊) = 𝑊) |
124 | 39, 9, 123 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 × 𝑊) = 𝑊) |
125 | 122, 124 | eqtrd 2656 |
. . . . . . . 8
⊢ (𝜑 → (((𝐾 × {𝑀})‘𝑊) × (( I ↾ 𝐾)‘𝑊)) = 𝑊) |
126 | 117, 125 | eqtrd 2656 |
. . . . . . 7
⊢ (𝜑 → (((𝐾 × {𝑀}) ∘𝑓 × ( I
↾ 𝐾))‘𝑊) = 𝑊) |
127 | 111, 126 | eqtrd 2656 |
. . . . . 6
⊢ (𝜑 → ((𝑂‘(𝑀 · 𝑋))‘𝑊) = 𝑊) |
128 | | fniniseg 6338 |
. . . . . . 7
⊢ ((𝑂‘(𝑀 · 𝑋)) Fn 𝐾 → (𝑊 ∈ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}) ↔ (𝑊 ∈ 𝐾 ∧ ((𝑂‘(𝑀 · 𝑋))‘𝑊) = 𝑊))) |
129 | 28, 128 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑊 ∈ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}) ↔ (𝑊 ∈ 𝐾 ∧ ((𝑂‘(𝑀 · 𝑋))‘𝑊) = 𝑊))) |
130 | 80, 127, 129 | mpbir2and 957 |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) |
131 | 130 | snssd 4340 |
. . . 4
⊢ (𝜑 → {𝑊} ⊆ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) |
132 | | hashsng 13159 |
. . . . . . 7
⊢ (𝑊 ∈ 𝐾 → (#‘{𝑊}) = 1) |
133 | 80, 132 | syl 17 |
. . . . . 6
⊢ (𝜑 → (#‘{𝑊}) = 1) |
134 | | ssdomg 8001 |
. . . . . . . . . 10
⊢ ((◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}) ∈ V → ({𝑊} ⊆ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}) → {𝑊} ≼ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}))) |
135 | 34, 131, 134 | mpsyl 68 |
. . . . . . . . 9
⊢ (𝜑 → {𝑊} ≼ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) |
136 | | snfi 8038 |
. . . . . . . . . 10
⊢ {𝑊} ∈ Fin |
137 | | hashdom 13168 |
. . . . . . . . . 10
⊢ (({𝑊} ∈ Fin ∧ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}) ∈ V) → ((#‘{𝑊}) ≤ (#‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) ↔ {𝑊} ≼ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}))) |
138 | 136, 34, 137 | mp2an 708 |
. . . . . . . . 9
⊢
((#‘{𝑊}) ≤
(#‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) ↔ {𝑊} ≼ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) |
139 | 135, 138 | sylibr 224 |
. . . . . . . 8
⊢ (𝜑 → (#‘{𝑊}) ≤ (#‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}))) |
140 | 133, 139 | eqbrtrrd 4677 |
. . . . . . 7
⊢ (𝜑 → 1 ≤ (#‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}))) |
141 | | hashcl 13147 |
. . . . . . . . . 10
⊢ ((◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}) ∈ Fin → (#‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) ∈
ℕ0) |
142 | 78, 141 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (#‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) ∈
ℕ0) |
143 | 142 | nn0red 11352 |
. . . . . . . 8
⊢ (𝜑 → (#‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) ∈ ℝ) |
144 | | 1re 10039 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
145 | | letri3 10123 |
. . . . . . . 8
⊢
(((#‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) ∈ ℝ ∧ 1 ∈ ℝ)
→ ((#‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) = 1 ↔ ((#‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) ≤ 1 ∧ 1 ≤ (#‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}))))) |
146 | 143, 144,
145 | sylancl 694 |
. . . . . . 7
⊢ (𝜑 → ((#‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) = 1 ↔ ((#‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) ≤ 1 ∧ 1 ≤ (#‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}))))) |
147 | 76, 140, 146 | mpbir2and 957 |
. . . . . 6
⊢ (𝜑 → (#‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) = 1) |
148 | 133, 147 | eqtr4d 2659 |
. . . . 5
⊢ (𝜑 → (#‘{𝑊}) = (#‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}))) |
149 | | hashen 13135 |
. . . . . 6
⊢ (({𝑊} ∈ Fin ∧ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}) ∈ Fin) → ((#‘{𝑊}) = (#‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) ↔ {𝑊} ≈ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}))) |
150 | 136, 78, 149 | sylancr 695 |
. . . . 5
⊢ (𝜑 → ((#‘{𝑊}) = (#‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) ↔ {𝑊} ≈ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}))) |
151 | 148, 150 | mpbid 222 |
. . . 4
⊢ (𝜑 → {𝑊} ≈ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) |
152 | | fisseneq 8171 |
. . . 4
⊢ (((◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}) ∈ Fin ∧ {𝑊} ⊆ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}) ∧ {𝑊} ≈ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) → {𝑊} = (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) |
153 | 78, 131, 151, 152 | syl3anc 1326 |
. . 3
⊢ (𝜑 → {𝑊} = (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) |
154 | 31, 153 | eleqtrrd 2704 |
. 2
⊢ (𝜑 → 𝑁 ∈ {𝑊}) |
155 | | elsni 4194 |
. 2
⊢ (𝑁 ∈ {𝑊} → 𝑁 = 𝑊) |
156 | 154, 155 | syl 17 |
1
⊢ (𝜑 → 𝑁 = 𝑊) |