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

Theorem colinearalglem2 28430
Description: Lemma for colinearalg 28433. Translate between two forms of the colinearity condition. (Contributed by Scott Fenton, 24-Jun-2013.)
Assertion
Ref Expression
colinearalglem2 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†” โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)))))
Distinct variable groups:   ๐ด,๐‘–,๐‘—   ๐ต,๐‘–,๐‘—   ๐ถ,๐‘–,๐‘—   ๐‘–,๐‘,๐‘—

Proof of Theorem colinearalglem2
StepHypRef Expression
1 simp1 1134 . . . 4 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ ๐ด โˆˆ (๐”ผโ€˜๐‘))
2 simpl 481 . . . 4 ((๐‘– โˆˆ (1...๐‘) โˆง ๐‘— โˆˆ (1...๐‘)) โ†’ ๐‘– โˆˆ (1...๐‘))
3 fveecn 28425 . . . 4 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐ดโ€˜๐‘–) โˆˆ โ„‚)
41, 2, 3syl2an 594 . . 3 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (๐‘– โˆˆ (1...๐‘) โˆง ๐‘— โˆˆ (1...๐‘))) โ†’ (๐ดโ€˜๐‘–) โˆˆ โ„‚)
5 simp2 1135 . . . 4 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ ๐ต โˆˆ (๐”ผโ€˜๐‘))
6 fveecn 28425 . . . 4 ((๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐ตโ€˜๐‘–) โˆˆ โ„‚)
75, 2, 6syl2an 594 . . 3 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (๐‘– โˆˆ (1...๐‘) โˆง ๐‘— โˆˆ (1...๐‘))) โ†’ (๐ตโ€˜๐‘–) โˆˆ โ„‚)
8 simp3 1136 . . . 4 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ ๐ถ โˆˆ (๐”ผโ€˜๐‘))
9 fveecn 28425 . . . 4 ((๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐ถโ€˜๐‘–) โˆˆ โ„‚)
108, 2, 9syl2an 594 . . 3 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (๐‘– โˆˆ (1...๐‘) โˆง ๐‘— โˆˆ (1...๐‘))) โ†’ (๐ถโ€˜๐‘–) โˆˆ โ„‚)
11 simpr 483 . . . 4 ((๐‘– โˆˆ (1...๐‘) โˆง ๐‘— โˆˆ (1...๐‘)) โ†’ ๐‘— โˆˆ (1...๐‘))
12 fveecn 28425 . . . 4 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘— โˆˆ (1...๐‘)) โ†’ (๐ดโ€˜๐‘—) โˆˆ โ„‚)
131, 11, 12syl2an 594 . . 3 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (๐‘– โˆˆ (1...๐‘) โˆง ๐‘— โˆˆ (1...๐‘))) โ†’ (๐ดโ€˜๐‘—) โˆˆ โ„‚)
14 fveecn 28425 . . . 4 ((๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘— โˆˆ (1...๐‘)) โ†’ (๐ตโ€˜๐‘—) โˆˆ โ„‚)
155, 11, 14syl2an 594 . . 3 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (๐‘– โˆˆ (1...๐‘) โˆง ๐‘— โˆˆ (1...๐‘))) โ†’ (๐ตโ€˜๐‘—) โˆˆ โ„‚)
16 fveecn 28425 . . . 4 ((๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘— โˆˆ (1...๐‘)) โ†’ (๐ถโ€˜๐‘—) โˆˆ โ„‚)
178, 11, 16syl2an 594 . . 3 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (๐‘– โˆˆ (1...๐‘) โˆง ๐‘— โˆˆ (1...๐‘))) โ†’ (๐ถโ€˜๐‘—) โˆˆ โ„‚)
18 simp1 1134 . . . . . . . . . . . 12 (((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โ†’ (๐ดโ€˜๐‘–) โˆˆ โ„‚)
19 simp3 1136 . . . . . . . . . . . 12 (((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚) โ†’ (๐ถโ€˜๐‘—) โˆˆ โ„‚)
20 mulcl 11198 . . . . . . . . . . . 12 (((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚) โ†’ ((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆˆ โ„‚)
2118, 19, 20syl2an 594 . . . . . . . . . . 11 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆˆ โ„‚)
22 simp2 1135 . . . . . . . . . . . 12 (((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โ†’ (๐ตโ€˜๐‘–) โˆˆ โ„‚)
23 simp1 1134 . . . . . . . . . . . 12 (((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚) โ†’ (๐ดโ€˜๐‘—) โˆˆ โ„‚)
24 mulcl 11198 . . . . . . . . . . . 12 (((๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ดโ€˜๐‘—) โˆˆ โ„‚) โ†’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆˆ โ„‚)
2522, 23, 24syl2an 594 . . . . . . . . . . 11 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆˆ โ„‚)
2621, 25addcld 11239 . . . . . . . . . 10 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆˆ โ„‚)
27 mulcl 11198 . . . . . . . . . . 11 (((๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚) โ†’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆˆ โ„‚)
2822, 19, 27syl2an 594 . . . . . . . . . 10 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆˆ โ„‚)
2926, 28subcld 11577 . . . . . . . . 9 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โˆˆ โ„‚)
30 simp2 1135 . . . . . . . . . 10 (((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚) โ†’ (๐ตโ€˜๐‘—) โˆˆ โ„‚)
31 mulcl 11198 . . . . . . . . . 10 (((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚) โ†’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) โˆˆ โ„‚)
3218, 30, 31syl2an 594 . . . . . . . . 9 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) โˆˆ โ„‚)
33 simp3 1136 . . . . . . . . . . 11 (((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โ†’ (๐ถโ€˜๐‘–) โˆˆ โ„‚)
34 mulcl 11198 . . . . . . . . . . 11 (((๐ถโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ดโ€˜๐‘—) โˆˆ โ„‚) โ†’ ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆˆ โ„‚)
3533, 23, 34syl2an 594 . . . . . . . . . 10 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆˆ โ„‚)
36 mulcl 11198 . . . . . . . . . . 11 (((๐ถโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚) โ†’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) โˆˆ โ„‚)
3733, 30, 36syl2an 594 . . . . . . . . . 10 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) โˆˆ โ„‚)
3835, 37subcld 11577 . . . . . . . . 9 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆˆ โ„‚)
3929, 32, 38subadd2d 11596 . . . . . . . 8 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โ†” ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)))))
40 eqcom 2737 . . . . . . . 8 (((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โ†” ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) = ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))
4139, 40bitrdi 286 . . . . . . 7 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โ†” ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) = ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
4235, 32, 37addsubd 11598 . . . . . . . . 9 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))
4335, 32addcomd 11422 . . . . . . . . . 10 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = (((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))))
4443oveq1d 7428 . . . . . . . . 9 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = ((((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))
4542, 44eqtr3d 2772 . . . . . . . 8 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = ((((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))
4645eqeq2d 2741 . . . . . . 7 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) = ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โ†” ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) = ((((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
4741, 46bitrd 278 . . . . . 6 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โ†” ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) = ((((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
4826, 28, 32subsub4d 11608 . . . . . . . . 9 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
4928, 32addcld 11239 . . . . . . . . . 10 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆˆ โ„‚)
5021, 49, 25subsub3d 11607 . . . . . . . . 9 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ ((((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)))) = ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
5128, 25, 32subsub3d 11607 . . . . . . . . . . . 12 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = ((((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))))
5251eqcomd 2736 . . . . . . . . . . 11 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
5352oveq2d 7429 . . . . . . . . . 10 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ ((((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)))) = (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))))
5425, 32subcld 11577 . . . . . . . . . . 11 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆˆ โ„‚)
5521, 28, 54subsubd 11605 . . . . . . . . . 10 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))) = ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) + (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
5653, 55eqtrd 2770 . . . . . . . . 9 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ ((((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)))) = ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) + (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
5748, 50, 563eqtr2d 2776 . . . . . . . 8 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) + (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
5821, 28subcld 11577 . . . . . . . . 9 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โˆˆ โ„‚)
5958, 25, 32addsub12d 11600 . . . . . . . 8 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) + (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
6021, 28, 32subsub4d 11608 . . . . . . . . 9 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
6160oveq2d 7429 . . . . . . . 8 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))))
6257, 59, 613eqtrd 2774 . . . . . . 7 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))))
6362eqeq1d 2732 . . . . . 6 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โ†” (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
6432, 35addcld 11239 . . . . . . 7 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆˆ โ„‚)
65 subeqrev 11642 . . . . . . 7 ((((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆˆ โ„‚ โˆง ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆˆ โ„‚) โˆง ((((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆˆ โ„‚ โˆง ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) โˆˆ โ„‚)) โ†’ (((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) = ((((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โ†” (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)))) = (((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) โˆ’ (((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))))))
6626, 28, 64, 37, 65syl22anc 835 . . . . . 6 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) = ((((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โ†” (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)))) = (((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) โˆ’ (((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))))))
6747, 63, 663bitr3rd 309 . . . . 5 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)))) = (((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) โˆ’ (((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)))) โ†” (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
6821, 49subcld 11577 . . . . . . . 8 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) โˆˆ โ„‚)
6925, 68, 38addrsub 11637 . . . . . . 7 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โ†” (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)))))
7035, 37, 25sub32d 11609 . . . . . . . . 9 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) = ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))
7135, 25, 37subsub4d 11608 . . . . . . . . 9 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
7270, 71eqtrd 2770 . . . . . . . 8 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
7372eqeq2d 2741 . . . . . . 7 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โ†” (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))))
7469, 73bitrd 278 . . . . . 6 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โ†” (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))))
75 eqcom 2737 . . . . . 6 ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) โ†” (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
7674, 75bitrdi 286 . . . . 5 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โ†” (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))))
7767, 76bitrd 278 . . . 4 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)))) = (((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) โˆ’ (((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)))) โ†” (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))))
78 colinearalglem1 28429 . . . 4 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†” (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)))) = (((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) โˆ’ (((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))))))
79 3anrot 1098 . . . . 5 (((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โ†” ((๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ดโ€˜๐‘–) โˆˆ โ„‚))
80 3anrot 1098 . . . . 5 (((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚) โ†” ((๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ดโ€˜๐‘—) โˆˆ โ„‚))
81 colinearalglem1 28429 . . . . 5 ((((๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ดโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ดโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ†” (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))))
8279, 80, 81syl2anb 596 . . . 4 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ†” (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))))
8377, 78, 823bitr4d 310 . . 3 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†” (((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)))))
844, 7, 10, 13, 15, 17, 83syl33anc 1383 . 2 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (๐‘– โˆˆ (1...๐‘) โˆง ๐‘— โˆˆ (1...๐‘))) โ†’ ((((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†” (((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)))))
85842ralbidva 3214 1 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†” โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)))))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 394   โˆง w3a 1085   = wceq 1539   โˆˆ wcel 2104  โˆ€wral 3059  โ€˜cfv 6544  (class class class)co 7413  โ„‚cc 11112  1c1 11115   + caddc 11117   ยท cmul 11119   โˆ’ cmin 11450  ...cfz 13490  ๐”ผcee 28411
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7729  ax-cnex 11170  ax-resscn 11171  ax-1cn 11172  ax-icn 11173  ax-addcl 11174  ax-addrcl 11175  ax-mulcl 11176  ax-mulrcl 11177  ax-mulcom 11178  ax-addass 11179  ax-mulass 11180  ax-distr 11181  ax-i2m1 11182  ax-1ne0 11183  ax-1rid 11184  ax-rnegex 11185  ax-rrecex 11186  ax-cnre 11187  ax-pre-lttri 11188  ax-pre-lttrn 11189  ax-pre-ltadd 11190
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-po 5589  df-so 5590  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7369  df-ov 7416  df-oprab 7417  df-mpo 7418  df-er 8707  df-map 8826  df-en 8944  df-dom 8945  df-sdom 8946  df-pnf 11256  df-mnf 11257  df-ltxr 11259  df-sub 11452  df-neg 11453  df-ee 28414
This theorem is referenced by:  colinearalglem3  28431  colinearalg  28433
  Copyright terms: Public domain W3C validator