dipass - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > dipass		Structured version Visualization version GIF version

Theorem dipass 31208

Description: Associative law for inner product. Equation I2 of [Ponnusamy] p. 363. (Contributed by NM, 25-Aug-2007.) (New usage is discouraged.)

**Hypotheses**
Ref	Expression
ipass.1	⊢ 𝑋 = (BaseSet‘𝑈)
ipass.4	⊢ 𝑆 = ( ·_𝑠OLD ‘𝑈)
ipass.7	⊢ 𝑃 = (·_𝑖OLD‘𝑈)

**Assertion**
Ref	Expression
dipass	⊢ ((𝑈 ∈ CPreHil_OLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝑆𝐵)𝑃𝐶) = (𝐴 · (𝐵𝑃𝐶)))

**Proof of Theorem dipass**
Step	Hyp	Ref	Expression
1		ipass.1	. . . . . . 7 ⊢ 𝑋 = (BaseSet‘𝑈)
2		fveq2 6881	. . . . . . 7 ⊢ (𝑈 = if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩) → (BaseSet‘𝑈) = (BaseSet‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩)))
3	1, 2	eqtrid 2809	. . . . . 6 ⊢ (𝑈 = if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩) → 𝑋 = (BaseSet‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩)))
4	3	eleq2d 2848	. . . . 5 ⊢ (𝑈 = if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩) → (𝐵 ∈ 𝑋 ↔ 𝐵 ∈ (BaseSet‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩))))
5	3	eleq2d 2848	. . . . 5 ⊢ (𝑈 = if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩) → (𝐶 ∈ 𝑋 ↔ 𝐶 ∈ (BaseSet‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩))))
6	4, 5	3anbi23d 1466	. . . 4 ⊢ (𝑈 = if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩) → ((𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) ↔ (𝐴 ∈ ℂ ∧ 𝐵 ∈ (BaseSet‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩)) ∧ 𝐶 ∈ (BaseSet‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩)))))
7		ipass.4	. . . . . . . . 9 ⊢ 𝑆 = ( ·_𝑠OLD ‘𝑈)
8		fveq2 6881	. . . . . . . . 9 ⊢ (𝑈 = if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩) → ( ·_𝑠OLD ‘𝑈) = ( ·_𝑠OLD ‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩)))
9	7, 8	eqtrid 2809	. . . . . . . 8 ⊢ (𝑈 = if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩) → 𝑆 = ( ·_𝑠OLD ‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩)))
10	9	oveqd 7429	. . . . . . 7 ⊢ (𝑈 = if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩) → (𝐴𝑆𝐵) = (𝐴( ·_𝑠OLD ‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩))𝐵))
11	10	oveq1d 7427	. . . . . 6 ⊢ (𝑈 = if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩) → ((𝐴𝑆𝐵)𝑃𝐶) = ((𝐴( ·_𝑠OLD ‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩))𝐵)𝑃𝐶))
12		ipass.7	. . . . . . . 8 ⊢ 𝑃 = (·_𝑖OLD‘𝑈)
13		fveq2 6881	. . . . . . . 8 ⊢ (𝑈 = if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩) → (·_𝑖OLD‘𝑈) = (·_𝑖OLD‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩)))
14	12, 13	eqtrid 2809	. . . . . . 7 ⊢ (𝑈 = if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩) → 𝑃 = (·_𝑖OLD‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩)))
15	14	oveqd 7429	. . . . . 6 ⊢ (𝑈 = if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩) → ((𝐴( ·_𝑠OLD ‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩))𝐵)𝑃𝐶) = ((𝐴( ·_𝑠OLD ‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩))𝐵)(·_𝑖OLD‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩))𝐶))
16	11, 15	eqtrd 2797	. . . . 5 ⊢ (𝑈 = if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩) → ((𝐴𝑆𝐵)𝑃𝐶) = ((𝐴( ·_𝑠OLD ‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩))𝐵)(·_𝑖OLD‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩))𝐶))
17	14	oveqd 7429	. . . . . 6 ⊢ (𝑈 = if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩) → (𝐵𝑃𝐶) = (𝐵(·_𝑖OLD‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩))𝐶))
18	17	oveq2d 7428	. . . . 5 ⊢ (𝑈 = if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩) → (𝐴 · (𝐵𝑃𝐶)) = (𝐴 · (𝐵(·_𝑖OLD‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩))𝐶)))
19	16, 18	eqeq12d 2778	. . . 4 ⊢ (𝑈 = if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩) → (((𝐴𝑆𝐵)𝑃𝐶) = (𝐴 · (𝐵𝑃𝐶)) ↔ ((𝐴( ·_𝑠OLD ‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩))𝐵)(·_𝑖OLD‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩))𝐶) = (𝐴 · (𝐵(·_𝑖OLD‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩))𝐶))))
20	6, 19	imbi12d 347	. . 3 ⊢ (𝑈 = if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩) → (((𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ((𝐴𝑆𝐵)𝑃𝐶) = (𝐴 · (𝐵𝑃𝐶))) ↔ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ (BaseSet‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩)) ∧ 𝐶 ∈ (BaseSet‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩))) → ((𝐴( ·_𝑠OLD ‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩))𝐵)(·_𝑖OLD‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩))𝐶) = (𝐴 · (𝐵(·_𝑖OLD‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩))𝐶)))))
21		eqid 2762	. . . 4 ⊢ (BaseSet‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩)) = (BaseSet‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩))
22		eqid 2762	. . . 4 ⊢ ( +_𝑣 ‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩)) = ( +_𝑣 ‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩))
23		eqid 2762	. . . 4 ⊢ ( ·_𝑠OLD ‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩)) = ( ·_𝑠OLD ‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩))
24		eqid 2762	. . . 4 ⊢ (·_𝑖OLD‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩)) = (·_𝑖OLD‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩))
25		elimphu 31184	. . . 4 ⊢ if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩) ∈ CPreHil_OLD
26	21, 22, 23, 24, 25	ipassi 31204	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ (BaseSet‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩)) ∧ 𝐶 ∈ (BaseSet‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩))) → ((𝐴( ·_𝑠OLD ‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩))𝐵)(·_𝑖OLD‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩))𝐶) = (𝐴 · (𝐵(·_𝑖OLD‘if(𝑈 ∈ CPreHil_OLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩))𝐶)))
27	20, 26	dedth 4545	. 2 ⊢ (𝑈 ∈ CPreHil_OLD → ((𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ((𝐴𝑆𝐵)𝑃𝐶) = (𝐴 · (𝐵𝑃𝐶))))
28	27	imp 411	1 ⊢ ((𝑈 ∈ CPreHil_OLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝑆𝐵)𝑃𝐶) = (𝐴 · (𝐵𝑃𝐶)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 400 ∧ w3a 1102 = wceq 1569 ∈ wcel 2142 ifcif 4486 ⟨cop 4594 ‘cfv 6536 (class class class)co 7412 ℂcc 11104 + caddc 11109 · cmul 11111 abscabs 15292 +_𝑣 cpv 30948 BaseSetcba 30949 ·_𝑠OLD cns 30950 ·_𝑖OLDcdip 31063 CPreHil_OLDccphlo 31175

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1824 ax-4 1838 ax-5 1939 ax-6 1996 ax-7 2037 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5237 ax-sep 5256 ax-nul 5268 ax-pow 5335 ax-pr 5403 ax-un 7734 ax-inf2 9608 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183 ax-pre-sup 11184 ax-addf 11185 ax-mulf 11186

This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1103 df-3an 1104 df-tru 1572 df-fal 1582 df-ex 1809 df-nf 1813 df-sb 2096 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3368 df-reu 3369 df-rab 3416 df-v 3456 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4595 df-uni 4872 df-int 4912 df-iun 4957 df-iin 4958 df-br 5109 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5555 df-eprel 5560 df-po 5568 df-so 5569 df-fr 5613 df-se 5614 df-we 5615 df-xp 5666 df-rel 5667 df-cnv 5668 df-co 5669 df-dm 5670 df-rn 5671 df-res 5672 df-ima 5673 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-of 7676 df-om 7861 df-1st 7984 df-2nd 7985 df-supp 8155 df-frecs 8276 df-wrecs 8307 df-recs 8356 df-rdg 8395 df-1o 8451 df-2o 8452 df-er 8692 df-map 8824 df-ixp 8894 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-fsupp 9320 df-fi 9369 df-sup 9400 df-inf 9401 df-oi 9470 df-card 9932 df-pnf 11251 df-mnf 11252 df-xr 11253 df-ltxr 11254 df-le 11255 df-sub 11449 df-neg 11450 df-div 11878 df-nn 12240 df-2 12309 df-3 12310 df-4 12311 df-5 12312 df-6 12313 df-7 12314 df-8 12315 df-9 12316 df-n0 12511 df-z 12598 df-dec 12718 df-uz 12869 df-q 12979 df-rp 13023 df-xneg 13143 df-xadd 13144 df-xmul 13145 df-ioo 13382 df-icc 13385 df-fz 13542 df-fzo 13690 df-seq 14045 df-exp 14105 df-hash 14374 df-cj 15157 df-re 15158 df-im 15159 df-sqrt 15293 df-abs 15294 df-clim 15546 df-sum 15745 df-struct 17213 df-sets 17230 df-slot 17248 df-ndx 17260 df-base 17276 df-ress 17297 df-plusg 17329 df-mulr 17330 df-starv 17331 df-sca 17332 df-vsca 17333 df-ip 17334 df-tset 17335 df-ple 17336 df-ds 17338 df-unif 17339 df-hom 17340 df-cco 17341 df-rest 17481 df-topn 17482 df-0g 17500 df-gsum 17501 df-topgen 17502 df-pt 17503 df-prds 17506 df-xrs 17562 df-qtop 17567 df-imas 17568 df-xps 17570 df-mre 17644 df-mrc 17645 df-acs 17647 df-mgm 18704 df-sgrp 18783 df-mnd 18799 df-submnd 18848 df-mulg 19140 df-cntz 19393 df-cmn 19858 df-psmet 21525 df-xmet 21526 df-met 21527 df-bl 21528 df-mopn 21529 df-cnfld 21534 df-top 23062 df-topon 23079 df-topsp 23101 df-bases 23114 df-cld 23187 df-ntr 23188 df-cls 23189 df-cn 23395 df-cnp 23396 df-t1 23482 df-haus 23483 df-tx 23730 df-hmeo 23923 df-xms 24488 df-ms 24489 df-tms 24490 df-grpo 30856 df-gid 30857 df-ginv 30858 df-gdiv 30859 df-ablo 30908 df-vc 30922 df-nv 30955 df-va 30958 df-ba 30959 df-sm 30960 df-0v 30961 df-vs 30962 df-nmcv 30963 df-ims 30964 df-dip 31064 df-ph 31176

This theorem is used by: dipassr 31209 dipsubdir 31211 siilem1 31214 hlipass 31276

W3C validator