![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nvnnncan1 | Structured version Visualization version GIF version |
Description: Cancellation law for vector subtraction. (nnncan1 10520 analog.) (Contributed by NM, 7-Mar-2008.) (New usage is discouraged.) |
Ref | Expression |
---|---|
nvmf.1 | ⊢ 𝑋 = (BaseSet‘𝑈) |
nvmf.3 | ⊢ 𝑀 = ( −𝑣 ‘𝑈) |
Ref | Expression |
---|---|
nvnnncan1 | ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝑀𝐵)𝑀(𝐴𝑀𝐶)) = (𝐶𝑀𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2771 | . . 3 ⊢ ( +𝑣 ‘𝑈) = ( +𝑣 ‘𝑈) | |
2 | 1 | nvablo 27812 | . 2 ⊢ (𝑈 ∈ NrmCVec → ( +𝑣 ‘𝑈) ∈ AbelOp) |
3 | nvmf.1 | . . . 4 ⊢ 𝑋 = (BaseSet‘𝑈) | |
4 | 3, 1 | bafval 27800 | . . 3 ⊢ 𝑋 = ran ( +𝑣 ‘𝑈) |
5 | nvmf.3 | . . . 4 ⊢ 𝑀 = ( −𝑣 ‘𝑈) | |
6 | 1, 5 | vsfval 27829 | . . 3 ⊢ 𝑀 = ( /𝑔 ‘( +𝑣 ‘𝑈)) |
7 | 4, 6 | ablonnncan1 27753 | . 2 ⊢ ((( +𝑣 ‘𝑈) ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝑀𝐵)𝑀(𝐴𝑀𝐶)) = (𝐶𝑀𝐵)) |
8 | 2, 7 | sylan 563 | 1 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝑀𝐵)𝑀(𝐴𝑀𝐶)) = (𝐶𝑀𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 382 ∧ w3a 1071 = wceq 1631 ∈ wcel 2145 ‘cfv 6032 (class class class)co 6794 AbelOpcablo 27739 NrmCVeccnv 27780 +𝑣 cpv 27781 BaseSetcba 27782 −𝑣 cnsb 27785 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-8 2147 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-rep 4905 ax-sep 4916 ax-nul 4924 ax-pow 4975 ax-pr 5035 ax-un 7097 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 829 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ne 2944 df-ral 3066 df-rex 3067 df-reu 3068 df-rab 3070 df-v 3353 df-sbc 3589 df-csb 3684 df-dif 3727 df-un 3729 df-in 3731 df-ss 3738 df-nul 4065 df-if 4227 df-pw 4300 df-sn 4318 df-pr 4320 df-op 4324 df-uni 4576 df-iun 4657 df-br 4788 df-opab 4848 df-mpt 4865 df-id 5158 df-xp 5256 df-rel 5257 df-cnv 5258 df-co 5259 df-dm 5260 df-rn 5261 df-res 5262 df-ima 5263 df-iota 5995 df-fun 6034 df-fn 6035 df-f 6036 df-f1 6037 df-fo 6038 df-f1o 6039 df-fv 6040 df-riota 6755 df-ov 6797 df-oprab 6798 df-mpt2 6799 df-1st 7316 df-2nd 7317 df-grpo 27688 df-gid 27689 df-ginv 27690 df-gdiv 27691 df-ablo 27740 df-vc 27755 df-nv 27788 df-va 27791 df-ba 27792 df-sm 27793 df-0v 27794 df-vs 27795 df-nmcv 27796 |
This theorem is referenced by: minvecolem2 28072 |
Copyright terms: Public domain | W3C validator |