Nearby theorems
|
|
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > MPE Home > Th. List > dipsubdi | Structured version Visualization version GIF version | ||
| Description: Distributive law for inner product subtraction. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
| Ref | Expression |
|---|---|
| ipsubdir.1 | ⊢ 𝑋 = (BaseSet‘𝑈) |
| ipsubdir.3 | ⊢ 𝑀 = ( −𝑣 ‘𝑈) |
| ipsubdir.7 | ⊢ 𝑃 = (·𝑖OLD‘𝑈) |
| Ref | Expression |
|---|---|
| dipsubdi | ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑃(𝐵𝑀𝐶)) = ((𝐴𝑃𝐵) − (𝐴𝑃𝐶))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | id 22 | . . 3 ⊢ ((𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) | |
| 2 | 1 | 3com13 1123 | . 2 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) |
| 3 | id 22 | . . . . . 6 ⊢ ((𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) | |
| 4 | 3 | 3com12 1122 | . . . . 5 ⊢ ((𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) |
| 5 | ipsubdir.1 | . . . . . 6 ⊢ 𝑋 = (BaseSet‘𝑈) | |
| 6 | ipsubdir.3 | . . . . . 6 ⊢ 𝑀 = ( −𝑣 ‘𝑈) | |
| 7 | ipsubdir.7 | . . . . . 6 ⊢ 𝑃 = (·𝑖OLD‘𝑈) | |
| 8 | 5, 6, 7 | dipsubdir 29318 | . . . . 5 ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → ((𝐵𝑀𝐶)𝑃𝐴) = ((𝐵𝑃𝐴) − (𝐶𝑃𝐴))) |
| 9 | 4, 8 | sylan2 593 | . . . 4 ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → ((𝐵𝑀𝐶)𝑃𝐴) = ((𝐵𝑃𝐴) − (𝐶𝑃𝐴))) |
| 10 | 9 | fveq2d 6813 | . . 3 ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (∗‘((𝐵𝑀𝐶)𝑃𝐴)) = (∗‘((𝐵𝑃𝐴) − (𝐶𝑃𝐴)))) |
| 11 | phnv 29284 | . . . 4 ⊢ (𝑈 ∈ CPreHilOLD → 𝑈 ∈ NrmCVec) | |
| 12 | simpl 483 | . . . . 5 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → 𝑈 ∈ NrmCVec) | |
| 13 | 5, 6 | nvmcl 29116 | . . . . . . 7 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐵𝑀𝐶) ∈ 𝑋) |
| 14 | 13 | 3com23 1125 | . . . . . 6 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐵𝑀𝐶) ∈ 𝑋) |
| 15 | 14 | 3adant3r3 1183 | . . . . 5 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐵𝑀𝐶) ∈ 𝑋) |
| 16 | simpr3 1195 | . . . . 5 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → 𝐴 ∈ 𝑋) | |
| 17 | 5, 7 | dipcj 29184 | . . . . 5 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐵𝑀𝐶) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (∗‘((𝐵𝑀𝐶)𝑃𝐴)) = (𝐴𝑃(𝐵𝑀𝐶))) |
| 18 | 12, 15, 16, 17 | syl3anc 1370 | . . . 4 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (∗‘((𝐵𝑀𝐶)𝑃𝐴)) = (𝐴𝑃(𝐵𝑀𝐶))) |
| 19 | 11, 18 | sylan 580 | . . 3 ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (∗‘((𝐵𝑀𝐶)𝑃𝐴)) = (𝐴𝑃(𝐵𝑀𝐶))) |
| 20 | 5, 7 | dipcl 29182 | . . . . . . 7 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝐵𝑃𝐴) ∈ ℂ) |
| 21 | 20 | 3adant3r1 1181 | . . . . . 6 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐵𝑃𝐴) ∈ ℂ) |
| 22 | 5, 7 | dipcl 29182 | . . . . . . 7 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (𝐶𝑃𝐴) ∈ ℂ) |
| 23 | 22 | 3adant3r2 1182 | . . . . . 6 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐶𝑃𝐴) ∈ ℂ) |
| 24 | cjsub 14929 | . . . . . 6 ⊢ (((𝐵𝑃𝐴) ∈ ℂ ∧ (𝐶𝑃𝐴) ∈ ℂ) → (∗‘((𝐵𝑃𝐴) − (𝐶𝑃𝐴))) = ((∗‘(𝐵𝑃𝐴)) − (∗‘(𝐶𝑃𝐴)))) | |
| 25 | 21, 23, 24 | syl2anc 584 | . . . . 5 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (∗‘((𝐵𝑃𝐴) − (𝐶𝑃𝐴))) = ((∗‘(𝐵𝑃𝐴)) − (∗‘(𝐶𝑃𝐴)))) |
| 26 | 5, 7 | dipcj 29184 | . . . . . . 7 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (∗‘(𝐵𝑃𝐴)) = (𝐴𝑃𝐵)) |
| 27 | 26 | 3adant3r1 1181 | . . . . . 6 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (∗‘(𝐵𝑃𝐴)) = (𝐴𝑃𝐵)) |
| 28 | 5, 7 | dipcj 29184 | . . . . . . 7 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → (∗‘(𝐶𝑃𝐴)) = (𝐴𝑃𝐶)) |
| 29 | 28 | 3adant3r2 1182 | . . . . . 6 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (∗‘(𝐶𝑃𝐴)) = (𝐴𝑃𝐶)) |
| 30 | 27, 29 | oveq12d 7331 | . . . . 5 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → ((∗‘(𝐵𝑃𝐴)) − (∗‘(𝐶𝑃𝐴))) = ((𝐴𝑃𝐵) − (𝐴𝑃𝐶))) |
| 31 | 25, 30 | eqtrd 2777 | . . . 4 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (∗‘((𝐵𝑃𝐴) − (𝐶𝑃𝐴))) = ((𝐴𝑃𝐵) − (𝐴𝑃𝐶))) |
| 32 | 11, 31 | sylan 580 | . . 3 ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (∗‘((𝐵𝑃𝐴) − (𝐶𝑃𝐴))) = ((𝐴𝑃𝐵) − (𝐴𝑃𝐶))) |
| 33 | 10, 19, 32 | 3eqtr3d 2785 | . 2 ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴𝑃(𝐵𝑀𝐶)) = ((𝐴𝑃𝐵) − (𝐴𝑃𝐶))) |
| 34 | 2, 33 | sylan2 593 | 1 ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑃(𝐵𝑀𝐶)) = ((𝐴𝑃𝐵) − (𝐴𝑃𝐶))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1086 = wceq 1540 ∈ wcel 2105 ‘cfv 6463 (class class class)co 7313 ℂcc 10939 − cmin 11275 ∗ccj 14876 NrmCVeccnv 29054 BaseSetcba 29056 −𝑣 cnsb 29059 ·𝑖OLDcdip 29170 CPreHilOLDccphlo 29282 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2708 ax-rep 5222 ax-sep 5236 ax-nul 5243 ax-pow 5301 ax-pr 5365 ax-un 7626 ax-inf2 9467 ax-cnex 10997 ax-resscn 10998 ax-1cn 10999 ax-icn 11000 ax-addcl 11001 ax-addrcl 11002 ax-mulcl 11003 ax-mulrcl 11004 ax-mulcom 11005 ax-addass 11006 ax-mulass 11007 ax-distr 11008 ax-i2m1 11009 ax-1ne0 11010 ax-1rid 11011 ax-rnegex 11012 ax-rrecex 11013 ax-cnre 11014 ax-pre-lttri 11015 ax-pre-lttrn 11016 ax-pre-ltadd 11017 ax-pre-mulgt0 11018 ax-pre-sup 11019 ax-addf 11020 ax-mulf 11021 |
| This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3350 df-reu 3351 df-rab 3405 df-v 3443 df-sbc 3726 df-csb 3842 df-dif 3899 df-un 3901 df-in 3903 df-ss 3913 df-pss 3915 df-nul 4267 df-if 4470 df-pw 4545 df-sn 4570 df-pr 4572 df-tp 4574 df-op 4576 df-uni 4849 df-int 4891 df-iun 4937 df-iin 4938 df-br 5086 df-opab 5148 df-mpt 5169 df-tr 5203 df-id 5505 df-eprel 5511 df-po 5519 df-so 5520 df-fr 5560 df-se 5561 df-we 5562 df-xp 5611 df-rel 5612 df-cnv 5613 df-co 5614 df-dm 5615 df-rn 5616 df-res 5617 df-ima 5618 df-pred 6222 df-ord 6289 df-on 6290 df-lim 6291 df-suc 6292 df-iota 6415 df-fun 6465 df-fn 6466 df-f 6467 df-f1 6468 df-fo 6469 df-f1o 6470 df-fv 6471 df-isom 6472 df-riota 7270 df-ov 7316 df-oprab 7317 df-mpo 7318 df-of 7571 df-om 7756 df-1st 7874 df-2nd 7875 df-supp 8023 df-frecs 8142 df-wrecs 8173 df-recs 8247 df-rdg 8286 df-1o 8342 df-2o 8343 df-er 8544 df-map 8663 df-ixp 8732 df-en 8780 df-dom 8781 df-sdom 8782 df-fin 8783 df-fsupp 9197 df-fi 9238 df-sup 9269 df-inf 9270 df-oi 9337 df-card 9765 df-pnf 11081 df-mnf 11082 df-xr 11083 df-ltxr 11084 df-le 11085 df-sub 11277 df-neg 11278 df-div 11703 df-nn 12044 df-2 12106 df-3 12107 df-4 12108 df-5 12109 df-6 12110 df-7 12111 df-8 12112 df-9 12113 df-n0 12304 df-z 12390 df-dec 12508 df-uz 12653 df-q 12759 df-rp 12801 df-xneg 12918 df-xadd 12919 df-xmul 12920 df-ioo 13153 df-icc 13156 df-fz 13310 df-fzo 13453 df-seq 13792 df-exp 13853 df-hash 14115 df-cj 14879 df-re 14880 df-im 14881 df-sqrt 15015 df-abs 15016 df-clim 15266 df-sum 15467 df-struct 16915 df-sets 16932 df-slot 16950 df-ndx 16962 df-base 16980 df-ress 17009 df-plusg 17042 df-mulr 17043 df-starv 17044 df-sca 17045 df-vsca 17046 df-ip 17047 df-tset 17048 df-ple 17049 df-ds 17051 df-unif 17052 df-hom 17053 df-cco 17054 df-rest 17200 df-topn 17201 df-0g 17219 df-gsum 17220 df-topgen 17221 df-pt 17222 df-prds 17225 df-xrs 17280 df-qtop 17285 df-imas 17286 df-xps 17288 df-mre 17362 df-mrc 17363 df-acs 17365 df-mgm 18393 df-sgrp 18442 df-mnd 18453 df-submnd 18498 df-mulg 18768 df-cntz 18990 df-cmn 19455 df-psmet 20660 df-xmet 20661 df-met 20662 df-bl 20663 df-mopn 20664 df-cnfld 20669 df-top 22114 df-topon 22131 df-topsp 22153 df-bases 22167 df-cld 22241 df-ntr 22242 df-cls 22243 df-cn 22449 df-cnp 22450 df-t1 22536 df-haus 22537 df-tx 22784 df-hmeo 22977 df-xms 23544 df-ms 23545 df-tms 23546 df-grpo 28963 df-gid 28964 df-ginv 28965 df-gdiv 28966 df-ablo 29015 df-vc 29029 df-nv 29062 df-va 29065 df-ba 29066 df-sm 29067 df-0v 29068 df-vs 29069 df-nmcv 29070 df-ims 29071 df-dip 29171 df-ph 29283 |
| This theorem is referenced by: siilem1 29321 ip2eqi 29326 |
| Copyright terms: Public domain | W3C validator |