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

Theorem colinearalglem2 28165
Description: Lemma for colinearalg 28168. 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 1137 . . . 4 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ ๐ด โˆˆ (๐”ผโ€˜๐‘))
2 simpl 484 . . . 4 ((๐‘– โˆˆ (1...๐‘) โˆง ๐‘— โˆˆ (1...๐‘)) โ†’ ๐‘– โˆˆ (1...๐‘))
3 fveecn 28160 . . . 4 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐ดโ€˜๐‘–) โˆˆ โ„‚)
41, 2, 3syl2an 597 . . 3 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (๐‘– โˆˆ (1...๐‘) โˆง ๐‘— โˆˆ (1...๐‘))) โ†’ (๐ดโ€˜๐‘–) โˆˆ โ„‚)
5 simp2 1138 . . . 4 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ ๐ต โˆˆ (๐”ผโ€˜๐‘))
6 fveecn 28160 . . . 4 ((๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐ตโ€˜๐‘–) โˆˆ โ„‚)
75, 2, 6syl2an 597 . . 3 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (๐‘– โˆˆ (1...๐‘) โˆง ๐‘— โˆˆ (1...๐‘))) โ†’ (๐ตโ€˜๐‘–) โˆˆ โ„‚)
8 simp3 1139 . . . 4 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ ๐ถ โˆˆ (๐”ผโ€˜๐‘))
9 fveecn 28160 . . . 4 ((๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘– โˆˆ (1...๐‘)) โ†’ (๐ถโ€˜๐‘–) โˆˆ โ„‚)
108, 2, 9syl2an 597 . . 3 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (๐‘– โˆˆ (1...๐‘) โˆง ๐‘— โˆˆ (1...๐‘))) โ†’ (๐ถโ€˜๐‘–) โˆˆ โ„‚)
11 simpr 486 . . . 4 ((๐‘– โˆˆ (1...๐‘) โˆง ๐‘— โˆˆ (1...๐‘)) โ†’ ๐‘— โˆˆ (1...๐‘))
12 fveecn 28160 . . . 4 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘— โˆˆ (1...๐‘)) โ†’ (๐ดโ€˜๐‘—) โˆˆ โ„‚)
131, 11, 12syl2an 597 . . 3 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (๐‘– โˆˆ (1...๐‘) โˆง ๐‘— โˆˆ (1...๐‘))) โ†’ (๐ดโ€˜๐‘—) โˆˆ โ„‚)
14 fveecn 28160 . . . 4 ((๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘— โˆˆ (1...๐‘)) โ†’ (๐ตโ€˜๐‘—) โˆˆ โ„‚)
155, 11, 14syl2an 597 . . 3 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (๐‘– โˆˆ (1...๐‘) โˆง ๐‘— โˆˆ (1...๐‘))) โ†’ (๐ตโ€˜๐‘—) โˆˆ โ„‚)
16 fveecn 28160 . . . 4 ((๐ถ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘— โˆˆ (1...๐‘)) โ†’ (๐ถโ€˜๐‘—) โˆˆ โ„‚)
178, 11, 16syl2an 597 . . 3 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (๐‘– โˆˆ (1...๐‘) โˆง ๐‘— โˆˆ (1...๐‘))) โ†’ (๐ถโ€˜๐‘—) โˆˆ โ„‚)
18 simp1 1137 . . . . . . . . . . . 12 (((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โ†’ (๐ดโ€˜๐‘–) โˆˆ โ„‚)
19 simp3 1139 . . . . . . . . . . . 12 (((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚) โ†’ (๐ถโ€˜๐‘—) โˆˆ โ„‚)
20 mulcl 11194 . . . . . . . . . . . 12 (((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚) โ†’ ((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆˆ โ„‚)
2118, 19, 20syl2an 597 . . . . . . . . . . 11 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆˆ โ„‚)
22 simp2 1138 . . . . . . . . . . . 12 (((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โ†’ (๐ตโ€˜๐‘–) โˆˆ โ„‚)
23 simp1 1137 . . . . . . . . . . . 12 (((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚) โ†’ (๐ดโ€˜๐‘—) โˆˆ โ„‚)
24 mulcl 11194 . . . . . . . . . . . 12 (((๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ดโ€˜๐‘—) โˆˆ โ„‚) โ†’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆˆ โ„‚)
2522, 23, 24syl2an 597 . . . . . . . . . . 11 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆˆ โ„‚)
2621, 25addcld 11233 . . . . . . . . . 10 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆˆ โ„‚)
27 mulcl 11194 . . . . . . . . . . 11 (((๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚) โ†’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆˆ โ„‚)
2822, 19, 27syl2an 597 . . . . . . . . . 10 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆˆ โ„‚)
2926, 28subcld 11571 . . . . . . . . 9 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โˆˆ โ„‚)
30 simp2 1138 . . . . . . . . . 10 (((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚) โ†’ (๐ตโ€˜๐‘—) โˆˆ โ„‚)
31 mulcl 11194 . . . . . . . . . 10 (((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚) โ†’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) โˆˆ โ„‚)
3218, 30, 31syl2an 597 . . . . . . . . 9 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) โˆˆ โ„‚)
33 simp3 1139 . . . . . . . . . . 11 (((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โ†’ (๐ถโ€˜๐‘–) โˆˆ โ„‚)
34 mulcl 11194 . . . . . . . . . . 11 (((๐ถโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ดโ€˜๐‘—) โˆˆ โ„‚) โ†’ ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆˆ โ„‚)
3533, 23, 34syl2an 597 . . . . . . . . . 10 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆˆ โ„‚)
36 mulcl 11194 . . . . . . . . . . 11 (((๐ถโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚) โ†’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) โˆˆ โ„‚)
3733, 30, 36syl2an 597 . . . . . . . . . 10 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) โˆˆ โ„‚)
3835, 37subcld 11571 . . . . . . . . 9 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆˆ โ„‚)
3929, 32, 38subadd2d 11590 . . . . . . . 8 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โ†” ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)))))
40 eqcom 2740 . . . . . . . 8 (((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โ†” ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) = ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))
4139, 40bitrdi 287 . . . . . . 7 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โ†” ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) = ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
4235, 32, 37addsubd 11592 . . . . . . . . 9 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))
4335, 32addcomd 11416 . . . . . . . . . 10 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = (((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))))
4443oveq1d 7424 . . . . . . . . 9 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = ((((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))
4542, 44eqtr3d 2775 . . . . . . . 8 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = ((((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))
4645eqeq2d 2744 . . . . . . 7 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) = ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โ†” ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) = ((((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
4741, 46bitrd 279 . . . . . 6 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โ†” ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) = ((((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
4826, 28, 32subsub4d 11602 . . . . . . . . 9 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
4928, 32addcld 11233 . . . . . . . . . 10 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆˆ โ„‚)
5021, 49, 25subsub3d 11601 . . . . . . . . 9 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ ((((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)))) = ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
5128, 25, 32subsub3d 11601 . . . . . . . . . . . 12 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = ((((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))))
5251eqcomd 2739 . . . . . . . . . . 11 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
5352oveq2d 7425 . . . . . . . . . 10 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ ((((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)))) = (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))))
5425, 32subcld 11571 . . . . . . . . . . 11 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆˆ โ„‚)
5521, 28, 54subsubd 11599 . . . . . . . . . 10 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))) = ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) + (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
5653, 55eqtrd 2773 . . . . . . . . 9 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ ((((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)))) = ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) + (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
5748, 50, 563eqtr2d 2779 . . . . . . . 8 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) + (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
5821, 28subcld 11571 . . . . . . . . 9 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โˆˆ โ„‚)
5958, 25, 32addsub12d 11594 . . . . . . . 8 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) + (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
6021, 28, 32subsub4d 11602 . . . . . . . . 9 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
6160oveq2d 7425 . . . . . . . 8 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))))
6257, 59, 613eqtrd 2777 . . . . . . 7 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))))
6362eqeq1d 2735 . . . . . 6 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) โˆ’ ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โ†” (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
6432, 35addcld 11233 . . . . . . 7 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆˆ โ„‚)
65 subeqrev 11636 . . . . . . 7 ((((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆˆ โ„‚ โˆง ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆˆ โ„‚) โˆง ((((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆˆ โ„‚ โˆง ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) โˆˆ โ„‚)) โ†’ (((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) = ((((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โ†” (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)))) = (((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) โˆ’ (((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))))))
6626, 28, 64, 37, 65syl22anc 838 . . . . . 6 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—))) = ((((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โ†” (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)))) = (((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) โˆ’ (((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))))))
6747, 63, 663bitr3rd 310 . . . . 5 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)))) = (((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) โˆ’ (((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)))) โ†” (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
6821, 49subcld 11571 . . . . . . . 8 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) โˆˆ โ„‚)
6925, 68, 38addrsub 11631 . . . . . . 7 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โ†” (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)))))
7035, 37, 25sub32d 11603 . . . . . . . . 9 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) = ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))
7135, 25, 37subsub4d 11602 . . . . . . . . 9 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
7270, 71eqtrd 2773 . . . . . . . 8 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
7372eqeq2d 2744 . . . . . . 7 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = ((((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โˆ’ ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))) โ†” (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))))
7469, 73bitrd 279 . . . . . 6 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โ†” (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))))
75 eqcom 2740 . . . . . 6 ((((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) โ†” (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))))
7674, 75bitrdi 287 . . . . 5 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))) = (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))) โ†” (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))))
7767, 76bitrd 279 . . . 4 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)))) = (((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) โˆ’ (((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)))) โ†” (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))))
78 colinearalglem1 28164 . . . 4 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†” (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)))) = (((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) โˆ’ (((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—))))))
79 3anrot 1101 . . . . 5 (((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โ†” ((๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ดโ€˜๐‘–) โˆˆ โ„‚))
80 3anrot 1101 . . . . 5 (((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚) โ†” ((๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ดโ€˜๐‘—) โˆˆ โ„‚))
81 colinearalglem1 28164 . . . . 5 ((((๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ดโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ดโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ†” (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))))
8279, 80, 81syl2anb 599 . . . 4 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–))) โ†” (((๐ถโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ดโ€˜๐‘—)) + ((๐ถโ€˜๐‘–) ยท (๐ตโ€˜๐‘—)))) = (((๐ดโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) โˆ’ (((๐ตโ€˜๐‘–) ยท (๐ถโ€˜๐‘—)) + ((๐ดโ€˜๐‘–) ยท (๐ตโ€˜๐‘—))))))
8377, 78, 823bitr4d 311 . . 3 ((((๐ดโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘–) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘–) โˆˆ โ„‚) โˆง ((๐ดโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ตโ€˜๐‘—) โˆˆ โ„‚ โˆง (๐ถโ€˜๐‘—) โˆˆ โ„‚)) โ†’ ((((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†” (((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)))))
844, 7, 10, 13, 15, 17, 83syl33anc 1386 . 2 (((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โˆง (๐‘– โˆˆ (1...๐‘) โˆง ๐‘— โˆˆ (1...๐‘))) โ†’ ((((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†” (((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)))))
85842ralbidva 3217 1 ((๐ด โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ต โˆˆ (๐”ผโ€˜๐‘) โˆง ๐ถ โˆˆ (๐”ผโ€˜๐‘)) โ†’ (โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ตโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–)) ยท ((๐ถโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—))) = (((๐ตโ€˜๐‘—) โˆ’ (๐ดโ€˜๐‘—)) ยท ((๐ถโ€˜๐‘–) โˆ’ (๐ดโ€˜๐‘–))) โ†” โˆ€๐‘– โˆˆ (1...๐‘)โˆ€๐‘— โˆˆ (1...๐‘)(((๐ถโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)) ยท ((๐ดโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—))) = (((๐ถโ€˜๐‘—) โˆ’ (๐ตโ€˜๐‘—)) ยท ((๐ดโ€˜๐‘–) โˆ’ (๐ตโ€˜๐‘–)))))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆง w3a 1088   = wceq 1542   โˆˆ wcel 2107  โˆ€wral 3062  โ€˜cfv 6544  (class class class)co 7409  โ„‚cc 11108  1c1 11111   + caddc 11113   ยท cmul 11115   โˆ’ cmin 11444  ...cfz 13484  ๐”ผcee 28146
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  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 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-er 8703  df-map 8822  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11250  df-mnf 11251  df-ltxr 11253  df-sub 11446  df-neg 11447  df-ee 28149
This theorem is referenced by:  colinearalglem3  28166  colinearalg  28168
  Copyright terms: Public domain W3C validator