Theorem vsfval

Description: Value of the function for the vector subtraction operation on a normed complex vector space. (Contributed by NM, 15-Feb-2008) (Revised by Mario Carneiro, 27-Dec-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	vsfval.2	⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
	vsfval.3	⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
Assertion	vsfval	⊢ 𝑀 = ( /𝑔 ‘ 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		vsfval.2	⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
2		vsfval.3	⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
3		df-vs	⊢ −𝑣 = ( /𝑔 ∘ +𝑣 )
4	3	fveq1i	⊢ ( −𝑣 ‘ 𝑈 ) = ( ( /𝑔 ∘ +𝑣 ) ‘ 𝑈 )
5		fo1st	⊢ 1st : V –onto→ V
6		fof	⊢ ( 1st : V –onto→ V → 1st : V ⟶ V )
7	5 6	ax-mp	⊢ 1st : V ⟶ V
8		fco	⊢ ( ( 1st : V ⟶ V ∧ 1st : V ⟶ V ) → ( 1st ∘ 1st ) : V ⟶ V )
9	7 7 8	mp2an	⊢ ( 1st ∘ 1st ) : V ⟶ V
10		df-va	⊢ +𝑣 = ( 1st ∘ 1st )
11	10	feq1i	⊢ ( +𝑣 : V ⟶ V ↔ ( 1st ∘ 1st ) : V ⟶ V )
12	9 11	mpbir	⊢ +𝑣 : V ⟶ V
13		fvco3	⊢ ( ( +𝑣 : V ⟶ V ∧ 𝑈 ∈ V ) → ( ( /𝑔 ∘ +𝑣 ) ‘ 𝑈 ) = ( /𝑔 ‘ ( +𝑣 ‘ 𝑈 ) ) )
14	12 13	mpan	⊢ ( 𝑈 ∈ V → ( ( /𝑔 ∘ +𝑣 ) ‘ 𝑈 ) = ( /𝑔 ‘ ( +𝑣 ‘ 𝑈 ) ) )
15	4 14	syl5eq	⊢ ( 𝑈 ∈ V → ( −𝑣 ‘ 𝑈 ) = ( /𝑔 ‘ ( +𝑣 ‘ 𝑈 ) ) )
16		0ngrp	⊢ ¬ ∅ ∈ GrpOp
17		vex	⊢ 𝑔 ∈ V
18	17	rnex	⊢ ran 𝑔 ∈ V
19	18 18	mpoex	⊢ ( 𝑥 ∈ ran 𝑔 , 𝑦 ∈ ran 𝑔 ↦ ( 𝑥 𝑔 ( ( inv ‘ 𝑔 ) ‘ 𝑦 ) ) ) ∈ V
20		df-gdiv	⊢ /𝑔 = ( 𝑔 ∈ GrpOp ↦ ( 𝑥 ∈ ran 𝑔 , 𝑦 ∈ ran 𝑔 ↦ ( 𝑥 𝑔 ( ( inv ‘ 𝑔 ) ‘ 𝑦 ) ) ) )
21	19 20	dmmpti	⊢ dom /𝑔 = GrpOp
22	21	eleq2i	⊢ ( ∅ ∈ dom /𝑔 ↔ ∅ ∈ GrpOp )
23	16 22	mtbir	⊢ ¬ ∅ ∈ dom /𝑔
24		ndmfv	⊢ ( ¬ ∅ ∈ dom /𝑔 → ( /𝑔 ‘ ∅ ) = ∅ )
25	23 24	mp1i	⊢ ( ¬ 𝑈 ∈ V → ( /𝑔 ‘ ∅ ) = ∅ )
26		fvprc	⊢ ( ¬ 𝑈 ∈ V → ( +𝑣 ‘ 𝑈 ) = ∅ )
27	26	fveq2d	⊢ ( ¬ 𝑈 ∈ V → ( /𝑔 ‘ ( +𝑣 ‘ 𝑈 ) ) = ( /𝑔 ‘ ∅ ) )
28		fvprc	⊢ ( ¬ 𝑈 ∈ V → ( −𝑣 ‘ 𝑈 ) = ∅ )
29	25 27 28	3eqtr4rd	⊢ ( ¬ 𝑈 ∈ V → ( −𝑣 ‘ 𝑈 ) = ( /𝑔 ‘ ( +𝑣 ‘ 𝑈 ) ) )
30	15 29	pm2.61i	⊢ ( −𝑣 ‘ 𝑈 ) = ( /𝑔 ‘ ( +𝑣 ‘ 𝑈 ) )
31	1	fveq2i	⊢ ( /𝑔 ‘ 𝐺 ) = ( /𝑔 ‘ ( +𝑣 ‘ 𝑈 ) )
32	30 2 31	3eqtr4i	⊢ 𝑀 = ( /𝑔 ‘ 𝐺 )