Description: Derive Axiom ax-his1 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 | ||
| axhfi.1 | ⊢ ·ih = ( ·𝑖OLD ‘ 𝑈 ) | ||
| Assertion | axhis1-zf | ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 ·ih 𝐵 ) = ( ∗ ‘ ( 𝐵 ·ih 𝐴 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | axhil.1 | ⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ | |
| 2 | axhil.2 | ⊢ 𝑈 ∈ CHilOLD | |
| 3 | axhfi.1 | ⊢ ·ih = ( ·𝑖OLD ‘ 𝑈 ) | |
| 4 | df-hba | ⊢ ℋ = ( BaseSet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) | |
| 5 | 1 | fveq2i | ⊢ ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) |
| 6 | 4 5 | eqtr4i | ⊢ ℋ = ( BaseSet ‘ 𝑈 ) |
| 7 | 6 3 | hlipcj | ⊢ ( ( 𝑈 ∈ CHilOLD ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 ·ih 𝐵 ) = ( ∗ ‘ ( 𝐵 ·ih 𝐴 ) ) ) |
| 8 | 2 7 | mp3an1 | ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 ·ih 𝐵 ) = ( ∗ ‘ ( 𝐵 ·ih 𝐴 ) ) ) |