| Step | Hyp | Ref
| Expression |
| 1 | | prjspner01.e |
. . . 4
⊢ ∼ =
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝑆 𝑥 = (𝑙 · 𝑦))} |
| 2 | 1 | prjsprel 42614 |
. . 3
⊢ (𝑋 ∼ 𝑌 ↔ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ∃𝑚 ∈ 𝑆 𝑋 = (𝑚 · 𝑌))) |
| 3 | | prjspner1.1 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋‘0) ≠ 0 ) |
| 4 | | fveq1 6905 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 = (0g‘𝑊) → (𝑋‘0) = ((0g‘𝑊)‘0)) |
| 5 | | prjspner01.w |
. . . . . . . . . . . . . . . 16
⊢ 𝑊 = (𝐾 freeLMod (0...𝑁)) |
| 6 | | prjspner01.0 |
. . . . . . . . . . . . . . . 16
⊢ 0 =
(0g‘𝐾) |
| 7 | | prjspner01.k |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐾 ∈ DivRing) |
| 8 | 7 | drngringd 20737 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐾 ∈ Ring) |
| 9 | | ovexd 7466 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (0...𝑁) ∈ V) |
| 10 | | prjspner01.n |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 11 | | 0elfz 13664 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ0
→ 0 ∈ (0...𝑁)) |
| 12 | 10, 11 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 ∈ (0...𝑁)) |
| 13 | 5, 6, 8, 9, 12 | frlm0vald 42549 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 →
((0g‘𝑊)‘0) = 0 ) |
| 14 | 4, 13 | sylan9eqr 2799 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑋 = (0g‘𝑊)) → (𝑋‘0) = 0 ) |
| 15 | 3, 14 | mteqand 3033 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 ≠ (0g‘𝑊)) |
| 16 | 5 | frlmsca 21773 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐾 ∈ DivRing ∧ (0...𝑁) ∈ V) → 𝐾 = (Scalar‘𝑊)) |
| 17 | 7, 9, 16 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐾 = (Scalar‘𝑊)) |
| 18 | 17 | fveq2d 6910 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (0g‘𝐾) =
(0g‘(Scalar‘𝑊))) |
| 19 | 6, 18 | eqtrid 2789 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 =
(0g‘(Scalar‘𝑊))) |
| 20 | 19 | oveq1d 7446 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ( 0 · 𝑌) =
((0g‘(Scalar‘𝑊)) · 𝑌)) |
| 21 | 5 | frlmlvec 21781 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐾 ∈ DivRing ∧ (0...𝑁) ∈ V) → 𝑊 ∈ LVec) |
| 22 | 7, 9, 21 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑊 ∈ LVec) |
| 23 | 22 | lveclmodd 21106 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑊 ∈ LMod) |
| 24 | | prjspner1.y |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
| 25 | | prjspner01.b |
. . . . . . . . . . . . . . . . 17
⊢ 𝐵 = ((Base‘𝑊) ∖
{(0g‘𝑊)}) |
| 26 | 24, 25 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑌 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)})) |
| 27 | 26 | eldifad 3963 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑌 ∈ (Base‘𝑊)) |
| 28 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(Base‘𝑊) =
(Base‘𝑊) |
| 29 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
| 30 | | prjspner01.t |
. . . . . . . . . . . . . . . 16
⊢ · = (
·𝑠 ‘𝑊) |
| 31 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(0g‘(Scalar‘𝑊)) =
(0g‘(Scalar‘𝑊)) |
| 32 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(0g‘𝑊) = (0g‘𝑊) |
| 33 | 28, 29, 30, 31, 32 | lmod0vs 20893 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ (Base‘𝑊)) →
((0g‘(Scalar‘𝑊)) · 𝑌) = (0g‘𝑊)) |
| 34 | 23, 27, 33 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
((0g‘(Scalar‘𝑊)) · 𝑌) = (0g‘𝑊)) |
| 35 | 20, 34 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ( 0 · 𝑌) = (0g‘𝑊)) |
| 36 | 15, 35 | neeqtrrd 3015 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ≠ ( 0 · 𝑌)) |
| 37 | 36 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) → 𝑋 ≠ ( 0 · 𝑌)) |
| 38 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑚 = 0 → (𝑚 · 𝑌) = ( 0 · 𝑌)) |
| 39 | 38 | neeq2d 3001 |
. . . . . . . . . . 11
⊢ (𝑚 = 0 → (𝑋 ≠ (𝑚 · 𝑌) ↔ 𝑋 ≠ ( 0 · 𝑌))) |
| 40 | 37, 39 | syl5ibrcom 247 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) → (𝑚 = 0 → 𝑋 ≠ (𝑚 · 𝑌))) |
| 41 | 40 | necon2d 2963 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) → (𝑋 = (𝑚 · 𝑌) → 𝑚 ≠ 0 )) |
| 42 | 41 | ancrd 551 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) → (𝑋 = (𝑚 · 𝑌) → (𝑚 ≠ 0 ∧ 𝑋 = (𝑚 · 𝑌)))) |
| 43 | | prjspner01.s |
. . . . . . . . . . . . . . 15
⊢ 𝑆 = (Base‘𝐾) |
| 44 | | ovexd 7466 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) ∧ 𝑚 ≠ 0 ) → (0...𝑁) ∈ V) |
| 45 | | simplr 769 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) ∧ 𝑚 ≠ 0 ) → 𝑚 ∈ 𝑆) |
| 46 | 27 | ad3antrrr 730 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) ∧ 𝑚 ≠ 0 ) → 𝑌 ∈ (Base‘𝑊)) |
| 47 | 12 | ad3antrrr 730 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) ∧ 𝑚 ≠ 0 ) → 0 ∈
(0...𝑁)) |
| 48 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
(.r‘𝐾) = (.r‘𝐾) |
| 49 | 5, 28, 43, 44, 45, 46, 47, 30, 48 | frlmvscaval 21788 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) ∧ 𝑚 ≠ 0 ) → ((𝑚 · 𝑌)‘0) = (𝑚(.r‘𝐾)(𝑌‘0))) |
| 50 | 49 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) ∧ 𝑚 ≠ 0 ) → (𝐼‘((𝑚 · 𝑌)‘0)) = (𝐼‘(𝑚(.r‘𝐾)(𝑌‘0)))) |
| 51 | | prjspner01.i |
. . . . . . . . . . . . . 14
⊢ 𝐼 = (invr‘𝐾) |
| 52 | 7 | ad3antrrr 730 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) ∧ 𝑚 ≠ 0 ) → 𝐾 ∈ DivRing) |
| 53 | 5, 43, 28 | frlmbasf 21780 |
. . . . . . . . . . . . . . . . 17
⊢
(((0...𝑁) ∈ V
∧ 𝑌 ∈
(Base‘𝑊)) →
𝑌:(0...𝑁)⟶𝑆) |
| 54 | 9, 27, 53 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑌:(0...𝑁)⟶𝑆) |
| 55 | 54, 12 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑌‘0) ∈ 𝑆) |
| 56 | 55 | ad3antrrr 730 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) ∧ 𝑚 ≠ 0 ) → (𝑌‘0) ∈ 𝑆) |
| 57 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) ∧ 𝑚 ≠ 0 ) → 𝑚 ≠ 0 ) |
| 58 | | prjspner1.2 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑌‘0) ≠ 0 ) |
| 59 | 58 | ad3antrrr 730 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) ∧ 𝑚 ≠ 0 ) → (𝑌‘0) ≠ 0
) |
| 60 | 43, 6, 48, 51, 52, 45, 56, 57, 59 | drnginvmuld 42537 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) ∧ 𝑚 ≠ 0 ) → (𝐼‘(𝑚(.r‘𝐾)(𝑌‘0))) = ((𝐼‘(𝑌‘0))(.r‘𝐾)(𝐼‘𝑚))) |
| 61 | 50, 60 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) ∧ 𝑚 ≠ 0 ) → (𝐼‘((𝑚 · 𝑌)‘0)) = ((𝐼‘(𝑌‘0))(.r‘𝐾)(𝐼‘𝑚))) |
| 62 | 61 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) ∧ 𝑚 ≠ 0 ) → ((𝐼‘((𝑚 · 𝑌)‘0)) · (𝑚 · 𝑌)) = (((𝐼‘(𝑌‘0))(.r‘𝐾)(𝐼‘𝑚)) · (𝑚 · 𝑌))) |
| 63 | 23 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) ∧ 𝑚 ≠ 0 ) → 𝑊 ∈ LMod) |
| 64 | 8 | ad3antrrr 730 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) ∧ 𝑚 ≠ 0 ) → 𝐾 ∈ Ring) |
| 65 | 43, 6, 51, 52, 56, 59 | drnginvrcld 20755 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) ∧ 𝑚 ≠ 0 ) → (𝐼‘(𝑌‘0)) ∈ 𝑆) |
| 66 | 43, 6, 51, 52, 45, 57 | drnginvrcld 20755 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) ∧ 𝑚 ≠ 0 ) → (𝐼‘𝑚) ∈ 𝑆) |
| 67 | 43, 48, 64, 65, 66 | ringcld 20257 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) ∧ 𝑚 ≠ 0 ) → ((𝐼‘(𝑌‘0))(.r‘𝐾)(𝐼‘𝑚)) ∈ 𝑆) |
| 68 | 17 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (Base‘𝐾) =
(Base‘(Scalar‘𝑊))) |
| 69 | 43, 68 | eqtrid 2789 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 = (Base‘(Scalar‘𝑊))) |
| 70 | 69 | ad3antrrr 730 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) ∧ 𝑚 ≠ 0 ) → 𝑆 = (Base‘(Scalar‘𝑊))) |
| 71 | 67, 70 | eleqtrd 2843 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) ∧ 𝑚 ≠ 0 ) → ((𝐼‘(𝑌‘0))(.r‘𝐾)(𝐼‘𝑚)) ∈ (Base‘(Scalar‘𝑊))) |
| 72 | 45, 70 | eleqtrd 2843 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) ∧ 𝑚 ≠ 0 ) → 𝑚 ∈
(Base‘(Scalar‘𝑊))) |
| 73 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
| 74 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(.r‘(Scalar‘𝑊)) =
(.r‘(Scalar‘𝑊)) |
| 75 | 28, 29, 30, 73, 74 | lmodvsass 20885 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ (((𝐼‘(𝑌‘0))(.r‘𝐾)(𝐼‘𝑚)) ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑚 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑌 ∈ (Base‘𝑊))) → ((((𝐼‘(𝑌‘0))(.r‘𝐾)(𝐼‘𝑚))(.r‘(Scalar‘𝑊))𝑚) · 𝑌) = (((𝐼‘(𝑌‘0))(.r‘𝐾)(𝐼‘𝑚)) · (𝑚 · 𝑌))) |
| 76 | 63, 71, 72, 46, 75 | syl13anc 1374 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) ∧ 𝑚 ≠ 0 ) → ((((𝐼‘(𝑌‘0))(.r‘𝐾)(𝐼‘𝑚))(.r‘(Scalar‘𝑊))𝑚) · 𝑌) = (((𝐼‘(𝑌‘0))(.r‘𝐾)(𝐼‘𝑚)) · (𝑚 · 𝑌))) |
| 77 | 43, 48, 64, 65, 66, 45 | ringassd 20254 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) ∧ 𝑚 ≠ 0 ) → (((𝐼‘(𝑌‘0))(.r‘𝐾)(𝐼‘𝑚))(.r‘𝐾)𝑚) = ((𝐼‘(𝑌‘0))(.r‘𝐾)((𝐼‘𝑚)(.r‘𝐾)𝑚))) |
| 78 | 52, 44, 16 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) ∧ 𝑚 ≠ 0 ) → 𝐾 = (Scalar‘𝑊)) |
| 79 | 78 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) ∧ 𝑚 ≠ 0 ) →
(.r‘𝐾) =
(.r‘(Scalar‘𝑊))) |
| 80 | 79 | oveqd 7448 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) ∧ 𝑚 ≠ 0 ) → (((𝐼‘(𝑌‘0))(.r‘𝐾)(𝐼‘𝑚))(.r‘𝐾)𝑚) = (((𝐼‘(𝑌‘0))(.r‘𝐾)(𝐼‘𝑚))(.r‘(Scalar‘𝑊))𝑚)) |
| 81 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(1r‘𝐾) = (1r‘𝐾) |
| 82 | 43, 6, 48, 81, 51, 52, 45, 57 | drnginvrld 20758 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) ∧ 𝑚 ≠ 0 ) → ((𝐼‘𝑚)(.r‘𝐾)𝑚) = (1r‘𝐾)) |
| 83 | 82 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) ∧ 𝑚 ≠ 0 ) → ((𝐼‘(𝑌‘0))(.r‘𝐾)((𝐼‘𝑚)(.r‘𝐾)𝑚)) = ((𝐼‘(𝑌‘0))(.r‘𝐾)(1r‘𝐾))) |
| 84 | 43, 48, 81, 64, 65 | ringridmd 20270 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) ∧ 𝑚 ≠ 0 ) → ((𝐼‘(𝑌‘0))(.r‘𝐾)(1r‘𝐾)) = (𝐼‘(𝑌‘0))) |
| 85 | 83, 84 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) ∧ 𝑚 ≠ 0 ) → ((𝐼‘(𝑌‘0))(.r‘𝐾)((𝐼‘𝑚)(.r‘𝐾)𝑚)) = (𝐼‘(𝑌‘0))) |
| 86 | 77, 80, 85 | 3eqtr3d 2785 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) ∧ 𝑚 ≠ 0 ) → (((𝐼‘(𝑌‘0))(.r‘𝐾)(𝐼‘𝑚))(.r‘(Scalar‘𝑊))𝑚) = (𝐼‘(𝑌‘0))) |
| 87 | 86 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) ∧ 𝑚 ≠ 0 ) → ((((𝐼‘(𝑌‘0))(.r‘𝐾)(𝐼‘𝑚))(.r‘(Scalar‘𝑊))𝑚) · 𝑌) = ((𝐼‘(𝑌‘0)) · 𝑌)) |
| 88 | 62, 76, 87 | 3eqtr2d 2783 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) ∧ 𝑚 ≠ 0 ) → ((𝐼‘((𝑚 · 𝑌)‘0)) · (𝑚 · 𝑌)) = ((𝐼‘(𝑌‘0)) · 𝑌)) |
| 89 | | fveq1 6905 |
. . . . . . . . . . . . 13
⊢ (𝑋 = (𝑚 · 𝑌) → (𝑋‘0) = ((𝑚 · 𝑌)‘0)) |
| 90 | 89 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ (𝑋 = (𝑚 · 𝑌) → (𝐼‘(𝑋‘0)) = (𝐼‘((𝑚 · 𝑌)‘0))) |
| 91 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑋 = (𝑚 · 𝑌) → 𝑋 = (𝑚 · 𝑌)) |
| 92 | 90, 91 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ (𝑋 = (𝑚 · 𝑌) → ((𝐼‘(𝑋‘0)) · 𝑋) = ((𝐼‘((𝑚 · 𝑌)‘0)) · (𝑚 · 𝑌))) |
| 93 | 92 | eqeq1d 2739 |
. . . . . . . . . 10
⊢ (𝑋 = (𝑚 · 𝑌) → (((𝐼‘(𝑋‘0)) · 𝑋) = ((𝐼‘(𝑌‘0)) · 𝑌) ↔ ((𝐼‘((𝑚 · 𝑌)‘0)) · (𝑚 · 𝑌)) = ((𝐼‘(𝑌‘0)) · 𝑌))) |
| 94 | 88, 93 | syl5ibrcom 247 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) ∧ 𝑚 ≠ 0 ) → (𝑋 = (𝑚 · 𝑌) → ((𝐼‘(𝑋‘0)) · 𝑋) = ((𝐼‘(𝑌‘0)) · 𝑌))) |
| 95 | 94 | expimpd 453 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) → ((𝑚 ≠ 0 ∧ 𝑋 = (𝑚 · 𝑌)) → ((𝐼‘(𝑋‘0)) · 𝑋) = ((𝐼‘(𝑌‘0)) · 𝑌))) |
| 96 | 42, 95 | syld 47 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑆) → (𝑋 = (𝑚 · 𝑌) → ((𝐼‘(𝑋‘0)) · 𝑋) = ((𝐼‘(𝑌‘0)) · 𝑌))) |
| 97 | 96 | rexlimdva 3155 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (∃𝑚 ∈ 𝑆 𝑋 = (𝑚 · 𝑌) → ((𝐼‘(𝑋‘0)) · 𝑋) = ((𝐼‘(𝑌‘0)) · 𝑌))) |
| 98 | 97 | impr 454 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ∃𝑚 ∈ 𝑆 𝑋 = (𝑚 · 𝑌))) → ((𝐼‘(𝑋‘0)) · 𝑋) = ((𝐼‘(𝑌‘0)) · 𝑌)) |
| 99 | 3 | neneqd 2945 |
. . . . . . 7
⊢ (𝜑 → ¬ (𝑋‘0) = 0 ) |
| 100 | 99 | iffalsed 4536 |
. . . . . 6
⊢ (𝜑 → if((𝑋‘0) = 0 , 𝑋, ((𝐼‘(𝑋‘0)) · 𝑋)) = ((𝐼‘(𝑋‘0)) · 𝑋)) |
| 101 | 100 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ∃𝑚 ∈ 𝑆 𝑋 = (𝑚 · 𝑌))) → if((𝑋‘0) = 0 , 𝑋, ((𝐼‘(𝑋‘0)) · 𝑋)) = ((𝐼‘(𝑋‘0)) · 𝑋)) |
| 102 | 58 | neneqd 2945 |
. . . . . . 7
⊢ (𝜑 → ¬ (𝑌‘0) = 0 ) |
| 103 | 102 | iffalsed 4536 |
. . . . . 6
⊢ (𝜑 → if((𝑌‘0) = 0 , 𝑌, ((𝐼‘(𝑌‘0)) · 𝑌)) = ((𝐼‘(𝑌‘0)) · 𝑌)) |
| 104 | 103 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ∃𝑚 ∈ 𝑆 𝑋 = (𝑚 · 𝑌))) → if((𝑌‘0) = 0 , 𝑌, ((𝐼‘(𝑌‘0)) · 𝑌)) = ((𝐼‘(𝑌‘0)) · 𝑌)) |
| 105 | 98, 101, 104 | 3eqtr4d 2787 |
. . . 4
⊢ ((𝜑 ∧ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ∃𝑚 ∈ 𝑆 𝑋 = (𝑚 · 𝑌))) → if((𝑋‘0) = 0 , 𝑋, ((𝐼‘(𝑋‘0)) · 𝑋)) = if((𝑌‘0) = 0 , 𝑌, ((𝐼‘(𝑌‘0)) · 𝑌))) |
| 106 | | prjspner01.f |
. . . . 5
⊢ 𝐹 = (𝑏 ∈ 𝐵 ↦ if((𝑏‘0) = 0 , 𝑏, ((𝐼‘(𝑏‘0)) · 𝑏))) |
| 107 | | fveq1 6905 |
. . . . . . 7
⊢ (𝑏 = 𝑋 → (𝑏‘0) = (𝑋‘0)) |
| 108 | 107 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑏 = 𝑋 → ((𝑏‘0) = 0 ↔ (𝑋‘0) = 0 )) |
| 109 | | id 22 |
. . . . . 6
⊢ (𝑏 = 𝑋 → 𝑏 = 𝑋) |
| 110 | 107 | fveq2d 6910 |
. . . . . . 7
⊢ (𝑏 = 𝑋 → (𝐼‘(𝑏‘0)) = (𝐼‘(𝑋‘0))) |
| 111 | 110, 109 | oveq12d 7449 |
. . . . . 6
⊢ (𝑏 = 𝑋 → ((𝐼‘(𝑏‘0)) · 𝑏) = ((𝐼‘(𝑋‘0)) · 𝑋)) |
| 112 | 108, 109,
111 | ifbieq12d 4554 |
. . . . 5
⊢ (𝑏 = 𝑋 → if((𝑏‘0) = 0 , 𝑏, ((𝐼‘(𝑏‘0)) · 𝑏)) = if((𝑋‘0) = 0 , 𝑋, ((𝐼‘(𝑋‘0)) · 𝑋))) |
| 113 | | simprll 779 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ∃𝑚 ∈ 𝑆 𝑋 = (𝑚 · 𝑌))) → 𝑋 ∈ 𝐵) |
| 114 | | ovexd 7466 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ∃𝑚 ∈ 𝑆 𝑋 = (𝑚 · 𝑌))) → ((𝐼‘(𝑋‘0)) · 𝑋) ∈ V) |
| 115 | 113, 114 | ifexd 4574 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ∃𝑚 ∈ 𝑆 𝑋 = (𝑚 · 𝑌))) → if((𝑋‘0) = 0 , 𝑋, ((𝐼‘(𝑋‘0)) · 𝑋)) ∈ V) |
| 116 | 106, 112,
113, 115 | fvmptd3 7039 |
. . . 4
⊢ ((𝜑 ∧ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ∃𝑚 ∈ 𝑆 𝑋 = (𝑚 · 𝑌))) → (𝐹‘𝑋) = if((𝑋‘0) = 0 , 𝑋, ((𝐼‘(𝑋‘0)) · 𝑋))) |
| 117 | | fveq1 6905 |
. . . . . . 7
⊢ (𝑏 = 𝑌 → (𝑏‘0) = (𝑌‘0)) |
| 118 | 117 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑏 = 𝑌 → ((𝑏‘0) = 0 ↔ (𝑌‘0) = 0 )) |
| 119 | | id 22 |
. . . . . 6
⊢ (𝑏 = 𝑌 → 𝑏 = 𝑌) |
| 120 | 117 | fveq2d 6910 |
. . . . . . 7
⊢ (𝑏 = 𝑌 → (𝐼‘(𝑏‘0)) = (𝐼‘(𝑌‘0))) |
| 121 | 120, 119 | oveq12d 7449 |
. . . . . 6
⊢ (𝑏 = 𝑌 → ((𝐼‘(𝑏‘0)) · 𝑏) = ((𝐼‘(𝑌‘0)) · 𝑌)) |
| 122 | 118, 119,
121 | ifbieq12d 4554 |
. . . . 5
⊢ (𝑏 = 𝑌 → if((𝑏‘0) = 0 , 𝑏, ((𝐼‘(𝑏‘0)) · 𝑏)) = if((𝑌‘0) = 0 , 𝑌, ((𝐼‘(𝑌‘0)) · 𝑌))) |
| 123 | | simprlr 780 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ∃𝑚 ∈ 𝑆 𝑋 = (𝑚 · 𝑌))) → 𝑌 ∈ 𝐵) |
| 124 | | ovexd 7466 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ∃𝑚 ∈ 𝑆 𝑋 = (𝑚 · 𝑌))) → ((𝐼‘(𝑌‘0)) · 𝑌) ∈ V) |
| 125 | 123, 124 | ifexd 4574 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ∃𝑚 ∈ 𝑆 𝑋 = (𝑚 · 𝑌))) → if((𝑌‘0) = 0 , 𝑌, ((𝐼‘(𝑌‘0)) · 𝑌)) ∈ V) |
| 126 | 106, 122,
123, 125 | fvmptd3 7039 |
. . . 4
⊢ ((𝜑 ∧ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ∃𝑚 ∈ 𝑆 𝑋 = (𝑚 · 𝑌))) → (𝐹‘𝑌) = if((𝑌‘0) = 0 , 𝑌, ((𝐼‘(𝑌‘0)) · 𝑌))) |
| 127 | 105, 116,
126 | 3eqtr4d 2787 |
. . 3
⊢ ((𝜑 ∧ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ∃𝑚 ∈ 𝑆 𝑋 = (𝑚 · 𝑌))) → (𝐹‘𝑋) = (𝐹‘𝑌)) |
| 128 | 2, 127 | sylan2b 594 |
. 2
⊢ ((𝜑 ∧ 𝑋 ∼ 𝑌) → (𝐹‘𝑋) = (𝐹‘𝑌)) |
| 129 | 1, 5, 25, 43, 30, 7 | prjspner 42629 |
. . . 4
⊢ (𝜑 → ∼ Er 𝐵) |
| 130 | 129 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝐹‘𝑋) = (𝐹‘𝑌)) → ∼ Er 𝐵) |
| 131 | | prjspner01.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
| 132 | 1, 106, 25, 5, 30, 43, 6, 51, 7, 10, 131 | prjspner01 42635 |
. . . 4
⊢ (𝜑 → 𝑋 ∼ (𝐹‘𝑋)) |
| 133 | 132 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝐹‘𝑋) = (𝐹‘𝑌)) → 𝑋 ∼ (𝐹‘𝑋)) |
| 134 | 129, 132 | ercl2 8758 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘𝑋) ∈ 𝐵) |
| 135 | 134 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹‘𝑋) = (𝐹‘𝑌)) → (𝐹‘𝑋) ∈ 𝐵) |
| 136 | 130, 135 | erref 8765 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹‘𝑋) = (𝐹‘𝑌)) → (𝐹‘𝑋) ∼ (𝐹‘𝑋)) |
| 137 | | breq2 5147 |
. . . . . 6
⊢ ((𝐹‘𝑋) = (𝐹‘𝑌) → ((𝐹‘𝑋) ∼ (𝐹‘𝑋) ↔ (𝐹‘𝑋) ∼ (𝐹‘𝑌))) |
| 138 | 137 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹‘𝑋) = (𝐹‘𝑌)) → ((𝐹‘𝑋) ∼ (𝐹‘𝑋) ↔ (𝐹‘𝑋) ∼ (𝐹‘𝑌))) |
| 139 | 136, 138 | mpbid 232 |
. . . 4
⊢ ((𝜑 ∧ (𝐹‘𝑋) = (𝐹‘𝑌)) → (𝐹‘𝑋) ∼ (𝐹‘𝑌)) |
| 140 | 1, 106, 25, 5, 30, 43, 6, 51, 7, 10, 24 | prjspner01 42635 |
. . . . 5
⊢ (𝜑 → 𝑌 ∼ (𝐹‘𝑌)) |
| 141 | 140 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝐹‘𝑋) = (𝐹‘𝑌)) → 𝑌 ∼ (𝐹‘𝑌)) |
| 142 | 130, 139,
141 | ertr4d 8764 |
. . 3
⊢ ((𝜑 ∧ (𝐹‘𝑋) = (𝐹‘𝑌)) → (𝐹‘𝑋) ∼ 𝑌) |
| 143 | 130, 133,
142 | ertrd 8761 |
. 2
⊢ ((𝜑 ∧ (𝐹‘𝑋) = (𝐹‘𝑌)) → 𝑋 ∼ 𝑌) |
| 144 | 128, 143 | impbida 801 |
1
⊢ (𝜑 → (𝑋 ∼ 𝑌 ↔ (𝐹‘𝑋) = (𝐹‘𝑌))) |