| Step | Hyp | Ref
| Expression |
| 1 | | lspsneu.v |
. . . . . . 7
⊢ 𝑉 = (Base‘𝑊) |
| 2 | | lspsneu.s |
. . . . . . 7
⊢ 𝑆 = (Scalar‘𝑊) |
| 3 | | lspsneu.k |
. . . . . . 7
⊢ 𝐾 = (Base‘𝑆) |
| 4 | | lspsneu.o |
. . . . . . 7
⊢ 𝑂 = (0g‘𝑆) |
| 5 | | lspsneu.t |
. . . . . . 7
⊢ · = (
·𝑠 ‘𝑊) |
| 6 | | lspsneu.n |
. . . . . . 7
⊢ 𝑁 = (LSpan‘𝑊) |
| 7 | | lspsneu.w |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ LVec) |
| 8 | | lspsneu.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
| 9 | | lspsneu.y |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) |
| 10 | 9 | eldifad 3963 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
| 11 | 1, 2, 3, 4, 5, 6, 7, 8, 10 | lspsneq 21124 |
. . . . . 6
⊢ (𝜑 → ((𝑁‘{𝑋}) = (𝑁‘{𝑌}) ↔ ∃𝑗 ∈ (𝐾 ∖ {𝑂})𝑋 = (𝑗 · 𝑌))) |
| 12 | 11 | biimpd 229 |
. . . . 5
⊢ (𝜑 → ((𝑁‘{𝑋}) = (𝑁‘{𝑌}) → ∃𝑗 ∈ (𝐾 ∖ {𝑂})𝑋 = (𝑗 · 𝑌))) |
| 13 | | eqtr2 2761 |
. . . . . . . . . 10
⊢ ((𝑋 = (𝑗 · 𝑌) ∧ 𝑋 = (𝑖 · 𝑌)) → (𝑗 · 𝑌) = (𝑖 · 𝑌)) |
| 14 | 13 | 3ad2ant3 1136 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ (𝑗 ∈ (𝐾 ∖ {𝑂}) ∧ 𝑖 ∈ (𝐾 ∖ {𝑂})) ∧ (𝑋 = (𝑗 · 𝑌) ∧ 𝑋 = (𝑖 · 𝑌))) → (𝑗 · 𝑌) = (𝑖 · 𝑌)) |
| 15 | | lspsneu.z |
. . . . . . . . . 10
⊢ 0 =
(0g‘𝑊) |
| 16 | | simp1l 1198 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ (𝑗 ∈ (𝐾 ∖ {𝑂}) ∧ 𝑖 ∈ (𝐾 ∖ {𝑂})) ∧ (𝑋 = (𝑗 · 𝑌) ∧ 𝑋 = (𝑖 · 𝑌))) → 𝜑) |
| 17 | 16, 7 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ (𝑗 ∈ (𝐾 ∖ {𝑂}) ∧ 𝑖 ∈ (𝐾 ∖ {𝑂})) ∧ (𝑋 = (𝑗 · 𝑌) ∧ 𝑋 = (𝑖 · 𝑌))) → 𝑊 ∈ LVec) |
| 18 | | simp2l 1200 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ (𝑗 ∈ (𝐾 ∖ {𝑂}) ∧ 𝑖 ∈ (𝐾 ∖ {𝑂})) ∧ (𝑋 = (𝑗 · 𝑌) ∧ 𝑋 = (𝑖 · 𝑌))) → 𝑗 ∈ (𝐾 ∖ {𝑂})) |
| 19 | 18 | eldifad 3963 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ (𝑗 ∈ (𝐾 ∖ {𝑂}) ∧ 𝑖 ∈ (𝐾 ∖ {𝑂})) ∧ (𝑋 = (𝑗 · 𝑌) ∧ 𝑋 = (𝑖 · 𝑌))) → 𝑗 ∈ 𝐾) |
| 20 | | simp2r 1201 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ (𝑗 ∈ (𝐾 ∖ {𝑂}) ∧ 𝑖 ∈ (𝐾 ∖ {𝑂})) ∧ (𝑋 = (𝑗 · 𝑌) ∧ 𝑋 = (𝑖 · 𝑌))) → 𝑖 ∈ (𝐾 ∖ {𝑂})) |
| 21 | 20 | eldifad 3963 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ (𝑗 ∈ (𝐾 ∖ {𝑂}) ∧ 𝑖 ∈ (𝐾 ∖ {𝑂})) ∧ (𝑋 = (𝑗 · 𝑌) ∧ 𝑋 = (𝑖 · 𝑌))) → 𝑖 ∈ 𝐾) |
| 22 | 16, 10 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ (𝑗 ∈ (𝐾 ∖ {𝑂}) ∧ 𝑖 ∈ (𝐾 ∖ {𝑂})) ∧ (𝑋 = (𝑗 · 𝑌) ∧ 𝑋 = (𝑖 · 𝑌))) → 𝑌 ∈ 𝑉) |
| 23 | | eldifsni 4790 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ (𝑉 ∖ { 0 }) → 𝑌 ≠ 0 ) |
| 24 | 16, 9, 23 | 3syl 18 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ (𝑗 ∈ (𝐾 ∖ {𝑂}) ∧ 𝑖 ∈ (𝐾 ∖ {𝑂})) ∧ (𝑋 = (𝑗 · 𝑌) ∧ 𝑋 = (𝑖 · 𝑌))) → 𝑌 ≠ 0 ) |
| 25 | 1, 5, 2, 3, 15, 17, 19, 21, 22, 24 | lvecvscan2 21114 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ (𝑗 ∈ (𝐾 ∖ {𝑂}) ∧ 𝑖 ∈ (𝐾 ∖ {𝑂})) ∧ (𝑋 = (𝑗 · 𝑌) ∧ 𝑋 = (𝑖 · 𝑌))) → ((𝑗 · 𝑌) = (𝑖 · 𝑌) ↔ 𝑗 = 𝑖)) |
| 26 | 14, 25 | mpbid 232 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) ∧ (𝑗 ∈ (𝐾 ∖ {𝑂}) ∧ 𝑖 ∈ (𝐾 ∖ {𝑂})) ∧ (𝑋 = (𝑗 · 𝑌) ∧ 𝑋 = (𝑖 · 𝑌))) → 𝑗 = 𝑖) |
| 27 | 26 | 3exp 1120 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑁‘{𝑋}) = (𝑁‘{𝑌})) → ((𝑗 ∈ (𝐾 ∖ {𝑂}) ∧ 𝑖 ∈ (𝐾 ∖ {𝑂})) → ((𝑋 = (𝑗 · 𝑌) ∧ 𝑋 = (𝑖 · 𝑌)) → 𝑗 = 𝑖))) |
| 28 | 27 | ex 412 |
. . . . . 6
⊢ (𝜑 → ((𝑁‘{𝑋}) = (𝑁‘{𝑌}) → ((𝑗 ∈ (𝐾 ∖ {𝑂}) ∧ 𝑖 ∈ (𝐾 ∖ {𝑂})) → ((𝑋 = (𝑗 · 𝑌) ∧ 𝑋 = (𝑖 · 𝑌)) → 𝑗 = 𝑖)))) |
| 29 | 28 | ralrimdvv 3203 |
. . . . 5
⊢ (𝜑 → ((𝑁‘{𝑋}) = (𝑁‘{𝑌}) → ∀𝑗 ∈ (𝐾 ∖ {𝑂})∀𝑖 ∈ (𝐾 ∖ {𝑂})((𝑋 = (𝑗 · 𝑌) ∧ 𝑋 = (𝑖 · 𝑌)) → 𝑗 = 𝑖))) |
| 30 | 12, 29 | jcad 512 |
. . . 4
⊢ (𝜑 → ((𝑁‘{𝑋}) = (𝑁‘{𝑌}) → (∃𝑗 ∈ (𝐾 ∖ {𝑂})𝑋 = (𝑗 · 𝑌) ∧ ∀𝑗 ∈ (𝐾 ∖ {𝑂})∀𝑖 ∈ (𝐾 ∖ {𝑂})((𝑋 = (𝑗 · 𝑌) ∧ 𝑋 = (𝑖 · 𝑌)) → 𝑗 = 𝑖)))) |
| 31 | | oveq1 7438 |
. . . . . 6
⊢ (𝑗 = 𝑖 → (𝑗 · 𝑌) = (𝑖 · 𝑌)) |
| 32 | 31 | eqeq2d 2748 |
. . . . 5
⊢ (𝑗 = 𝑖 → (𝑋 = (𝑗 · 𝑌) ↔ 𝑋 = (𝑖 · 𝑌))) |
| 33 | 32 | reu4 3737 |
. . . 4
⊢
(∃!𝑗 ∈
(𝐾 ∖ {𝑂})𝑋 = (𝑗 · 𝑌) ↔ (∃𝑗 ∈ (𝐾 ∖ {𝑂})𝑋 = (𝑗 · 𝑌) ∧ ∀𝑗 ∈ (𝐾 ∖ {𝑂})∀𝑖 ∈ (𝐾 ∖ {𝑂})((𝑋 = (𝑗 · 𝑌) ∧ 𝑋 = (𝑖 · 𝑌)) → 𝑗 = 𝑖))) |
| 34 | 30, 33 | imbitrrdi 252 |
. . 3
⊢ (𝜑 → ((𝑁‘{𝑋}) = (𝑁‘{𝑌}) → ∃!𝑗 ∈ (𝐾 ∖ {𝑂})𝑋 = (𝑗 · 𝑌))) |
| 35 | | reurex 3384 |
. . . 4
⊢
(∃!𝑗 ∈
(𝐾 ∖ {𝑂})𝑋 = (𝑗 · 𝑌) → ∃𝑗 ∈ (𝐾 ∖ {𝑂})𝑋 = (𝑗 · 𝑌)) |
| 36 | 35, 11 | imbitrrid 246 |
. . 3
⊢ (𝜑 → (∃!𝑗 ∈ (𝐾 ∖ {𝑂})𝑋 = (𝑗 · 𝑌) → (𝑁‘{𝑋}) = (𝑁‘{𝑌}))) |
| 37 | 34, 36 | impbid 212 |
. 2
⊢ (𝜑 → ((𝑁‘{𝑋}) = (𝑁‘{𝑌}) ↔ ∃!𝑗 ∈ (𝐾 ∖ {𝑂})𝑋 = (𝑗 · 𝑌))) |
| 38 | | oveq1 7438 |
. . . 4
⊢ (𝑗 = 𝑘 → (𝑗 · 𝑌) = (𝑘 · 𝑌)) |
| 39 | 38 | eqeq2d 2748 |
. . 3
⊢ (𝑗 = 𝑘 → (𝑋 = (𝑗 · 𝑌) ↔ 𝑋 = (𝑘 · 𝑌))) |
| 40 | 39 | cbvreuvw 3404 |
. 2
⊢
(∃!𝑗 ∈
(𝐾 ∖ {𝑂})𝑋 = (𝑗 · 𝑌) ↔ ∃!𝑘 ∈ (𝐾 ∖ {𝑂})𝑋 = (𝑘 · 𝑌)) |
| 41 | 37, 40 | bitrdi 287 |
1
⊢ (𝜑 → ((𝑁‘{𝑋}) = (𝑁‘{𝑌}) ↔ ∃!𝑘 ∈ (𝐾 ∖ {𝑂})𝑋 = (𝑘 · 𝑌))) |