Step | Hyp | Ref
| Expression |
1 | | vciOLD.1 |
. . . . . 6
โข ๐บ = (1st โ๐) |
2 | | vciOLD.2 |
. . . . . 6
โข ๐ = (2nd โ๐) |
3 | | vciOLD.3 |
. . . . . 6
โข ๐ = ran ๐บ |
4 | 1, 2, 3 | vciOLD 29545 |
. . . . 5
โข (๐ โ CVecOLD
โ (๐บ โ AbelOp
โง ๐:(โ ร
๐)โถ๐ โง โ๐ฅ โ ๐ ((1๐๐ฅ) = ๐ฅ โง โ๐ฆ โ โ (โ๐ง โ ๐ (๐ฆ๐(๐ฅ๐บ๐ง)) = ((๐ฆ๐๐ฅ)๐บ(๐ฆ๐๐ง)) โง โ๐ง โ โ (((๐ฆ + ๐ง)๐๐ฅ) = ((๐ฆ๐๐ฅ)๐บ(๐ง๐๐ฅ)) โง ((๐ฆ ยท ๐ง)๐๐ฅ) = (๐ฆ๐(๐ง๐๐ฅ))))))) |
5 | | simpl 484 |
. . . . . . . . 9
โข
((โ๐ง โ
๐ (๐ฆ๐(๐ฅ๐บ๐ง)) = ((๐ฆ๐๐ฅ)๐บ(๐ฆ๐๐ง)) โง โ๐ง โ โ (((๐ฆ + ๐ง)๐๐ฅ) = ((๐ฆ๐๐ฅ)๐บ(๐ง๐๐ฅ)) โง ((๐ฆ ยท ๐ง)๐๐ฅ) = (๐ฆ๐(๐ง๐๐ฅ)))) โ โ๐ง โ ๐ (๐ฆ๐(๐ฅ๐บ๐ง)) = ((๐ฆ๐๐ฅ)๐บ(๐ฆ๐๐ง))) |
6 | 5 | ralimi 3083 |
. . . . . . . 8
โข
(โ๐ฆ โ
โ (โ๐ง โ
๐ (๐ฆ๐(๐ฅ๐บ๐ง)) = ((๐ฆ๐๐ฅ)๐บ(๐ฆ๐๐ง)) โง โ๐ง โ โ (((๐ฆ + ๐ง)๐๐ฅ) = ((๐ฆ๐๐ฅ)๐บ(๐ง๐๐ฅ)) โง ((๐ฆ ยท ๐ง)๐๐ฅ) = (๐ฆ๐(๐ง๐๐ฅ)))) โ โ๐ฆ โ โ โ๐ง โ ๐ (๐ฆ๐(๐ฅ๐บ๐ง)) = ((๐ฆ๐๐ฅ)๐บ(๐ฆ๐๐ง))) |
7 | 6 | adantl 483 |
. . . . . . 7
โข (((1๐๐ฅ) = ๐ฅ โง โ๐ฆ โ โ (โ๐ง โ ๐ (๐ฆ๐(๐ฅ๐บ๐ง)) = ((๐ฆ๐๐ฅ)๐บ(๐ฆ๐๐ง)) โง โ๐ง โ โ (((๐ฆ + ๐ง)๐๐ฅ) = ((๐ฆ๐๐ฅ)๐บ(๐ง๐๐ฅ)) โง ((๐ฆ ยท ๐ง)๐๐ฅ) = (๐ฆ๐(๐ง๐๐ฅ))))) โ โ๐ฆ โ โ โ๐ง โ ๐ (๐ฆ๐(๐ฅ๐บ๐ง)) = ((๐ฆ๐๐ฅ)๐บ(๐ฆ๐๐ง))) |
8 | 7 | ralimi 3083 |
. . . . . 6
โข
(โ๐ฅ โ
๐ ((1๐๐ฅ) = ๐ฅ โง โ๐ฆ โ โ (โ๐ง โ ๐ (๐ฆ๐(๐ฅ๐บ๐ง)) = ((๐ฆ๐๐ฅ)๐บ(๐ฆ๐๐ง)) โง โ๐ง โ โ (((๐ฆ + ๐ง)๐๐ฅ) = ((๐ฆ๐๐ฅ)๐บ(๐ง๐๐ฅ)) โง ((๐ฆ ยท ๐ง)๐๐ฅ) = (๐ฆ๐(๐ง๐๐ฅ))))) โ โ๐ฅ โ ๐ โ๐ฆ โ โ โ๐ง โ ๐ (๐ฆ๐(๐ฅ๐บ๐ง)) = ((๐ฆ๐๐ฅ)๐บ(๐ฆ๐๐ง))) |
9 | 8 | 3ad2ant3 1136 |
. . . . 5
โข ((๐บ โ AbelOp โง ๐:(โ ร ๐)โถ๐ โง โ๐ฅ โ ๐ ((1๐๐ฅ) = ๐ฅ โง โ๐ฆ โ โ (โ๐ง โ ๐ (๐ฆ๐(๐ฅ๐บ๐ง)) = ((๐ฆ๐๐ฅ)๐บ(๐ฆ๐๐ง)) โง โ๐ง โ โ (((๐ฆ + ๐ง)๐๐ฅ) = ((๐ฆ๐๐ฅ)๐บ(๐ง๐๐ฅ)) โง ((๐ฆ ยท ๐ง)๐๐ฅ) = (๐ฆ๐(๐ง๐๐ฅ)))))) โ โ๐ฅ โ ๐ โ๐ฆ โ โ โ๐ง โ ๐ (๐ฆ๐(๐ฅ๐บ๐ง)) = ((๐ฆ๐๐ฅ)๐บ(๐ฆ๐๐ง))) |
10 | 4, 9 | syl 17 |
. . . 4
โข (๐ โ CVecOLD
โ โ๐ฅ โ
๐ โ๐ฆ โ โ โ๐ง โ ๐ (๐ฆ๐(๐ฅ๐บ๐ง)) = ((๐ฆ๐๐ฅ)๐บ(๐ฆ๐๐ง))) |
11 | | oveq1 7365 |
. . . . . . 7
โข (๐ฅ = ๐ต โ (๐ฅ๐บ๐ง) = (๐ต๐บ๐ง)) |
12 | 11 | oveq2d 7374 |
. . . . . 6
โข (๐ฅ = ๐ต โ (๐ฆ๐(๐ฅ๐บ๐ง)) = (๐ฆ๐(๐ต๐บ๐ง))) |
13 | | oveq2 7366 |
. . . . . . 7
โข (๐ฅ = ๐ต โ (๐ฆ๐๐ฅ) = (๐ฆ๐๐ต)) |
14 | 13 | oveq1d 7373 |
. . . . . 6
โข (๐ฅ = ๐ต โ ((๐ฆ๐๐ฅ)๐บ(๐ฆ๐๐ง)) = ((๐ฆ๐๐ต)๐บ(๐ฆ๐๐ง))) |
15 | 12, 14 | eqeq12d 2749 |
. . . . 5
โข (๐ฅ = ๐ต โ ((๐ฆ๐(๐ฅ๐บ๐ง)) = ((๐ฆ๐๐ฅ)๐บ(๐ฆ๐๐ง)) โ (๐ฆ๐(๐ต๐บ๐ง)) = ((๐ฆ๐๐ต)๐บ(๐ฆ๐๐ง)))) |
16 | | oveq1 7365 |
. . . . . 6
โข (๐ฆ = ๐ด โ (๐ฆ๐(๐ต๐บ๐ง)) = (๐ด๐(๐ต๐บ๐ง))) |
17 | | oveq1 7365 |
. . . . . . 7
โข (๐ฆ = ๐ด โ (๐ฆ๐๐ต) = (๐ด๐๐ต)) |
18 | | oveq1 7365 |
. . . . . . 7
โข (๐ฆ = ๐ด โ (๐ฆ๐๐ง) = (๐ด๐๐ง)) |
19 | 17, 18 | oveq12d 7376 |
. . . . . 6
โข (๐ฆ = ๐ด โ ((๐ฆ๐๐ต)๐บ(๐ฆ๐๐ง)) = ((๐ด๐๐ต)๐บ(๐ด๐๐ง))) |
20 | 16, 19 | eqeq12d 2749 |
. . . . 5
โข (๐ฆ = ๐ด โ ((๐ฆ๐(๐ต๐บ๐ง)) = ((๐ฆ๐๐ต)๐บ(๐ฆ๐๐ง)) โ (๐ด๐(๐ต๐บ๐ง)) = ((๐ด๐๐ต)๐บ(๐ด๐๐ง)))) |
21 | | oveq2 7366 |
. . . . . . 7
โข (๐ง = ๐ถ โ (๐ต๐บ๐ง) = (๐ต๐บ๐ถ)) |
22 | 21 | oveq2d 7374 |
. . . . . 6
โข (๐ง = ๐ถ โ (๐ด๐(๐ต๐บ๐ง)) = (๐ด๐(๐ต๐บ๐ถ))) |
23 | | oveq2 7366 |
. . . . . . 7
โข (๐ง = ๐ถ โ (๐ด๐๐ง) = (๐ด๐๐ถ)) |
24 | 23 | oveq2d 7374 |
. . . . . 6
โข (๐ง = ๐ถ โ ((๐ด๐๐ต)๐บ(๐ด๐๐ง)) = ((๐ด๐๐ต)๐บ(๐ด๐๐ถ))) |
25 | 22, 24 | eqeq12d 2749 |
. . . . 5
โข (๐ง = ๐ถ โ ((๐ด๐(๐ต๐บ๐ง)) = ((๐ด๐๐ต)๐บ(๐ด๐๐ง)) โ (๐ด๐(๐ต๐บ๐ถ)) = ((๐ด๐๐ต)๐บ(๐ด๐๐ถ)))) |
26 | 15, 20, 25 | rspc3v 3592 |
. . . 4
โข ((๐ต โ ๐ โง ๐ด โ โ โง ๐ถ โ ๐) โ (โ๐ฅ โ ๐ โ๐ฆ โ โ โ๐ง โ ๐ (๐ฆ๐(๐ฅ๐บ๐ง)) = ((๐ฆ๐๐ฅ)๐บ(๐ฆ๐๐ง)) โ (๐ด๐(๐ต๐บ๐ถ)) = ((๐ด๐๐ต)๐บ(๐ด๐๐ถ)))) |
27 | 10, 26 | syl5 34 |
. . 3
โข ((๐ต โ ๐ โง ๐ด โ โ โง ๐ถ โ ๐) โ (๐ โ CVecOLD โ (๐ด๐(๐ต๐บ๐ถ)) = ((๐ด๐๐ต)๐บ(๐ด๐๐ถ)))) |
28 | 27 | 3com12 1124 |
. 2
โข ((๐ด โ โ โง ๐ต โ ๐ โง ๐ถ โ ๐) โ (๐ โ CVecOLD โ (๐ด๐(๐ต๐บ๐ถ)) = ((๐ด๐๐ต)๐บ(๐ด๐๐ถ)))) |
29 | 28 | impcom 409 |
1
โข ((๐ โ CVecOLD โง
(๐ด โ โ โง
๐ต โ ๐ โง ๐ถ โ ๐)) โ (๐ด๐(๐ต๐บ๐ถ)) = ((๐ด๐๐ต)๐บ(๐ด๐๐ถ))) |