Theorem hlhilsplus

Description: Scalar addition for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015) (Revised by Mario Carneiro, 28-Jun-2015) (Revised by AV, 6-Nov-2024)

	Ref	Expression
Hypotheses	hlhilslem.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	hlhilslem.e	⊢ 𝐸 = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 )
	hlhilslem.u	⊢ 𝑈 = ( ( HLHil ‘ 𝐾 ) ‘ 𝑊 )
	hlhilslem.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
	hlhilslem.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	hlhilsplus.a	⊢ + = ( +g ‘ 𝐸 )
Assertion	hlhilsplus	⊢ ( 𝜑 → + = ( +g ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		hlhilslem.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		hlhilslem.e	⊢ 𝐸 = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 )
3		hlhilslem.u	⊢ 𝑈 = ( ( HLHil ‘ 𝐾 ) ‘ 𝑊 )
4		hlhilslem.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
5		hlhilslem.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
6		hlhilsplus.a	⊢ + = ( +g ‘ 𝐸 )
7		plusgid	⊢ +g = Slot ( +g ‘ ndx )
8		starvndxnplusgndx	⊢ ( *𝑟 ‘ ndx ) ≠ ( +g ‘ ndx )
9	8	necomi	⊢ ( +g ‘ ndx ) ≠ ( *𝑟 ‘ ndx )
10	1 2 3 4 5 7 9 6	hlhilslem	⊢ ( 𝜑 → + = ( +g ‘ 𝑅 ) )