Step |
Hyp |
Ref |
Expression |
1 |
|
hhsssh2.1 |
โข ๐ = โจ โจ ( +โ โพ ( ๐ป ร ๐ป ) ) , ( ยทโ โพ ( โ ร ๐ป ) ) โฉ , ( normโ โพ ๐ป ) โฉ |
2 |
|
hhssba.2 |
โข ๐ป โ Sโ |
3 |
|
eqid |
โข โจ โจ +โ , ยทโ โฉ , normโ โฉ = โจ โจ +โ , ยทโ โฉ , normโ โฉ |
4 |
3
|
hhnv |
โข โจ โจ +โ , ยทโ โฉ , normโ โฉ โ NrmCVec |
5 |
3 1
|
hhsst |
โข ( ๐ป โ Sโ โ ๐ โ ( SubSp โ โจ โจ +โ , ยทโ โฉ , normโ โฉ ) ) |
6 |
2 5
|
ax-mp |
โข ๐ โ ( SubSp โ โจ โจ +โ , ยทโ โฉ , normโ โฉ ) |
7 |
1 2
|
hhssba |
โข ๐ป = ( BaseSet โ ๐ ) |
8 |
3
|
hhvs |
โข โโ = ( โ๐ฃ โ โจ โจ +โ , ยทโ โฉ , normโ โฉ ) |
9 |
|
eqid |
โข ( โ๐ฃ โ ๐ ) = ( โ๐ฃ โ ๐ ) |
10 |
|
eqid |
โข ( SubSp โ โจ โจ +โ , ยทโ โฉ , normโ โฉ ) = ( SubSp โ โจ โจ +โ , ยทโ โฉ , normโ โฉ ) |
11 |
7 8 9 10
|
sspm |
โข ( ( โจ โจ +โ , ยทโ โฉ , normโ โฉ โ NrmCVec โง ๐ โ ( SubSp โ โจ โจ +โ , ยทโ โฉ , normโ โฉ ) ) โ ( โ๐ฃ โ ๐ ) = ( โโ โพ ( ๐ป ร ๐ป ) ) ) |
12 |
4 6 11
|
mp2an |
โข ( โ๐ฃ โ ๐ ) = ( โโ โพ ( ๐ป ร ๐ป ) ) |
13 |
12
|
eqcomi |
โข ( โโ โพ ( ๐ป ร ๐ป ) ) = ( โ๐ฃ โ ๐ ) |