Description: Derive Axiom ax-hv0cl 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 | axhv0cl-zf | ⊢ 0ℎ ∈ ℋ |
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 | df-h0v | ⊢ 0ℎ = ( 0vec ‘ 〈 〈 +ℎ , ·ℎ 〉 , normℎ 〉 ) | |
7 | 1 | fveq2i | ⊢ ( 0vec ‘ 𝑈 ) = ( 0vec ‘ 〈 〈 +ℎ , ·ℎ 〉 , normℎ 〉 ) |
8 | 6 7 | eqtr4i | ⊢ 0ℎ = ( 0vec ‘ 𝑈 ) |
9 | 5 8 | hl0cl | ⊢ ( 𝑈 ∈ CHilOLD → 0ℎ ∈ ℋ ) |
10 | 2 9 | ax-mp | ⊢ 0ℎ ∈ ℋ |