Metamath Proof Explorer


Theorem axhfvadd-zf

Description: Derive Axiom ax-hfvadd from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008) (New usage is discouraged.)

Ref Expression
Hypotheses axhil.1 โŠข ๐‘ˆ = โŸจ โŸจ +โ„Ž , ยทโ„Ž โŸฉ , normโ„Ž โŸฉ
axhil.2 โŠข ๐‘ˆ โˆˆ CHilOLD
Assertion axhfvadd-zf +โ„Ž : ( โ„‹ ร— โ„‹ ) โŸถ โ„‹

Proof

Step Hyp Ref Expression
1 axhil.1 โŠข ๐‘ˆ = โŸจ โŸจ +โ„Ž , ยทโ„Ž โŸฉ , normโ„Ž โŸฉ
2 axhil.2 โŠข ๐‘ˆ โˆˆ CHilOLD
3 df-hba โŠข โ„‹ = ( BaseSet โ€˜ โŸจ โŸจ +โ„Ž , ยทโ„Ž โŸฉ , normโ„Ž โŸฉ )
4 1 fveq2i โŠข ( BaseSet โ€˜ ๐‘ˆ ) = ( BaseSet โ€˜ โŸจ โŸจ +โ„Ž , ยทโ„Ž โŸฉ , normโ„Ž โŸฉ )
5 3 4 eqtr4i โŠข โ„‹ = ( BaseSet โ€˜ ๐‘ˆ )
6 2 hlnvi โŠข ๐‘ˆ โˆˆ NrmCVec
7 1 6 h2hva โŠข +โ„Ž = ( +๐‘ฃ โ€˜ ๐‘ˆ )
8 5 7 hladdf โŠข ( ๐‘ˆ โˆˆ CHilOLD โ†’ +โ„Ž : ( โ„‹ ร— โ„‹ ) โŸถ โ„‹ )
9 2 8 ax-mp โŠข +โ„Ž : ( โ„‹ ร— โ„‹ ) โŸถ โ„‹