This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lspsnsub

Description: Swapping subtraction order does not change the span of a singleton. (Contributed by NM, 4-Apr-2015)

Ref Expression
Hypotheses lspsnsub.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lspsnsub.s ⊢ − = ( -g ‘ 𝑊 )
lspsnsub.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lspsnsub.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
lspsnsub.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
lspsnsub.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
Assertion lspsnsub ( 𝜑 → ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) = ( 𝑁 ‘ { ( 𝑌 − 𝑋 ) } ) )

Proof

Step Hyp Ref Expression
1 lspsnsub.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lspsnsub.s ⊢ − = ( -g ‘ 𝑊 )
3 lspsnsub.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4 lspsnsub.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
5 lspsnsub.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
6 lspsnsub.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
7 1 2 lmodvsubcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 − 𝑌 ) ∈ 𝑉 )
8 4 5 6 7 syl3anc ⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) ∈ 𝑉 )
9 eqid ⊢ ( invg ‘ 𝑊 ) = ( invg ‘ 𝑊 )
10 1 9 3 lspsnneg ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑋 − 𝑌 ) ∈ 𝑉 ) → ( 𝑁 ‘ { ( ( invg ‘ 𝑊 ) ‘ ( 𝑋 − 𝑌 ) ) } ) = ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) )
11 4 8 10 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { ( ( invg ‘ 𝑊 ) ‘ ( 𝑋 − 𝑌 ) ) } ) = ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) )
12 lmodgrp ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp )
13 4 12 syl ⊢ ( 𝜑 → 𝑊 ∈ Grp )
14 1 2 9 grpinvsub ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( invg ‘ 𝑊 ) ‘ ( 𝑋 − 𝑌 ) ) = ( 𝑌 − 𝑋 ) )
15 13 5 6 14 syl3anc ⊢ ( 𝜑 → ( ( invg ‘ 𝑊 ) ‘ ( 𝑋 − 𝑌 ) ) = ( 𝑌 − 𝑋 ) )
16 15 sneqd ⊢ ( 𝜑 → { ( ( invg ‘ 𝑊 ) ‘ ( 𝑋 − 𝑌 ) ) } = { ( 𝑌 − 𝑋 ) } )
17 16 fveq2d ⊢ ( 𝜑 → ( 𝑁 ‘ { ( ( invg ‘ 𝑊 ) ‘ ( 𝑋 − 𝑌 ) ) } ) = ( 𝑁 ‘ { ( 𝑌 − 𝑋 ) } ) )
18 11 17 eqtr3d ⊢ ( 𝜑 → ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) = ( 𝑁 ‘ { ( 𝑌 − 𝑋 ) } ) )