Description: Derive Axiom ax-hvass 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 | axhvass-zf | ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 +ℎ 𝐵 ) +ℎ 𝐶 ) = ( 𝐴 +ℎ ( 𝐵 +ℎ 𝐶 ) ) ) |
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 | hlass | ⊢ ( ( 𝑈 ∈ CHilOLD ∧ ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ) → ( ( 𝐴 +ℎ 𝐵 ) +ℎ 𝐶 ) = ( 𝐴 +ℎ ( 𝐵 +ℎ 𝐶 ) ) ) |
9 | 2 8 | mpan | ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 +ℎ 𝐵 ) +ℎ 𝐶 ) = ( 𝐴 +ℎ ( 𝐵 +ℎ 𝐶 ) ) ) |