Proof of Theorem nvmul0or
| Step | Hyp | Ref
| Expression |
| 1 | | df-ne 2941 |
. . . . 5
⊢ (𝐴 ≠ 0 ↔ ¬ 𝐴 = 0) |
| 2 | | oveq2 7439 |
. . . . . . . 8
⊢ ((𝐴𝑆𝐵) = 𝑍 → ((1 / 𝐴)𝑆(𝐴𝑆𝐵)) = ((1 / 𝐴)𝑆𝑍)) |
| 3 | 2 | ad2antlr 727 |
. . . . . . 7
⊢ ((((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑆𝐵) = 𝑍) ∧ 𝐴 ≠ 0) → ((1 / 𝐴)𝑆(𝐴𝑆𝐵)) = ((1 / 𝐴)𝑆𝑍)) |
| 4 | | recid2 11937 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → ((1 / 𝐴) · 𝐴) = 1) |
| 5 | 4 | oveq1d 7446 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (((1 / 𝐴) · 𝐴)𝑆𝐵) = (1𝑆𝐵)) |
| 6 | 5 | 3ad2antl2 1187 |
. . . . . . . . 9
⊢ (((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≠ 0) → (((1 / 𝐴) · 𝐴)𝑆𝐵) = (1𝑆𝐵)) |
| 7 | | simpl1 1192 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≠ 0) → 𝑈 ∈ NrmCVec) |
| 8 | | reccl 11929 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈
ℂ) |
| 9 | 8 | 3ad2antl2 1187 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈ ℂ) |
| 10 | | simpl2 1193 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≠ 0) → 𝐴 ∈ ℂ) |
| 11 | | simpl3 1194 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≠ 0) → 𝐵 ∈ 𝑋) |
| 12 | | nvmul0or.1 |
. . . . . . . . . . 11
⊢ 𝑋 = (BaseSet‘𝑈) |
| 13 | | nvmul0or.4 |
. . . . . . . . . . 11
⊢ 𝑆 = (
·𝑠OLD ‘𝑈) |
| 14 | 12, 13 | nvsass 30647 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ ((1 /
𝐴) ∈ ℂ ∧
𝐴 ∈ ℂ ∧
𝐵 ∈ 𝑋)) → (((1 / 𝐴) · 𝐴)𝑆𝐵) = ((1 / 𝐴)𝑆(𝐴𝑆𝐵))) |
| 15 | 7, 9, 10, 11, 14 | syl13anc 1374 |
. . . . . . . . 9
⊢ (((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≠ 0) → (((1 / 𝐴) · 𝐴)𝑆𝐵) = ((1 / 𝐴)𝑆(𝐴𝑆𝐵))) |
| 16 | 12, 13 | nvsid 30646 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋) → (1𝑆𝐵) = 𝐵) |
| 17 | 16 | 3adant2 1132 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋) → (1𝑆𝐵) = 𝐵) |
| 18 | 17 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≠ 0) → (1𝑆𝐵) = 𝐵) |
| 19 | 6, 15, 18 | 3eqtr3d 2785 |
. . . . . . . 8
⊢ (((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≠ 0) → ((1 / 𝐴)𝑆(𝐴𝑆𝐵)) = 𝐵) |
| 20 | 19 | adantlr 715 |
. . . . . . 7
⊢ ((((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑆𝐵) = 𝑍) ∧ 𝐴 ≠ 0) → ((1 / 𝐴)𝑆(𝐴𝑆𝐵)) = 𝐵) |
| 21 | | nvmul0or.6 |
. . . . . . . . . . . 12
⊢ 𝑍 = (0vec‘𝑈) |
| 22 | 13, 21 | nvsz 30657 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ NrmCVec ∧ (1 / 𝐴) ∈ ℂ) → ((1 /
𝐴)𝑆𝑍) = 𝑍) |
| 23 | 8, 22 | sylan2 593 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0)) → ((1 / 𝐴)𝑆𝑍) = 𝑍) |
| 24 | 23 | anassrs 467 |
. . . . . . . . 9
⊢ (((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ) ∧ 𝐴 ≠ 0) → ((1 / 𝐴)𝑆𝑍) = 𝑍) |
| 25 | 24 | 3adantl3 1169 |
. . . . . . . 8
⊢ (((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≠ 0) → ((1 / 𝐴)𝑆𝑍) = 𝑍) |
| 26 | 25 | adantlr 715 |
. . . . . . 7
⊢ ((((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑆𝐵) = 𝑍) ∧ 𝐴 ≠ 0) → ((1 / 𝐴)𝑆𝑍) = 𝑍) |
| 27 | 3, 20, 26 | 3eqtr3d 2785 |
. . . . . 6
⊢ ((((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑆𝐵) = 𝑍) ∧ 𝐴 ≠ 0) → 𝐵 = 𝑍) |
| 28 | 27 | ex 412 |
. . . . 5
⊢ (((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑆𝐵) = 𝑍) → (𝐴 ≠ 0 → 𝐵 = 𝑍)) |
| 29 | 1, 28 | biimtrrid 243 |
. . . 4
⊢ (((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑆𝐵) = 𝑍) → (¬ 𝐴 = 0 → 𝐵 = 𝑍)) |
| 30 | 29 | orrd 864 |
. . 3
⊢ (((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑆𝐵) = 𝑍) → (𝐴 = 0 ∨ 𝐵 = 𝑍)) |
| 31 | 30 | ex 412 |
. 2
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋) → ((𝐴𝑆𝐵) = 𝑍 → (𝐴 = 0 ∨ 𝐵 = 𝑍))) |
| 32 | 12, 13, 21 | nv0 30656 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋) → (0𝑆𝐵) = 𝑍) |
| 33 | | oveq1 7438 |
. . . . . 6
⊢ (𝐴 = 0 → (𝐴𝑆𝐵) = (0𝑆𝐵)) |
| 34 | 33 | eqeq1d 2739 |
. . . . 5
⊢ (𝐴 = 0 → ((𝐴𝑆𝐵) = 𝑍 ↔ (0𝑆𝐵) = 𝑍)) |
| 35 | 32, 34 | syl5ibrcom 247 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋) → (𝐴 = 0 → (𝐴𝑆𝐵) = 𝑍)) |
| 36 | 35 | 3adant2 1132 |
. . 3
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋) → (𝐴 = 0 → (𝐴𝑆𝐵) = 𝑍)) |
| 37 | 13, 21 | nvsz 30657 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ) → (𝐴𝑆𝑍) = 𝑍) |
| 38 | | oveq2 7439 |
. . . . . 6
⊢ (𝐵 = 𝑍 → (𝐴𝑆𝐵) = (𝐴𝑆𝑍)) |
| 39 | 38 | eqeq1d 2739 |
. . . . 5
⊢ (𝐵 = 𝑍 → ((𝐴𝑆𝐵) = 𝑍 ↔ (𝐴𝑆𝑍) = 𝑍)) |
| 40 | 37, 39 | syl5ibrcom 247 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ) → (𝐵 = 𝑍 → (𝐴𝑆𝐵) = 𝑍)) |
| 41 | 40 | 3adant3 1133 |
. . 3
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋) → (𝐵 = 𝑍 → (𝐴𝑆𝐵) = 𝑍)) |
| 42 | 36, 41 | jaod 860 |
. 2
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋) → ((𝐴 = 0 ∨ 𝐵 = 𝑍) → (𝐴𝑆𝐵) = 𝑍)) |
| 43 | 31, 42 | impbid 212 |
1
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋) → ((𝐴𝑆𝐵) = 𝑍 ↔ (𝐴 = 0 ∨ 𝐵 = 𝑍))) |