Theorem signspval

Description: The value of the skipping 0 sign operation. (Contributed by Thierry Arnoux, 9-Sep-2018)

	Ref	Expression
Hypothesis	signsw.p	⊢ ⨣ = ( 𝑎 ∈ { - 1 , 0 , 1 } , 𝑏 ∈ { - 1 , 0 , 1 } ↦ if ( 𝑏 = 0 , 𝑎 , 𝑏 ) )
Assertion	signspval	⊢ ( ( 𝑋 ∈ { - 1 , 0 , 1 } ∧ 𝑌 ∈ { - 1 , 0 , 1 } ) → ( 𝑋 ⨣ 𝑌 ) = if ( 𝑌 = 0 , 𝑋 , 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		signsw.p	⊢ ⨣ = ( 𝑎 ∈ { - 1 , 0 , 1 } , 𝑏 ∈ { - 1 , 0 , 1 } ↦ if ( 𝑏 = 0 , 𝑎 , 𝑏 ) )
2		ifcl	⊢ ( ( 𝑋 ∈ { - 1 , 0 , 1 } ∧ 𝑌 ∈ { - 1 , 0 , 1 } ) → if ( 𝑌 = 0 , 𝑋 , 𝑌 ) ∈ { - 1 , 0 , 1 } )
3		ifeq1	⊢ ( 𝑎 = 𝑋 → if ( 𝑏 = 0 , 𝑎 , 𝑏 ) = if ( 𝑏 = 0 , 𝑋 , 𝑏 ) )
4		eqeq1	⊢ ( 𝑏 = 𝑌 → ( 𝑏 = 0 ↔ 𝑌 = 0 ) )
5		id	⊢ ( 𝑏 = 𝑌 → 𝑏 = 𝑌 )
6	4 5	ifbieq2d	⊢ ( 𝑏 = 𝑌 → if ( 𝑏 = 0 , 𝑋 , 𝑏 ) = if ( 𝑌 = 0 , 𝑋 , 𝑌 ) )
7	3 6 1	ovmpog	⊢ ( ( 𝑋 ∈ { - 1 , 0 , 1 } ∧ 𝑌 ∈ { - 1 , 0 , 1 } ∧ if ( 𝑌 = 0 , 𝑋 , 𝑌 ) ∈ { - 1 , 0 , 1 } ) → ( 𝑋 ⨣ 𝑌 ) = if ( 𝑌 = 0 , 𝑋 , 𝑌 ) )
8	2 7	mpd3an3	⊢ ( ( 𝑋 ∈ { - 1 , 0 , 1 } ∧ 𝑌 ∈ { - 1 , 0 , 1 } ) → ( 𝑋 ⨣ 𝑌 ) = if ( 𝑌 = 0 , 𝑋 , 𝑌 ) )