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

Theorem colinearalglem2 28154
Description: Lemma for colinearalg 28157. 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 1136 . . . 4 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ ๐ด โˆˆ (๐”ผโ€˜๐‘))
2 simpl 483 . . . 4 ((๐‘– โˆˆ (1...๐‘) โˆง ๐‘— โˆˆ (1...๐‘)) โ†’ ๐‘– โˆˆ (1...๐‘))
3 fveecn 28149 . . . 4 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐ดโ€˜๐‘–) โˆˆ โ„‚)
41, 2, 3syl2an 596 . . 3 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (๐‘– โˆˆ (1...๐‘) โˆง ๐‘— โˆˆ (1...๐‘))) โ†’ (๐ดโ€˜๐‘–) โˆˆ โ„‚)
5 simp2 1137 . . . 4 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ ๐ต โˆˆ (๐”ผโ€˜๐‘))
6 fveecn 28149 . . . 4 ((๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐ตโ€˜๐‘–) โˆˆ โ„‚)
75, 2, 6syl2an 596 . . 3 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (๐‘– โˆˆ (1...๐‘) โˆง ๐‘— โˆˆ (1...๐‘))) โ†’ (๐ตโ€˜๐‘–) โˆˆ โ„‚)
8 simp3 1138 . . . 4 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ ๐ถ โˆˆ (๐”ผโ€˜๐‘))
9 fveecn 28149 . . . 4 ((๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐ถโ€˜๐‘–) โˆˆ โ„‚)
108, 2, 9syl2an 596 . . 3 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (๐‘– โˆˆ (1...๐‘) โˆง ๐‘— โˆˆ (1...๐‘))) โ†’ (๐ถโ€˜๐‘–) โˆˆ โ„‚)
11 simpr 485 . . . 4 ((๐‘– โˆˆ (1...๐‘) โˆง ๐‘— โˆˆ (1...๐‘)) โ†’ ๐‘— โˆˆ (1...๐‘))
12 fveecn 28149 . . . 4 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘— โˆˆ (1...๐‘)) โ†’ (๐ดโ€˜๐‘—) โˆˆ โ„‚)
131, 11, 12syl2an 596 . . 3 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (๐‘– โˆˆ (1...๐‘) โˆง ๐‘— โˆˆ (1...๐‘))) โ†’ (๐ดโ€˜๐‘—) โˆˆ โ„‚)
14 fveecn 28149 . . . 4 ((๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘— โˆˆ (1...๐‘)) โ†’ (๐ตโ€˜๐‘—) โˆˆ โ„‚)
155, 11, 14syl2an 596 . . 3 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (๐‘– โˆˆ (1...๐‘) โˆง ๐‘— โˆˆ (1...๐‘))) โ†’ (๐ตโ€˜๐‘—) โˆˆ โ„‚)
16 fveecn 28149 . . . 4 ((๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘— โˆˆ (1...๐‘)) โ†’ (๐ถโ€˜๐‘—) โˆˆ โ„‚)
178, 11, 16syl2an 596 . . 3 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (๐‘– โˆˆ (1...๐‘) โˆง ๐‘— โˆˆ (1...๐‘))) โ†’ (๐ถโ€˜๐‘—) โˆˆ โ„‚)
18 simp1 1136 . . . . . . . . . . . 12 (((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โ†’ (๐ดโ€˜๐‘–) โˆˆ โ„‚)
19 simp3 1138 . . . . . . . . . . . 12 (((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚) โ†’ (๐ถโ€˜๐‘—) โˆˆ โ„‚)
20 mulcl 11190 . . . . . . . . . . . 12 (((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚) โ†’ ((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆˆ โ„‚)
2118, 19, 20syl2an 596 . . . . . . . . . . 11 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆˆ โ„‚)
22 simp2 1137 . . . . . . . . . . . 12 (((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โ†’ (๐ตโ€˜๐‘–) โˆˆ โ„‚)
23 simp1 1136 . . . . . . . . . . . 12 (((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚) โ†’ (๐ดโ€˜๐‘—) โˆˆ โ„‚)
24 mulcl 11190 . . . . . . . . . . . 12 (((๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ดโ€˜๐‘—) โˆˆ โ„‚) โ†’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆˆ โ„‚)
2522, 23, 24syl2an 596 . . . . . . . . . . 11 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆˆ โ„‚)
2621, 25addcld 11229 . . . . . . . . . 10 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆˆ โ„‚)
27 mulcl 11190 . . . . . . . . . . 11 (((๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚) โ†’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆˆ โ„‚)
2822, 19, 27syl2an 596 . . . . . . . . . 10 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆˆ โ„‚)
2926, 28subcld 11567 . . . . . . . . 9 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โˆˆ โ„‚)
30 simp2 1137 . . . . . . . . . 10 (((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚) โ†’ (๐ตโ€˜๐‘—) โˆˆ โ„‚)
31 mulcl 11190 . . . . . . . . . 10 (((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚) โ†’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) โˆˆ โ„‚)
3218, 30, 31syl2an 596 . . . . . . . . 9 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) โˆˆ โ„‚)
33 simp3 1138 . . . . . . . . . . 11 (((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โ†’ (๐ถโ€˜๐‘–) โˆˆ โ„‚)
34 mulcl 11190 . . . . . . . . . . 11 (((๐ถโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ดโ€˜๐‘—) โˆˆ โ„‚) โ†’ ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆˆ โ„‚)
3533, 23, 34syl2an 596 . . . . . . . . . 10 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆˆ โ„‚)
36 mulcl 11190 . . . . . . . . . . 11 (((๐ถโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚) โ†’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) โˆˆ โ„‚)
3733, 30, 36syl2an 596 . . . . . . . . . 10 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) โˆˆ โ„‚)
3835, 37subcld 11567 . . . . . . . . 9 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆˆ โ„‚)
3929, 32, 38subadd2d 11586 . . . . . . . 8 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โ†” ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)))))
40 eqcom 2739 . . . . . . . 8 (((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โ†” ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) = ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))
4139, 40bitrdi 286 . . . . . . 7 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โ†” ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) = ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
4235, 32, 37addsubd 11588 . . . . . . . . 9 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))
4335, 32addcomd 11412 . . . . . . . . . 10 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = (((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))))
4443oveq1d 7420 . . . . . . . . 9 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = ((((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))
4542, 44eqtr3d 2774 . . . . . . . 8 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = ((((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))
4645eqeq2d 2743 . . . . . . 7 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) = ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โ†” ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) = ((((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
4741, 46bitrd 278 . . . . . 6 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โ†” ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) = ((((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
4826, 28, 32subsub4d 11598 . . . . . . . . 9 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
4928, 32addcld 11229 . . . . . . . . . 10 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆˆ โ„‚)
5021, 49, 25subsub3d 11597 . . . . . . . . 9 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ ((((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)))) = ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
5128, 25, 32subsub3d 11597 . . . . . . . . . . . 12 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = ((((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))))
5251eqcomd 2738 . . . . . . . . . . 11 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
5352oveq2d 7421 . . . . . . . . . 10 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ ((((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)))) = (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))))
5425, 32subcld 11567 . . . . . . . . . . 11 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆˆ โ„‚)
5521, 28, 54subsubd 11595 . . . . . . . . . 10 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))) = ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) + (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
5653, 55eqtrd 2772 . . . . . . . . 9 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ ((((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)))) = ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) + (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
5748, 50, 563eqtr2d 2778 . . . . . . . 8 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) + (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
5821, 28subcld 11567 . . . . . . . . 9 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โˆˆ โ„‚)
5958, 25, 32addsub12d 11590 . . . . . . . 8 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) + (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
6021, 28, 32subsub4d 11598 . . . . . . . . 9 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
6160oveq2d 7421 . . . . . . . 8 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))))
6257, 59, 613eqtrd 2776 . . . . . . 7 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))))
6362eqeq1d 2734 . . . . . 6 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โ†” (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
6432, 35addcld 11229 . . . . . . 7 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆˆ โ„‚)
65 subeqrev 11632 . . . . . . 7 ((((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆˆ โ„‚ โˆง ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆˆ โ„‚) โˆง ((((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆˆ โ„‚ โˆง ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) โˆˆ โ„‚)) โ†’ (((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) = ((((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โ†” (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)))) = (((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) โˆ’ (((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))))))
6626, 28, 64, 37, 65syl22anc 837 . . . . . 6 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) = ((((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โ†” (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)))) = (((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) โˆ’ (((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))))))
6747, 63, 663bitr3rd 309 . . . . 5 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)))) = (((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) โˆ’ (((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)))) โ†” (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
6821, 49subcld 11567 . . . . . . . 8 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) โˆˆ โ„‚)
6925, 68, 38addrsub 11627 . . . . . . 7 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โ†” (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)))))
7035, 37, 25sub32d 11599 . . . . . . . . 9 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) = ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))
7135, 25, 37subsub4d 11598 . . . . . . . . 9 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
7270, 71eqtrd 2772 . . . . . . . 8 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
7372eqeq2d 2743 . . . . . . 7 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โ†” (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))))
7469, 73bitrd 278 . . . . . 6 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โ†” (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))))
75 eqcom 2739 . . . . . 6 ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) โ†” (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
7674, 75bitrdi 286 . . . . 5 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โ†” (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))))
7767, 76bitrd 278 . . . 4 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)))) = (((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) โˆ’ (((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)))) โ†” (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))))
78 colinearalglem1 28153 . . . 4 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†” (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)))) = (((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) โˆ’ (((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))))))
79 3anrot 1100 . . . . 5 (((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โ†” ((๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ดโ€˜๐‘–) โˆˆ โ„‚))
80 3anrot 1100 . . . . 5 (((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚) โ†” ((๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ดโ€˜๐‘—) โˆˆ โ„‚))
81 colinearalglem1 28153 . . . . 5 ((((๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ดโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ดโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ†” (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))))
8279, 80, 81syl2anb 598 . . . 4 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ†” (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))))
8377, 78, 823bitr4d 310 . . 3 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†” (((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)))))
844, 7, 10, 13, 15, 17, 83syl33anc 1385 . 2 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (๐‘– โˆˆ (1...๐‘) โˆง ๐‘— โˆˆ (1...๐‘))) โ†’ ((((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†” (((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)))))
85842ralbidva 3216 1 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†” โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)))))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 396   โˆง w3a 1087   = wceq 1541   โˆˆ wcel 2106  โˆ€wral 3061  โ€˜cfv 6540  (class class class)co 7405  โ„‚cc 11104  1c1 11107   + caddc 11109   ยท cmul 11111   โˆ’ cmin 11440  ...cfz 13480  ๐”ผcee 28135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  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
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-po 5587  df-so 5588  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-er 8699  df-map 8818  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-ltxr 11249  df-sub 11442  df-neg 11443  df-ee 28138
This theorem is referenced by:  colinearalglem3  28155  colinearalg  28157
  Copyright terms: Public domain W3C validator