Step | Hyp | Ref
| Expression |
1 | | isvciOLD.8 |
. 2
โข ๐ = โจ๐บ, ๐โฉ |
2 | | isvciOLD.1 |
. . 3
โข ๐บ โ AbelOp |
3 | | isvciOLD.3 |
. . 3
โข ๐:(โ ร ๐)โถ๐ |
4 | | isvciOLD.4 |
. . . . 5
โข (๐ฅ โ ๐ โ (1๐๐ฅ) = ๐ฅ) |
5 | | isvciOLD.5 |
. . . . . . . . . 10
โข ((๐ฆ โ โ โง ๐ฅ โ ๐ โง ๐ง โ ๐) โ (๐ฆ๐(๐ฅ๐บ๐ง)) = ((๐ฆ๐๐ฅ)๐บ(๐ฆ๐๐ง))) |
6 | 5 | 3com12 1124 |
. . . . . . . . 9
โข ((๐ฅ โ ๐ โง ๐ฆ โ โ โง ๐ง โ ๐) โ (๐ฆ๐(๐ฅ๐บ๐ง)) = ((๐ฆ๐๐ฅ)๐บ(๐ฆ๐๐ง))) |
7 | 6 | 3expa 1119 |
. . . . . . . 8
โข (((๐ฅ โ ๐ โง ๐ฆ โ โ) โง ๐ง โ ๐) โ (๐ฆ๐(๐ฅ๐บ๐ง)) = ((๐ฆ๐๐ฅ)๐บ(๐ฆ๐๐ง))) |
8 | 7 | ralrimiva 3142 |
. . . . . . 7
โข ((๐ฅ โ ๐ โง ๐ฆ โ โ) โ โ๐ง โ ๐ (๐ฆ๐(๐ฅ๐บ๐ง)) = ((๐ฆ๐๐ฅ)๐บ(๐ฆ๐๐ง))) |
9 | | isvciOLD.6 |
. . . . . . . . . . 11
โข ((๐ฆ โ โ โง ๐ง โ โ โง ๐ฅ โ ๐) โ ((๐ฆ + ๐ง)๐๐ฅ) = ((๐ฆ๐๐ฅ)๐บ(๐ง๐๐ฅ))) |
10 | | isvciOLD.7 |
. . . . . . . . . . 11
โข ((๐ฆ โ โ โง ๐ง โ โ โง ๐ฅ โ ๐) โ ((๐ฆ ยท ๐ง)๐๐ฅ) = (๐ฆ๐(๐ง๐๐ฅ))) |
11 | 9, 10 | jca 513 |
. . . . . . . . . 10
โข ((๐ฆ โ โ โง ๐ง โ โ โง ๐ฅ โ ๐) โ (((๐ฆ + ๐ง)๐๐ฅ) = ((๐ฆ๐๐ฅ)๐บ(๐ง๐๐ฅ)) โง ((๐ฆ ยท ๐ง)๐๐ฅ) = (๐ฆ๐(๐ง๐๐ฅ)))) |
12 | 11 | 3comr 1126 |
. . . . . . . . 9
โข ((๐ฅ โ ๐ โง ๐ฆ โ โ โง ๐ง โ โ) โ (((๐ฆ + ๐ง)๐๐ฅ) = ((๐ฆ๐๐ฅ)๐บ(๐ง๐๐ฅ)) โง ((๐ฆ ยท ๐ง)๐๐ฅ) = (๐ฆ๐(๐ง๐๐ฅ)))) |
13 | 12 | 3expa 1119 |
. . . . . . . 8
โข (((๐ฅ โ ๐ โง ๐ฆ โ โ) โง ๐ง โ โ) โ (((๐ฆ + ๐ง)๐๐ฅ) = ((๐ฆ๐๐ฅ)๐บ(๐ง๐๐ฅ)) โง ((๐ฆ ยท ๐ง)๐๐ฅ) = (๐ฆ๐(๐ง๐๐ฅ)))) |
14 | 13 | ralrimiva 3142 |
. . . . . . 7
โข ((๐ฅ โ ๐ โง ๐ฆ โ โ) โ โ๐ง โ โ (((๐ฆ + ๐ง)๐๐ฅ) = ((๐ฆ๐๐ฅ)๐บ(๐ง๐๐ฅ)) โง ((๐ฆ ยท ๐ง)๐๐ฅ) = (๐ฆ๐(๐ง๐๐ฅ)))) |
15 | 8, 14 | jca 513 |
. . . . . 6
โข ((๐ฅ โ ๐ โง ๐ฆ โ โ) โ (โ๐ง โ ๐ (๐ฆ๐(๐ฅ๐บ๐ง)) = ((๐ฆ๐๐ฅ)๐บ(๐ฆ๐๐ง)) โง โ๐ง โ โ (((๐ฆ + ๐ง)๐๐ฅ) = ((๐ฆ๐๐ฅ)๐บ(๐ง๐๐ฅ)) โง ((๐ฆ ยท ๐ง)๐๐ฅ) = (๐ฆ๐(๐ง๐๐ฅ))))) |
16 | 15 | ralrimiva 3142 |
. . . . 5
โข (๐ฅ โ ๐ โ โ๐ฆ โ โ (โ๐ง โ ๐ (๐ฆ๐(๐ฅ๐บ๐ง)) = ((๐ฆ๐๐ฅ)๐บ(๐ฆ๐๐ง)) โง โ๐ง โ โ (((๐ฆ + ๐ง)๐๐ฅ) = ((๐ฆ๐๐ฅ)๐บ(๐ง๐๐ฅ)) โง ((๐ฆ ยท ๐ง)๐๐ฅ) = (๐ฆ๐(๐ง๐๐ฅ))))) |
17 | 4, 16 | jca 513 |
. . . 4
โข (๐ฅ โ ๐ โ ((1๐๐ฅ) = ๐ฅ โง โ๐ฆ โ โ (โ๐ง โ ๐ (๐ฆ๐(๐ฅ๐บ๐ง)) = ((๐ฆ๐๐ฅ)๐บ(๐ฆ๐๐ง)) โง โ๐ง โ โ (((๐ฆ + ๐ง)๐๐ฅ) = ((๐ฆ๐๐ฅ)๐บ(๐ง๐๐ฅ)) โง ((๐ฆ ยท ๐ง)๐๐ฅ) = (๐ฆ๐(๐ง๐๐ฅ)))))) |
18 | 17 | rgen 3065 |
. . 3
โข
โ๐ฅ โ
๐ ((1๐๐ฅ) = ๐ฅ โง โ๐ฆ โ โ (โ๐ง โ ๐ (๐ฆ๐(๐ฅ๐บ๐ง)) = ((๐ฆ๐๐ฅ)๐บ(๐ฆ๐๐ง)) โง โ๐ง โ โ (((๐ฆ + ๐ง)๐๐ฅ) = ((๐ฆ๐๐ฅ)๐บ(๐ง๐๐ฅ)) โง ((๐ฆ ยท ๐ง)๐๐ฅ) = (๐ฆ๐(๐ง๐๐ฅ))))) |
19 | | ablogrpo 29275 |
. . . . . 6
โข (๐บ โ AbelOp โ ๐บ โ GrpOp) |
20 | 2, 19 | ax-mp 5 |
. . . . 5
โข ๐บ โ GrpOp |
21 | | isvciOLD.2 |
. . . . 5
โข dom ๐บ = (๐ ร ๐) |
22 | 20, 21 | grporn 29249 |
. . . 4
โข ๐ = ran ๐บ |
23 | 22 | isvcOLD 29307 |
. . 3
โข
(โจ๐บ, ๐โฉ โ CVecOLD
โ (๐บ โ AbelOp
โง ๐:(โ ร
๐)โถ๐ โง โ๐ฅ โ ๐ ((1๐๐ฅ) = ๐ฅ โง โ๐ฆ โ โ (โ๐ง โ ๐ (๐ฆ๐(๐ฅ๐บ๐ง)) = ((๐ฆ๐๐ฅ)๐บ(๐ฆ๐๐ง)) โง โ๐ง โ โ (((๐ฆ + ๐ง)๐๐ฅ) = ((๐ฆ๐๐ฅ)๐บ(๐ง๐๐ฅ)) โง ((๐ฆ ยท ๐ง)๐๐ฅ) = (๐ฆ๐(๐ง๐๐ฅ))))))) |
24 | 2, 3, 18, 23 | mpbir3an 1342 |
. 2
โข
โจ๐บ, ๐โฉ โ
CVecOLD |
25 | 1, 24 | eqeltri 2835 |
1
โข ๐ โ
CVecOLD |