nvop

Description: A complex inner product space in terms of ordered pair components. (Contributed by NM, 11-Sep-2007) (New usage is discouraged.)

Step	Hyp	Ref	Expression
1		nvop.2	$⊢ G = +_{v} (U)$
2		nvop.4	$⊢ S = \cdot_{𝑠OLD} (U)$
3		nvop.6	$⊢ N = {norm}_{CV} (U)$
4		nvrel	$⊢ Rel NrmCVec$
5		1st2nd	$⊢ (Rel NrmCVec \land U \in NrmCVec) \to U = ⟨1^{st} (U), 2^{nd} (U)⟩$
6	4 5	mpan	$⊢ U \in NrmCVec \to U = ⟨1^{st} (U), 2^{nd} (U)⟩$
7	3	nmcvfval	$⊢ N = 2^{nd} (U)$
8	7	opeq2i	$⊢ ⟨1^{st} (U), N⟩ = ⟨1^{st} (U), 2^{nd} (U)⟩$
9		eqid	$⊢ 1^{st} (U) = 1^{st} (U)$
10	9 1 2	nvvop	$⊢ U \in NrmCVec \to 1^{st} (U) = ⟨G, S⟩$
11	10	opeq1d	$⊢ U \in NrmCVec \to ⟨1^{st} (U), N⟩ = ⟨⟨G, S⟩, N⟩$
12	8 11	eqtr3id	$⊢ U \in NrmCVec \to ⟨1^{st} (U), 2^{nd} (U)⟩ = ⟨⟨G, S⟩, N⟩$
13	6 12	eqtrd	$⊢ U \in NrmCVec \to U = ⟨⟨G, S⟩, N⟩$

Metamath Proof Explorer