Step | Hyp | Ref
| Expression |
1 | | vcex 29569 |
. 2
โข
(โจ๐บ, ๐โฉ โ CVecOLD
โ (๐บ โ V โง
๐ โ
V)) |
2 | | elex 3465 |
. . . . 5
โข (๐บ โ AbelOp โ ๐บ โ V) |
3 | 2 | adantr 482 |
. . . 4
โข ((๐บ โ AbelOp โง ๐:(โ ร ๐)โถ๐) โ ๐บ โ V) |
4 | | cnex 11140 |
. . . . . . 7
โข โ
โ V |
5 | | ablogrpo 29538 |
. . . . . . . 8
โข (๐บ โ AbelOp โ ๐บ โ GrpOp) |
6 | | isvcOLD.1 |
. . . . . . . . 9
โข ๐ = ran ๐บ |
7 | | rnexg 7845 |
. . . . . . . . 9
โข (๐บ โ GrpOp โ ran ๐บ โ V) |
8 | 6, 7 | eqeltrid 2838 |
. . . . . . . 8
โข (๐บ โ GrpOp โ ๐ โ V) |
9 | 5, 8 | syl 17 |
. . . . . . 7
โข (๐บ โ AbelOp โ ๐ โ V) |
10 | | xpexg 7688 |
. . . . . . 7
โข ((โ
โ V โง ๐ โ V)
โ (โ ร ๐)
โ V) |
11 | 4, 9, 10 | sylancr 588 |
. . . . . 6
โข (๐บ โ AbelOp โ (โ
ร ๐) โ
V) |
12 | | fex 7180 |
. . . . . 6
โข ((๐:(โ ร ๐)โถ๐ โง (โ ร ๐) โ V) โ ๐ โ V) |
13 | 11, 12 | sylan2 594 |
. . . . 5
โข ((๐:(โ ร ๐)โถ๐ โง ๐บ โ AbelOp) โ ๐ โ V) |
14 | 13 | ancoms 460 |
. . . 4
โข ((๐บ โ AbelOp โง ๐:(โ ร ๐)โถ๐) โ ๐ โ V) |
15 | 3, 14 | jca 513 |
. . 3
โข ((๐บ โ AbelOp โง ๐:(โ ร ๐)โถ๐) โ (๐บ โ V โง ๐ โ V)) |
16 | 15 | 3adant3 1133 |
. 2
โข ((๐บ โ AbelOp โง ๐:(โ ร ๐)โถ๐ โง โ๐ฅ โ ๐ ((1๐๐ฅ) = ๐ฅ โง โ๐ฆ โ โ (โ๐ง โ ๐ (๐ฆ๐(๐ฅ๐บ๐ง)) = ((๐ฆ๐๐ฅ)๐บ(๐ฆ๐๐ง)) โง โ๐ง โ โ (((๐ฆ + ๐ง)๐๐ฅ) = ((๐ฆ๐๐ฅ)๐บ(๐ง๐๐ฅ)) โง ((๐ฆ ยท ๐ง)๐๐ฅ) = (๐ฆ๐(๐ง๐๐ฅ)))))) โ (๐บ โ V โง ๐ โ V)) |
17 | 6 | isvclem 29568 |
. 2
โข ((๐บ โ V โง ๐ โ V) โ (โจ๐บ, ๐โฉ โ CVecOLD โ
(๐บ โ AbelOp โง
๐:(โ ร ๐)โถ๐ โง โ๐ฅ โ ๐ ((1๐๐ฅ) = ๐ฅ โง โ๐ฆ โ โ (โ๐ง โ ๐ (๐ฆ๐(๐ฅ๐บ๐ง)) = ((๐ฆ๐๐ฅ)๐บ(๐ฆ๐๐ง)) โง โ๐ง โ โ (((๐ฆ + ๐ง)๐๐ฅ) = ((๐ฆ๐๐ฅ)๐บ(๐ง๐๐ฅ)) โง ((๐ฆ ยท ๐ง)๐๐ฅ) = (๐ฆ๐(๐ง๐๐ฅ)))))))) |
18 | 1, 16, 17 | pm5.21nii 380 |
1
โข
(โจ๐บ, ๐โฉ โ CVecOLD
โ (๐บ โ AbelOp
โง ๐:(โ ร
๐)โถ๐ โง โ๐ฅ โ ๐ ((1๐๐ฅ) = ๐ฅ โง โ๐ฆ โ โ (โ๐ง โ ๐ (๐ฆ๐(๐ฅ๐บ๐ง)) = ((๐ฆ๐๐ฅ)๐บ(๐ฆ๐๐ง)) โง โ๐ง โ โ (((๐ฆ + ๐ง)๐๐ฅ) = ((๐ฆ๐๐ฅ)๐บ(๐ง๐๐ฅ)) โง ((๐ฆ ยท ๐ง)๐๐ฅ) = (๐ฆ๐(๐ง๐๐ฅ))))))) |