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 22341 |
. . . . . . 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 22348 |
. . . . . 6
⊢ (𝜑 → ((𝑀 · 𝑋) ∈ 𝐵 ∧ ((𝑂‘(𝑀 · 𝑋))‘𝑁) = (𝑀 × 𝑁))) |
| 13 | 12 | simprd 495 |
. . . . 5
⊢ (𝜑 → ((𝑂‘(𝑀 · 𝑋))‘𝑁) = (𝑀 × 𝑁)) |
| 14 | | fta1blem.4 |
. . . . 5
⊢ (𝜑 → (𝑀 × 𝑁) = 𝑊) |
| 15 | 13, 14 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → ((𝑂‘(𝑀 · 𝑋))‘𝑁) = 𝑊) |
| 16 | | eqid 2737 |
. . . . . . 7
⊢ (𝑅 ↑s 𝐾) = (𝑅 ↑s 𝐾) |
| 17 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘(𝑅
↑s 𝐾)) = (Base‘(𝑅 ↑s 𝐾)) |
| 18 | 4 | fvexi 6920 |
. . . . . . . 8
⊢ 𝐾 ∈ V |
| 19 | 18 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ V) |
| 20 | 2, 3, 16, 4 | evl1rhm 22336 |
. . . . . . . . . 10
⊢ (𝑅 ∈ CRing → 𝑂 ∈ (𝑃 RingHom (𝑅 ↑s 𝐾))) |
| 21 | 6, 20 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑂 ∈ (𝑃 RingHom (𝑅 ↑s 𝐾))) |
| 22 | 5, 17 | rhmf 20485 |
. . . . . . . . 9
⊢ (𝑂 ∈ (𝑃 RingHom (𝑅 ↑s 𝐾)) → 𝑂:𝐵⟶(Base‘(𝑅 ↑s 𝐾))) |
| 23 | 21, 22 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑂:𝐵⟶(Base‘(𝑅 ↑s 𝐾))) |
| 24 | 12 | simpld 494 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 · 𝑋) ∈ 𝐵) |
| 25 | 23, 24 | ffvelcdmd 7105 |
. . . . . . 7
⊢ (𝜑 → (𝑂‘(𝑀 · 𝑋)) ∈ (Base‘(𝑅 ↑s 𝐾))) |
| 26 | 16, 4, 17, 6, 19, 25 | pwselbas 17534 |
. . . . . 6
⊢ (𝜑 → (𝑂‘(𝑀 · 𝑋)):𝐾⟶𝐾) |
| 27 | 26 | ffnd 6737 |
. . . . 5
⊢ (𝜑 → (𝑂‘(𝑀 · 𝑋)) Fn 𝐾) |
| 28 | | fniniseg 7080 |
. . . . 5
⊢ ((𝑂‘(𝑀 · 𝑋)) Fn 𝐾 → (𝑁 ∈ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}) ↔ (𝑁 ∈ 𝐾 ∧ ((𝑂‘(𝑀 · 𝑋))‘𝑁) = 𝑊))) |
| 29 | 27, 28 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑁 ∈ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}) ↔ (𝑁 ∈ 𝐾 ∧ ((𝑂‘(𝑀 · 𝑋))‘𝑁) = 𝑊))) |
| 30 | 1, 15, 29 | mpbir2and 713 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) |
| 31 | | fvex 6919 |
. . . . . . . 8
⊢ (𝑂‘(𝑀 · 𝑋)) ∈ V |
| 32 | 31 | cnvex 7947 |
. . . . . . 7
⊢ ◡(𝑂‘(𝑀 · 𝑋)) ∈ V |
| 33 | 32 | imaex 7936 |
. . . . . 6
⊢ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}) ∈ V |
| 34 | 33 | a1i 11 |
. . . . 5
⊢ (𝜑 → (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}) ∈ V) |
| 35 | | 1nn0 12542 |
. . . . . 6
⊢ 1 ∈
ℕ0 |
| 36 | 35 | a1i 11 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℕ0) |
| 37 | | crngring 20242 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
| 38 | 6, 37 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 39 | 7, 3, 5 | vr1cl 22219 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring → 𝑋 ∈ 𝐵) |
| 40 | 38, 39 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
| 41 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(mulGrp‘𝑃) =
(mulGrp‘𝑃) |
| 42 | 41, 5 | mgpbas 20142 |
. . . . . . . . . . . 12
⊢ 𝐵 =
(Base‘(mulGrp‘𝑃)) |
| 43 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(.g‘(mulGrp‘𝑃)) =
(.g‘(mulGrp‘𝑃)) |
| 44 | 42, 43 | mulg1 19099 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ 𝐵 →
(1(.g‘(mulGrp‘𝑃))𝑋) = 𝑋) |
| 45 | 40, 44 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 →
(1(.g‘(mulGrp‘𝑃))𝑋) = 𝑋) |
| 46 | 45 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 ·
(1(.g‘(mulGrp‘𝑃))𝑋)) = (𝑀 · 𝑋)) |
| 47 | | fta1blem.5 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ≠ 𝑊) |
| 48 | | fta1b.w |
. . . . . . . . . . . . 13
⊢ 𝑊 = (0g‘𝑅) |
| 49 | 48, 4, 3, 7, 10, 41, 43 | coe1tmfv1 22277 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾 ∧ 1 ∈ ℕ0) →
((coe1‘(𝑀
·
(1(.g‘(mulGrp‘𝑃))𝑋)))‘1) = 𝑀) |
| 50 | 38, 9, 36, 49 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (𝜑 →
((coe1‘(𝑀
·
(1(.g‘(mulGrp‘𝑃))𝑋)))‘1) = 𝑀) |
| 51 | | fta1b.z |
. . . . . . . . . . . . . . 15
⊢ 0 =
(0g‘𝑃) |
| 52 | 3, 51, 48 | coe1z 22266 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ Ring →
(coe1‘ 0 ) = (ℕ0
× {𝑊})) |
| 53 | 38, 52 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (coe1‘
0 ) =
(ℕ0 × {𝑊})) |
| 54 | 53 | fveq1d 6908 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((coe1‘
0
)‘1) = ((ℕ0 × {𝑊})‘1)) |
| 55 | 48 | fvexi 6920 |
. . . . . . . . . . . . . 14
⊢ 𝑊 ∈ V |
| 56 | 55 | fvconst2 7224 |
. . . . . . . . . . . . 13
⊢ (1 ∈
ℕ0 → ((ℕ0 × {𝑊})‘1) = 𝑊) |
| 57 | 35, 56 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
((ℕ0 × {𝑊})‘1) = 𝑊 |
| 58 | 54, 57 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (𝜑 → ((coe1‘
0
)‘1) = 𝑊) |
| 59 | 47, 50, 58 | 3netr4d 3018 |
. . . . . . . . . 10
⊢ (𝜑 →
((coe1‘(𝑀
·
(1(.g‘(mulGrp‘𝑃))𝑋)))‘1) ≠ ((coe1‘
0
)‘1)) |
| 60 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ ((𝑀 ·
(1(.g‘(mulGrp‘𝑃))𝑋)) = 0 →
(coe1‘(𝑀
·
(1(.g‘(mulGrp‘𝑃))𝑋))) = (coe1‘ 0
)) |
| 61 | 60 | fveq1d 6908 |
. . . . . . . . . . 11
⊢ ((𝑀 ·
(1(.g‘(mulGrp‘𝑃))𝑋)) = 0 →
((coe1‘(𝑀
·
(1(.g‘(mulGrp‘𝑃))𝑋)))‘1) = ((coe1‘
0
)‘1)) |
| 62 | 61 | necon3i 2973 |
. . . . . . . . . 10
⊢
(((coe1‘(𝑀 ·
(1(.g‘(mulGrp‘𝑃))𝑋)))‘1) ≠ ((coe1‘
0
)‘1) → (𝑀 ·
(1(.g‘(mulGrp‘𝑃))𝑋)) ≠ 0 ) |
| 63 | 59, 62 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 ·
(1(.g‘(mulGrp‘𝑃))𝑋)) ≠ 0 ) |
| 64 | 46, 63 | eqnetrrd 3009 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 · 𝑋) ≠ 0 ) |
| 65 | | eldifsn 4786 |
. . . . . . . 8
⊢ ((𝑀 · 𝑋) ∈ (𝐵 ∖ { 0 }) ↔ ((𝑀 · 𝑋) ∈ 𝐵 ∧ (𝑀 · 𝑋) ≠ 0 )) |
| 66 | 24, 64, 65 | sylanbrc 583 |
. . . . . . 7
⊢ (𝜑 → (𝑀 · 𝑋) ∈ (𝐵 ∖ { 0 })) |
| 67 | | fta1blem.6 |
. . . . . . 7
⊢ (𝜑 → ((𝑀 · 𝑋) ∈ (𝐵 ∖ { 0 }) →
(♯‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) ≤ (𝐷‘(𝑀 · 𝑋)))) |
| 68 | 66, 67 | mpd 15 |
. . . . . 6
⊢ (𝜑 → (♯‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) ≤ (𝐷‘(𝑀 · 𝑋))) |
| 69 | 46 | fveq2d 6910 |
. . . . . . 7
⊢ (𝜑 → (𝐷‘(𝑀 ·
(1(.g‘(mulGrp‘𝑃))𝑋))) = (𝐷‘(𝑀 · 𝑋))) |
| 70 | | fta1b.d |
. . . . . . . . 9
⊢ 𝐷 = (deg1‘𝑅) |
| 71 | 70, 4, 3, 7, 10, 41, 43, 48 | deg1tm 26158 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝑀 ∈ 𝐾 ∧ 𝑀 ≠ 𝑊) ∧ 1 ∈ ℕ0) →
(𝐷‘(𝑀 ·
(1(.g‘(mulGrp‘𝑃))𝑋))) = 1) |
| 72 | 38, 9, 47, 36, 71 | syl121anc 1377 |
. . . . . . 7
⊢ (𝜑 → (𝐷‘(𝑀 ·
(1(.g‘(mulGrp‘𝑃))𝑋))) = 1) |
| 73 | 69, 72 | eqtr3d 2779 |
. . . . . 6
⊢ (𝜑 → (𝐷‘(𝑀 · 𝑋)) = 1) |
| 74 | 68, 73 | breqtrd 5169 |
. . . . 5
⊢ (𝜑 → (♯‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) ≤ 1) |
| 75 | | hashbnd 14375 |
. . . . 5
⊢ (((◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}) ∈ V ∧ 1 ∈
ℕ0 ∧ (♯‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) ≤ 1) → (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}) ∈ Fin) |
| 76 | 34, 36, 74, 75 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}) ∈ Fin) |
| 77 | 4, 48 | ring0cl 20264 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑊 ∈ 𝐾) |
| 78 | 38, 77 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ 𝐾) |
| 79 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(algSc‘𝑃) =
(algSc‘𝑃) |
| 80 | 3, 79, 4, 5 | ply1sclf 22288 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring →
(algSc‘𝑃):𝐾⟶𝐵) |
| 81 | 38, 80 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (algSc‘𝑃):𝐾⟶𝐵) |
| 82 | 81, 9 | ffvelcdmd 7105 |
. . . . . . . . . 10
⊢ (𝜑 → ((algSc‘𝑃)‘𝑀) ∈ 𝐵) |
| 83 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(.r‘𝑃) = (.r‘𝑃) |
| 84 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(.r‘(𝑅 ↑s 𝐾)) = (.r‘(𝑅 ↑s 𝐾)) |
| 85 | 5, 83, 84 | rhmmul 20486 |
. . . . . . . . . 10
⊢ ((𝑂 ∈ (𝑃 RingHom (𝑅 ↑s 𝐾)) ∧ ((algSc‘𝑃)‘𝑀) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑂‘(((algSc‘𝑃)‘𝑀)(.r‘𝑃)𝑋)) = ((𝑂‘((algSc‘𝑃)‘𝑀))(.r‘(𝑅 ↑s 𝐾))(𝑂‘𝑋))) |
| 86 | 21, 82, 40, 85 | syl3anc 1373 |
. . . . . . . . 9
⊢ (𝜑 → (𝑂‘(((algSc‘𝑃)‘𝑀)(.r‘𝑃)𝑋)) = ((𝑂‘((algSc‘𝑃)‘𝑀))(.r‘(𝑅 ↑s 𝐾))(𝑂‘𝑋))) |
| 87 | 3 | ply1assa 22201 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ CRing → 𝑃 ∈ AssAlg) |
| 88 | 6, 87 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈ AssAlg) |
| 89 | 3 | ply1sca 22254 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ CRing → 𝑅 = (Scalar‘𝑃)) |
| 90 | 6, 89 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑅 = (Scalar‘𝑃)) |
| 91 | 90 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (Base‘𝑅) =
(Base‘(Scalar‘𝑃))) |
| 92 | 4, 91 | eqtrid 2789 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 = (Base‘(Scalar‘𝑃))) |
| 93 | 9, 92 | eleqtrd 2843 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ (Base‘(Scalar‘𝑃))) |
| 94 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) |
| 95 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃)) |
| 96 | 79, 94, 95, 5, 83, 10 | asclmul1 21906 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ AssAlg ∧ 𝑀 ∈
(Base‘(Scalar‘𝑃)) ∧ 𝑋 ∈ 𝐵) → (((algSc‘𝑃)‘𝑀)(.r‘𝑃)𝑋) = (𝑀 · 𝑋)) |
| 97 | 88, 93, 40, 96 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (𝜑 → (((algSc‘𝑃)‘𝑀)(.r‘𝑃)𝑋) = (𝑀 · 𝑋)) |
| 98 | 97 | fveq2d 6910 |
. . . . . . . . 9
⊢ (𝜑 → (𝑂‘(((algSc‘𝑃)‘𝑀)(.r‘𝑃)𝑋)) = (𝑂‘(𝑀 · 𝑋))) |
| 99 | 23, 82 | ffvelcdmd 7105 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑂‘((algSc‘𝑃)‘𝑀)) ∈ (Base‘(𝑅 ↑s 𝐾))) |
| 100 | 23, 40 | ffvelcdmd 7105 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑂‘𝑋) ∈ (Base‘(𝑅 ↑s 𝐾))) |
| 101 | 16, 17, 6, 19, 99, 100, 11, 84 | pwsmulrval 17536 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑂‘((algSc‘𝑃)‘𝑀))(.r‘(𝑅 ↑s 𝐾))(𝑂‘𝑋)) = ((𝑂‘((algSc‘𝑃)‘𝑀)) ∘f × (𝑂‘𝑋))) |
| 102 | 2, 3, 4, 79 | evl1sca 22338 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐾) → (𝑂‘((algSc‘𝑃)‘𝑀)) = (𝐾 × {𝑀})) |
| 103 | 6, 9, 102 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑂‘((algSc‘𝑃)‘𝑀)) = (𝐾 × {𝑀})) |
| 104 | 2, 7, 4 | evl1var 22340 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ CRing → (𝑂‘𝑋) = ( I ↾ 𝐾)) |
| 105 | 6, 104 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑂‘𝑋) = ( I ↾ 𝐾)) |
| 106 | 103, 105 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑂‘((algSc‘𝑃)‘𝑀)) ∘f × (𝑂‘𝑋)) = ((𝐾 × {𝑀}) ∘f × ( I ↾ 𝐾))) |
| 107 | 101, 106 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑂‘((algSc‘𝑃)‘𝑀))(.r‘(𝑅 ↑s 𝐾))(𝑂‘𝑋)) = ((𝐾 × {𝑀}) ∘f × ( I ↾ 𝐾))) |
| 108 | 86, 98, 107 | 3eqtr3d 2785 |
. . . . . . . 8
⊢ (𝜑 → (𝑂‘(𝑀 · 𝑋)) = ((𝐾 × {𝑀}) ∘f × ( I ↾ 𝐾))) |
| 109 | 108 | fveq1d 6908 |
. . . . . . 7
⊢ (𝜑 → ((𝑂‘(𝑀 · 𝑋))‘𝑊) = (((𝐾 × {𝑀}) ∘f × ( I ↾ 𝐾))‘𝑊)) |
| 110 | | fnconstg 6796 |
. . . . . . . . . 10
⊢ (𝑀 ∈ 𝐾 → (𝐾 × {𝑀}) Fn 𝐾) |
| 111 | 9, 110 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐾 × {𝑀}) Fn 𝐾) |
| 112 | | fnresi 6697 |
. . . . . . . . . 10
⊢ ( I
↾ 𝐾) Fn 𝐾 |
| 113 | 112 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ( I ↾ 𝐾) Fn 𝐾) |
| 114 | | fnfvof 7714 |
. . . . . . . . 9
⊢ ((((𝐾 × {𝑀}) Fn 𝐾 ∧ ( I ↾ 𝐾) Fn 𝐾) ∧ (𝐾 ∈ V ∧ 𝑊 ∈ 𝐾)) → (((𝐾 × {𝑀}) ∘f × ( I ↾ 𝐾))‘𝑊) = (((𝐾 × {𝑀})‘𝑊) × (( I ↾ 𝐾)‘𝑊))) |
| 115 | 111, 113,
19, 78, 114 | syl22anc 839 |
. . . . . . . 8
⊢ (𝜑 → (((𝐾 × {𝑀}) ∘f × ( I ↾ 𝐾))‘𝑊) = (((𝐾 × {𝑀})‘𝑊) × (( I ↾ 𝐾)‘𝑊))) |
| 116 | | fvconst2g 7222 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ 𝐾 ∧ 𝑊 ∈ 𝐾) → ((𝐾 × {𝑀})‘𝑊) = 𝑀) |
| 117 | 9, 78, 116 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐾 × {𝑀})‘𝑊) = 𝑀) |
| 118 | | fvresi 7193 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ 𝐾 → (( I ↾ 𝐾)‘𝑊) = 𝑊) |
| 119 | 78, 118 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (( I ↾ 𝐾)‘𝑊) = 𝑊) |
| 120 | 117, 119 | oveq12d 7449 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐾 × {𝑀})‘𝑊) × (( I ↾ 𝐾)‘𝑊)) = (𝑀 × 𝑊)) |
| 121 | 4, 11, 48 | ringrz 20291 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐾) → (𝑀 × 𝑊) = 𝑊) |
| 122 | 38, 9, 121 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 × 𝑊) = 𝑊) |
| 123 | 120, 122 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝜑 → (((𝐾 × {𝑀})‘𝑊) × (( I ↾ 𝐾)‘𝑊)) = 𝑊) |
| 124 | 115, 123 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → (((𝐾 × {𝑀}) ∘f × ( I ↾ 𝐾))‘𝑊) = 𝑊) |
| 125 | 109, 124 | eqtrd 2777 |
. . . . . 6
⊢ (𝜑 → ((𝑂‘(𝑀 · 𝑋))‘𝑊) = 𝑊) |
| 126 | | fniniseg 7080 |
. . . . . . 7
⊢ ((𝑂‘(𝑀 · 𝑋)) Fn 𝐾 → (𝑊 ∈ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}) ↔ (𝑊 ∈ 𝐾 ∧ ((𝑂‘(𝑀 · 𝑋))‘𝑊) = 𝑊))) |
| 127 | 27, 126 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑊 ∈ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}) ↔ (𝑊 ∈ 𝐾 ∧ ((𝑂‘(𝑀 · 𝑋))‘𝑊) = 𝑊))) |
| 128 | 78, 125, 127 | mpbir2and 713 |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) |
| 129 | 128 | snssd 4809 |
. . . 4
⊢ (𝜑 → {𝑊} ⊆ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) |
| 130 | | hashsng 14408 |
. . . . . . 7
⊢ (𝑊 ∈ 𝐾 → (♯‘{𝑊}) = 1) |
| 131 | 78, 130 | syl 17 |
. . . . . 6
⊢ (𝜑 → (♯‘{𝑊}) = 1) |
| 132 | | ssdomg 9040 |
. . . . . . . . . 10
⊢ ((◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}) ∈ V → ({𝑊} ⊆ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}) → {𝑊} ≼ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}))) |
| 133 | 33, 129, 132 | mpsyl 68 |
. . . . . . . . 9
⊢ (𝜑 → {𝑊} ≼ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) |
| 134 | | snfi 9083 |
. . . . . . . . . 10
⊢ {𝑊} ∈ Fin |
| 135 | | hashdom 14418 |
. . . . . . . . . 10
⊢ (({𝑊} ∈ Fin ∧ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}) ∈ V) → ((♯‘{𝑊}) ≤ (♯‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) ↔ {𝑊} ≼ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}))) |
| 136 | 134, 33, 135 | mp2an 692 |
. . . . . . . . 9
⊢
((♯‘{𝑊})
≤ (♯‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) ↔ {𝑊} ≼ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) |
| 137 | 133, 136 | sylibr 234 |
. . . . . . . 8
⊢ (𝜑 → (♯‘{𝑊}) ≤ (♯‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}))) |
| 138 | 131, 137 | eqbrtrrd 5167 |
. . . . . . 7
⊢ (𝜑 → 1 ≤
(♯‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}))) |
| 139 | | hashcl 14395 |
. . . . . . . . . 10
⊢ ((◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}) ∈ Fin → (♯‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) ∈
ℕ0) |
| 140 | 76, 139 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (♯‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) ∈
ℕ0) |
| 141 | 140 | nn0red 12588 |
. . . . . . . 8
⊢ (𝜑 → (♯‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) ∈ ℝ) |
| 142 | | 1re 11261 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
| 143 | | letri3 11346 |
. . . . . . . 8
⊢
(((♯‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) ∈ ℝ ∧ 1 ∈ ℝ)
→ ((♯‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) = 1 ↔ ((♯‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) ≤ 1 ∧ 1 ≤
(♯‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}))))) |
| 144 | 141, 142,
143 | sylancl 586 |
. . . . . . 7
⊢ (𝜑 → ((♯‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) = 1 ↔ ((♯‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) ≤ 1 ∧ 1 ≤
(♯‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}))))) |
| 145 | 74, 138, 144 | mpbir2and 713 |
. . . . . 6
⊢ (𝜑 → (♯‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) = 1) |
| 146 | 131, 145 | eqtr4d 2780 |
. . . . 5
⊢ (𝜑 → (♯‘{𝑊}) = (♯‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}))) |
| 147 | | hashen 14386 |
. . . . . 6
⊢ (({𝑊} ∈ Fin ∧ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}) ∈ Fin) → ((♯‘{𝑊}) = (♯‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) ↔ {𝑊} ≈ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}))) |
| 148 | 134, 76, 147 | sylancr 587 |
. . . . 5
⊢ (𝜑 → ((♯‘{𝑊}) = (♯‘(◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) ↔ {𝑊} ≈ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}))) |
| 149 | 146, 148 | mpbid 232 |
. . . 4
⊢ (𝜑 → {𝑊} ≈ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) |
| 150 | | fisseneq 9293 |
. . . 4
⊢ (((◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}) ∈ Fin ∧ {𝑊} ⊆ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊}) ∧ {𝑊} ≈ (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) → {𝑊} = (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) |
| 151 | 76, 129, 149, 150 | syl3anc 1373 |
. . 3
⊢ (𝜑 → {𝑊} = (◡(𝑂‘(𝑀 · 𝑋)) “ {𝑊})) |
| 152 | 30, 151 | eleqtrrd 2844 |
. 2
⊢ (𝜑 → 𝑁 ∈ {𝑊}) |
| 153 | | elsni 4643 |
. 2
⊢ (𝑁 ∈ {𝑊} → 𝑁 = 𝑊) |
| 154 | 152, 153 | syl 17 |
1
⊢ (𝜑 → 𝑁 = 𝑊) |