Theorem nvpncan2

Description: Cancellation law for vector subtraction. (Contributed by NM, 27-Dec-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nvpncan2.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	nvpncan2.2	⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
	nvpncan2.3	⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
Assertion	nvpncan2	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐺 𝐵 ) 𝑀 𝐴 ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		nvpncan2.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		nvpncan2.2	⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
3		nvpncan2.3	⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
4		simp1	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝑈 ∈ NrmCVec )
5	1 2	nvgcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 )
6		simp2	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
7		eqid	⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 )
8	1 2 7 3	nvmval	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐴 𝐺 𝐵 ) 𝑀 𝐴 ) = ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) )
9	4 5 6 8	syl3anc	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐺 𝐵 ) 𝑀 𝐴 ) = ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) )
10		simp3	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐵 ∈ 𝑋 )
11		neg1cn	⊢ - 1 ∈ ℂ
12	1 7	nvscl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ - 1 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ∈ 𝑋 )
13	11 12	mp3an2	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ∈ 𝑋 )
14	13	3adant3	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ∈ 𝑋 )
15	1 2	nvadd32	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) = ( ( 𝐴 𝐺 ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) 𝐺 𝐵 ) )
16	4 6 10 14 15	syl13anc	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) = ( ( 𝐴 𝐺 ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) 𝐺 𝐵 ) )
17		eqid	⊢ ( 0vec ‘ 𝑈 ) = ( 0vec ‘ 𝑈 )
18	1 2 7 17	nvrinv	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐺 ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) = ( 0vec ‘ 𝑈 ) )
19	18	3adant3	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) = ( 0vec ‘ 𝑈 ) )
20	19	oveq1d	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐺 ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) 𝐺 𝐵 ) = ( ( 0vec ‘ 𝑈 ) 𝐺 𝐵 ) )
21	1 2 17	nv0lid	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( ( 0vec ‘ 𝑈 ) 𝐺 𝐵 ) = 𝐵 )
22	21	3adant2	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 0vec ‘ 𝑈 ) 𝐺 𝐵 ) = 𝐵 )
23	20 22	eqtrd	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐺 ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) 𝐺 𝐵 ) = 𝐵 )
24	16 23	eqtrd	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) = 𝐵 )
25	9 24	eqtrd	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐺 𝐵 ) 𝑀 𝐴 ) = 𝐵 )