Description: Derive Axiom ax-hvmulid 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 | axhvmulid-zf | ⊢ ( 𝐴 ∈ ℋ → ( 1 ·ℎ 𝐴 ) = 𝐴 ) |
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 | h2hsm | ⊢ ·ℎ = ( ·𝑠OLD ‘ 𝑈 ) |
8 | 5 7 | hlmulid | ⊢ ( ( 𝑈 ∈ CHilOLD ∧ 𝐴 ∈ ℋ ) → ( 1 ·ℎ 𝐴 ) = 𝐴 ) |
9 | 2 8 | mpan | ⊢ ( 𝐴 ∈ ℋ → ( 1 ·ℎ 𝐴 ) = 𝐴 ) |