Metamath Proof Explorer

Theorem ipdiri

Description: Distributive law for inner product. Equation I3 of Ponnusamy p. 362. (Contributed by NM, 27-Apr-2007) (New usage is discouraged.)

Ref Expression
Hypotheses ip1i.1 โŠข ๐‘‹ = ( BaseSet โ€˜ ๐‘ˆ )
ip1i.2 โŠข ๐บ = ( +๐‘ฃ โ€˜ ๐‘ˆ )
ip1i.4 โŠข ๐‘† = ( ยท๐‘ OLD โ€˜ ๐‘ˆ )
ip1i.7 โŠข ๐‘ƒ = ( ยท๐‘–OLD โ€˜ ๐‘ˆ )
ip1i.9 โŠข ๐‘ˆ โˆˆ CPreHilOLD
Assertion ipdiri ( ( ๐ด โˆˆ ๐‘‹ โˆง ๐ต โˆˆ ๐‘‹ โˆง ๐ถ โˆˆ ๐‘‹ ) โ†’ ( ( ๐ด ๐บ ๐ต ) ๐‘ƒ ๐ถ ) = ( ( ๐ด ๐‘ƒ ๐ถ ) + ( ๐ต ๐‘ƒ ๐ถ ) ) )

Proof

Step Hyp Ref Expression
1 ip1i.1 โŠข ๐‘‹ = ( BaseSet โ€˜ ๐‘ˆ )
2 ip1i.2 โŠข ๐บ = ( +๐‘ฃ โ€˜ ๐‘ˆ )
3 ip1i.4 โŠข ๐‘† = ( ยท๐‘ OLD โ€˜ ๐‘ˆ )
4 ip1i.7 โŠข ๐‘ƒ = ( ยท๐‘–OLD โ€˜ ๐‘ˆ )
5 ip1i.9 โŠข ๐‘ˆ โˆˆ CPreHilOLD
6 oveq1 โŠข ( ๐ด = if ( ๐ด โˆˆ ๐‘‹ , ๐ด , ( 0vec โ€˜ ๐‘ˆ ) ) โ†’ ( ๐ด ๐บ ๐ต ) = ( if ( ๐ด โˆˆ ๐‘‹ , ๐ด , ( 0vec โ€˜ ๐‘ˆ ) ) ๐บ ๐ต ) )
7 6 oveq1d โŠข ( ๐ด = if ( ๐ด โˆˆ ๐‘‹ , ๐ด , ( 0vec โ€˜ ๐‘ˆ ) ) โ†’ ( ( ๐ด ๐บ ๐ต ) ๐‘ƒ ๐ถ ) = ( ( if ( ๐ด โˆˆ ๐‘‹ , ๐ด , ( 0vec โ€˜ ๐‘ˆ ) ) ๐บ ๐ต ) ๐‘ƒ ๐ถ ) )
8 oveq1 โŠข ( ๐ด = if ( ๐ด โˆˆ ๐‘‹ , ๐ด , ( 0vec โ€˜ ๐‘ˆ ) ) โ†’ ( ๐ด ๐‘ƒ ๐ถ ) = ( if ( ๐ด โˆˆ ๐‘‹ , ๐ด , ( 0vec โ€˜ ๐‘ˆ ) ) ๐‘ƒ ๐ถ ) )
9 8 oveq1d โŠข ( ๐ด = if ( ๐ด โˆˆ ๐‘‹ , ๐ด , ( 0vec โ€˜ ๐‘ˆ ) ) โ†’ ( ( ๐ด ๐‘ƒ ๐ถ ) + ( ๐ต ๐‘ƒ ๐ถ ) ) = ( ( if ( ๐ด โˆˆ ๐‘‹ , ๐ด , ( 0vec โ€˜ ๐‘ˆ ) ) ๐‘ƒ ๐ถ ) + ( ๐ต ๐‘ƒ ๐ถ ) ) )
10 7 9 eqeq12d โŠข ( ๐ด = if ( ๐ด โˆˆ ๐‘‹ , ๐ด , ( 0vec โ€˜ ๐‘ˆ ) ) โ†’ ( ( ( ๐ด ๐บ ๐ต ) ๐‘ƒ ๐ถ ) = ( ( ๐ด ๐‘ƒ ๐ถ ) + ( ๐ต ๐‘ƒ ๐ถ ) ) โ†” ( ( if ( ๐ด โˆˆ ๐‘‹ , ๐ด , ( 0vec โ€˜ ๐‘ˆ ) ) ๐บ ๐ต ) ๐‘ƒ ๐ถ ) = ( ( if ( ๐ด โˆˆ ๐‘‹ , ๐ด , ( 0vec โ€˜ ๐‘ˆ ) ) ๐‘ƒ ๐ถ ) + ( ๐ต ๐‘ƒ ๐ถ ) ) ) )
11 oveq2 โŠข ( ๐ต = if ( ๐ต โˆˆ ๐‘‹ , ๐ต , ( 0vec โ€˜ ๐‘ˆ ) ) โ†’ ( if ( ๐ด โˆˆ ๐‘‹ , ๐ด , ( 0vec โ€˜ ๐‘ˆ ) ) ๐บ ๐ต ) = ( if ( ๐ด โˆˆ ๐‘‹ , ๐ด , ( 0vec โ€˜ ๐‘ˆ ) ) ๐บ if ( ๐ต โˆˆ ๐‘‹ , ๐ต , ( 0vec โ€˜ ๐‘ˆ ) ) ) )
12 11 oveq1d โŠข ( ๐ต = if ( ๐ต โˆˆ ๐‘‹ , ๐ต , ( 0vec โ€˜ ๐‘ˆ ) ) โ†’ ( ( if ( ๐ด โˆˆ ๐‘‹ , ๐ด , ( 0vec โ€˜ ๐‘ˆ ) ) ๐บ ๐ต ) ๐‘ƒ ๐ถ ) = ( ( if ( ๐ด โˆˆ ๐‘‹ , ๐ด , ( 0vec โ€˜ ๐‘ˆ ) ) ๐บ if ( ๐ต โˆˆ ๐‘‹ , ๐ต , ( 0vec โ€˜ ๐‘ˆ ) ) ) ๐‘ƒ ๐ถ ) )
13 oveq1 โŠข ( ๐ต = if ( ๐ต โˆˆ ๐‘‹ , ๐ต , ( 0vec โ€˜ ๐‘ˆ ) ) โ†’ ( ๐ต ๐‘ƒ ๐ถ ) = ( if ( ๐ต โˆˆ ๐‘‹ , ๐ต , ( 0vec โ€˜ ๐‘ˆ ) ) ๐‘ƒ ๐ถ ) )
14 13 oveq2d โŠข ( ๐ต = if ( ๐ต โˆˆ ๐‘‹ , ๐ต , ( 0vec โ€˜ ๐‘ˆ ) ) โ†’ ( ( if ( ๐ด โˆˆ ๐‘‹ , ๐ด , ( 0vec โ€˜ ๐‘ˆ ) ) ๐‘ƒ ๐ถ ) + ( ๐ต ๐‘ƒ ๐ถ ) ) = ( ( if ( ๐ด โˆˆ ๐‘‹ , ๐ด , ( 0vec โ€˜ ๐‘ˆ ) ) ๐‘ƒ ๐ถ ) + ( if ( ๐ต โˆˆ ๐‘‹ , ๐ต , ( 0vec โ€˜ ๐‘ˆ ) ) ๐‘ƒ ๐ถ ) ) )
15 12 14 eqeq12d โŠข ( ๐ต = if ( ๐ต โˆˆ ๐‘‹ , ๐ต , ( 0vec โ€˜ ๐‘ˆ ) ) โ†’ ( ( ( if ( ๐ด โˆˆ ๐‘‹ , ๐ด , ( 0vec โ€˜ ๐‘ˆ ) ) ๐บ ๐ต ) ๐‘ƒ ๐ถ ) = ( ( if ( ๐ด โˆˆ ๐‘‹ , ๐ด , ( 0vec โ€˜ ๐‘ˆ ) ) ๐‘ƒ ๐ถ ) + ( ๐ต ๐‘ƒ ๐ถ ) ) โ†” ( ( if ( ๐ด โˆˆ ๐‘‹ , ๐ด , ( 0vec โ€˜ ๐‘ˆ ) ) ๐บ if ( ๐ต โˆˆ ๐‘‹ , ๐ต , ( 0vec โ€˜ ๐‘ˆ ) ) ) ๐‘ƒ ๐ถ ) = ( ( if ( ๐ด โˆˆ ๐‘‹ , ๐ด , ( 0vec โ€˜ ๐‘ˆ ) ) ๐‘ƒ ๐ถ ) + ( if ( ๐ต โˆˆ ๐‘‹ , ๐ต , ( 0vec โ€˜ ๐‘ˆ ) ) ๐‘ƒ ๐ถ ) ) ) )
16 oveq2 โŠข ( ๐ถ = if ( ๐ถ โˆˆ ๐‘‹ , ๐ถ , ( 0vec โ€˜ ๐‘ˆ ) ) โ†’ ( ( if ( ๐ด โˆˆ ๐‘‹ , ๐ด , ( 0vec โ€˜ ๐‘ˆ ) ) ๐บ if ( ๐ต โˆˆ ๐‘‹ , ๐ต , ( 0vec โ€˜ ๐‘ˆ ) ) ) ๐‘ƒ ๐ถ ) = ( ( if ( ๐ด โˆˆ ๐‘‹ , ๐ด , ( 0vec โ€˜ ๐‘ˆ ) ) ๐บ if ( ๐ต โˆˆ ๐‘‹ , ๐ต , ( 0vec โ€˜ ๐‘ˆ ) ) ) ๐‘ƒ if ( ๐ถ โˆˆ ๐‘‹ , ๐ถ , ( 0vec โ€˜ ๐‘ˆ ) ) ) )
17 oveq2 โŠข ( ๐ถ = if ( ๐ถ โˆˆ ๐‘‹ , ๐ถ , ( 0vec โ€˜ ๐‘ˆ ) ) โ†’ ( if ( ๐ด โˆˆ ๐‘‹ , ๐ด , ( 0vec โ€˜ ๐‘ˆ ) ) ๐‘ƒ ๐ถ ) = ( if ( ๐ด โˆˆ ๐‘‹ , ๐ด , ( 0vec โ€˜ ๐‘ˆ ) ) ๐‘ƒ if ( ๐ถ โˆˆ ๐‘‹ , ๐ถ , ( 0vec โ€˜ ๐‘ˆ ) ) ) )
18 oveq2 โŠข ( ๐ถ = if ( ๐ถ โˆˆ ๐‘‹ , ๐ถ , ( 0vec โ€˜ ๐‘ˆ ) ) โ†’ ( if ( ๐ต โˆˆ ๐‘‹ , ๐ต , ( 0vec โ€˜ ๐‘ˆ ) ) ๐‘ƒ ๐ถ ) = ( if ( ๐ต โˆˆ ๐‘‹ , ๐ต , ( 0vec โ€˜ ๐‘ˆ ) ) ๐‘ƒ if ( ๐ถ โˆˆ ๐‘‹ , ๐ถ , ( 0vec โ€˜ ๐‘ˆ ) ) ) )
19 17 18 oveq12d โŠข ( ๐ถ = if ( ๐ถ โˆˆ ๐‘‹ , ๐ถ , ( 0vec โ€˜ ๐‘ˆ ) ) โ†’ ( ( if ( ๐ด โˆˆ ๐‘‹ , ๐ด , ( 0vec โ€˜ ๐‘ˆ ) ) ๐‘ƒ ๐ถ ) + ( if ( ๐ต โˆˆ ๐‘‹ , ๐ต , ( 0vec โ€˜ ๐‘ˆ ) ) ๐‘ƒ ๐ถ ) ) = ( ( if ( ๐ด โˆˆ ๐‘‹ , ๐ด , ( 0vec โ€˜ ๐‘ˆ ) ) ๐‘ƒ if ( ๐ถ โˆˆ ๐‘‹ , ๐ถ , ( 0vec โ€˜ ๐‘ˆ ) ) ) + ( if ( ๐ต โˆˆ ๐‘‹ , ๐ต , ( 0vec โ€˜ ๐‘ˆ ) ) ๐‘ƒ if ( ๐ถ โˆˆ ๐‘‹ , ๐ถ , ( 0vec โ€˜ ๐‘ˆ ) ) ) ) )
20 16 19 eqeq12d โŠข ( ๐ถ = if ( ๐ถ โˆˆ ๐‘‹ , ๐ถ , ( 0vec โ€˜ ๐‘ˆ ) ) โ†’ ( ( ( if ( ๐ด โˆˆ ๐‘‹ , ๐ด , ( 0vec โ€˜ ๐‘ˆ ) ) ๐บ if ( ๐ต โˆˆ ๐‘‹ , ๐ต , ( 0vec โ€˜ ๐‘ˆ ) ) ) ๐‘ƒ ๐ถ ) = ( ( if ( ๐ด โˆˆ ๐‘‹ , ๐ด , ( 0vec โ€˜ ๐‘ˆ ) ) ๐‘ƒ ๐ถ ) + ( if ( ๐ต โˆˆ ๐‘‹ , ๐ต , ( 0vec โ€˜ ๐‘ˆ ) ) ๐‘ƒ ๐ถ ) ) โ†” ( ( if ( ๐ด โˆˆ ๐‘‹ , ๐ด , ( 0vec โ€˜ ๐‘ˆ ) ) ๐บ if ( ๐ต โˆˆ ๐‘‹ , ๐ต , ( 0vec โ€˜ ๐‘ˆ ) ) ) ๐‘ƒ if ( ๐ถ โˆˆ ๐‘‹ , ๐ถ , ( 0vec โ€˜ ๐‘ˆ ) ) ) = ( ( if ( ๐ด โˆˆ ๐‘‹ , ๐ด , ( 0vec โ€˜ ๐‘ˆ ) ) ๐‘ƒ if ( ๐ถ โˆˆ ๐‘‹ , ๐ถ , ( 0vec โ€˜ ๐‘ˆ ) ) ) + ( if ( ๐ต โˆˆ ๐‘‹ , ๐ต , ( 0vec โ€˜ ๐‘ˆ ) ) ๐‘ƒ if ( ๐ถ โˆˆ ๐‘‹ , ๐ถ , ( 0vec โ€˜ ๐‘ˆ ) ) ) ) ) )
21 eqid โŠข ( 0vec โ€˜ ๐‘ˆ ) = ( 0vec โ€˜ ๐‘ˆ )
22 1 21 5 elimph โŠข if ( ๐ด โˆˆ ๐‘‹ , ๐ด , ( 0vec โ€˜ ๐‘ˆ ) ) โˆˆ ๐‘‹
23 1 21 5 elimph โŠข if ( ๐ต โˆˆ ๐‘‹ , ๐ต , ( 0vec โ€˜ ๐‘ˆ ) ) โˆˆ ๐‘‹
24 1 21 5 elimph โŠข if ( ๐ถ โˆˆ ๐‘‹ , ๐ถ , ( 0vec โ€˜ ๐‘ˆ ) ) โˆˆ ๐‘‹
25 1 2 3 4 5 22 23 24 ipdirilem โŠข ( ( if ( ๐ด โˆˆ ๐‘‹ , ๐ด , ( 0vec โ€˜ ๐‘ˆ ) ) ๐บ if ( ๐ต โˆˆ ๐‘‹ , ๐ต , ( 0vec โ€˜ ๐‘ˆ ) ) ) ๐‘ƒ if ( ๐ถ โˆˆ ๐‘‹ , ๐ถ , ( 0vec โ€˜ ๐‘ˆ ) ) ) = ( ( if ( ๐ด โˆˆ ๐‘‹ , ๐ด , ( 0vec โ€˜ ๐‘ˆ ) ) ๐‘ƒ if ( ๐ถ โˆˆ ๐‘‹ , ๐ถ , ( 0vec โ€˜ ๐‘ˆ ) ) ) + ( if ( ๐ต โˆˆ ๐‘‹ , ๐ต , ( 0vec โ€˜ ๐‘ˆ ) ) ๐‘ƒ if ( ๐ถ โˆˆ ๐‘‹ , ๐ถ , ( 0vec โ€˜ ๐‘ˆ ) ) ) )
26 10 15 20 25 dedth3h โŠข ( ( ๐ด โˆˆ ๐‘‹ โˆง ๐ต โˆˆ ๐‘‹ โˆง ๐ถ โˆˆ ๐‘‹ ) โ†’ ( ( ๐ด ๐บ ๐ต ) ๐‘ƒ ๐ถ ) = ( ( ๐ด ๐‘ƒ ๐ถ ) + ( ๐ต ๐‘ƒ ๐ถ ) ) )