Step | Hyp | Ref
| Expression |
1 | | vciOLD.1 |
. . . 4
โข ๐บ = (1st โ๐) |
2 | | vciOLD.2 |
. . . 4
โข ๐ = (2nd โ๐) |
3 | | vciOLD.3 |
. . . 4
โข ๐ = ran ๐บ |
4 | 1, 2, 3 | vciOLD 29545 |
. . 3
โข (๐ โ CVecOLD
โ (๐บ โ AbelOp
โง ๐:(โ ร
๐)โถ๐ โง โ๐ฅ โ ๐ ((1๐๐ฅ) = ๐ฅ โง โ๐ฆ โ โ (โ๐ง โ ๐ (๐ฆ๐(๐ฅ๐บ๐ง)) = ((๐ฆ๐๐ฅ)๐บ(๐ฆ๐๐ง)) โง โ๐ง โ โ (((๐ฆ + ๐ง)๐๐ฅ) = ((๐ฆ๐๐ฅ)๐บ(๐ง๐๐ฅ)) โง ((๐ฆ ยท ๐ง)๐๐ฅ) = (๐ฆ๐(๐ง๐๐ฅ))))))) |
5 | | simpl 484 |
. . . . 5
โข (((1๐๐ฅ) = ๐ฅ โง โ๐ฆ โ โ (โ๐ง โ ๐ (๐ฆ๐(๐ฅ๐บ๐ง)) = ((๐ฆ๐๐ฅ)๐บ(๐ฆ๐๐ง)) โง โ๐ง โ โ (((๐ฆ + ๐ง)๐๐ฅ) = ((๐ฆ๐๐ฅ)๐บ(๐ง๐๐ฅ)) โง ((๐ฆ ยท ๐ง)๐๐ฅ) = (๐ฆ๐(๐ง๐๐ฅ))))) โ (1๐๐ฅ) = ๐ฅ) |
6 | 5 | ralimi 3083 |
. . . 4
โข
(โ๐ฅ โ
๐ ((1๐๐ฅ) = ๐ฅ โง โ๐ฆ โ โ (โ๐ง โ ๐ (๐ฆ๐(๐ฅ๐บ๐ง)) = ((๐ฆ๐๐ฅ)๐บ(๐ฆ๐๐ง)) โง โ๐ง โ โ (((๐ฆ + ๐ง)๐๐ฅ) = ((๐ฆ๐๐ฅ)๐บ(๐ง๐๐ฅ)) โง ((๐ฆ ยท ๐ง)๐๐ฅ) = (๐ฆ๐(๐ง๐๐ฅ))))) โ โ๐ฅ โ ๐ (1๐๐ฅ) = ๐ฅ) |
7 | 6 | 3ad2ant3 1136 |
. . 3
โข ((๐บ โ AbelOp โง ๐:(โ ร ๐)โถ๐ โง โ๐ฅ โ ๐ ((1๐๐ฅ) = ๐ฅ โง โ๐ฆ โ โ (โ๐ง โ ๐ (๐ฆ๐(๐ฅ๐บ๐ง)) = ((๐ฆ๐๐ฅ)๐บ(๐ฆ๐๐ง)) โง โ๐ง โ โ (((๐ฆ + ๐ง)๐๐ฅ) = ((๐ฆ๐๐ฅ)๐บ(๐ง๐๐ฅ)) โง ((๐ฆ ยท ๐ง)๐๐ฅ) = (๐ฆ๐(๐ง๐๐ฅ)))))) โ โ๐ฅ โ ๐ (1๐๐ฅ) = ๐ฅ) |
8 | 4, 7 | syl 17 |
. 2
โข (๐ โ CVecOLD
โ โ๐ฅ โ
๐ (1๐๐ฅ) = ๐ฅ) |
9 | | oveq2 7366 |
. . . 4
โข (๐ฅ = ๐ด โ (1๐๐ฅ) = (1๐๐ด)) |
10 | | id 22 |
. . . 4
โข (๐ฅ = ๐ด โ ๐ฅ = ๐ด) |
11 | 9, 10 | eqeq12d 2749 |
. . 3
โข (๐ฅ = ๐ด โ ((1๐๐ฅ) = ๐ฅ โ (1๐๐ด) = ๐ด)) |
12 | 11 | rspccva 3579 |
. 2
โข
((โ๐ฅ โ
๐ (1๐๐ฅ) = ๐ฅ โง ๐ด โ ๐) โ (1๐๐ด) = ๐ด) |
13 | 8, 12 | sylan 581 |
1
โข ((๐ โ CVecOLD โง
๐ด โ ๐) โ (1๐๐ด) = ๐ด) |