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	⊢ 1^st : V –onto→ V
6		fof	⊢ ( 1^st : V –onto→ V → 1^st : V ⟶ V )
7	5 6	ax-mp	⊢ 1^st : V ⟶ V
8		fco	⊢ ( ( 1^st : V ⟶ V ∧ 1^st : V ⟶ V ) → ( 1^st ∘ 1^st ) : V ⟶ V )
9	7 7 8	mp2an	⊢ ( 1^st ∘ 1^st ) : V ⟶ V
10		df-va	⊢ +_𝑣 = ( 1^st ∘ 1^st )
11	10	feq1i	⊢ ( +_𝑣 : V ⟶ V ↔ ( 1^st ∘ 1^st ) : V ⟶ V )
12	9 11	mpbir	⊢ +_𝑣 : V ⟶ V
13		fvco3	⊢ ( ( +_𝑣 : V ⟶ V ∧ 𝑈 ∈ V ) → ( ( /_𝑔 ∘ +_𝑣 ) ‘ 𝑈 ) = ( /_𝑔 ‘ ( +_𝑣 ‘ 𝑈 ) ) )
14	12 13	mpan	⊢ ( 𝑈 ∈ V → ( ( /_𝑔 ∘ +_𝑣 ) ‘ 𝑈 ) = ( /_𝑔 ‘ ( +_𝑣 ‘ 𝑈 ) ) )
15	4 14	eqtrid	⊢ ( 𝑈 ∈ 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	⊢ 𝑀 = ( /_𝑔 ‘ 𝐺 )

Metamath Proof Explorer

Theorem vsfval

Proof