Theorem signsw0glem

Description: Neutral element property of .+^ . (Contributed by Thierry Arnoux, 9-Sep-2018)

	Ref	Expression
Hypothesis	signsw.p	⊢ ⨣ = ( 𝑎 ∈ { - 1 , 0 , 1 } , 𝑏 ∈ { - 1 , 0 , 1 } ↦ if ( 𝑏 = 0 , 𝑎 , 𝑏 ) )
Assertion	signsw0glem	⊢ ∀ 𝑢 ∈ { - 1 , 0 , 1 } ( ( 0 ⨣ 𝑢 ) = 𝑢 ∧ ( 𝑢 ⨣ 0 ) = 𝑢 )

Proof

Step	Hyp	Ref	Expression
1		signsw.p	⊢ ⨣ = ( 𝑎 ∈ { - 1 , 0 , 1 } , 𝑏 ∈ { - 1 , 0 , 1 } ↦ if ( 𝑏 = 0 , 𝑎 , 𝑏 ) )
2		c0ex	⊢ 0 ∈ V
3	2	tpid2	⊢ 0 ∈ { - 1 , 0 , 1 }
4	1	signspval	⊢ ( ( 0 ∈ { - 1 , 0 , 1 } ∧ 𝑢 ∈ { - 1 , 0 , 1 } ) → ( 0 ⨣ 𝑢 ) = if ( 𝑢 = 0 , 0 , 𝑢 ) )
5	3 4	mpan	⊢ ( 𝑢 ∈ { - 1 , 0 , 1 } → ( 0 ⨣ 𝑢 ) = if ( 𝑢 = 0 , 0 , 𝑢 ) )
6		iftrue	⊢ ( 𝑢 = 0 → if ( 𝑢 = 0 , 0 , 𝑢 ) = 0 )
7		id	⊢ ( 𝑢 = 0 → 𝑢 = 0 )
8	6 7	eqtr4d	⊢ ( 𝑢 = 0 → if ( 𝑢 = 0 , 0 , 𝑢 ) = 𝑢 )
9		iffalse	⊢ ( ¬ 𝑢 = 0 → if ( 𝑢 = 0 , 0 , 𝑢 ) = 𝑢 )
10	8 9	pm2.61i	⊢ if ( 𝑢 = 0 , 0 , 𝑢 ) = 𝑢
11	5 10	eqtrdi	⊢ ( 𝑢 ∈ { - 1 , 0 , 1 } → ( 0 ⨣ 𝑢 ) = 𝑢 )
12	1	signspval	⊢ ( ( 𝑢 ∈ { - 1 , 0 , 1 } ∧ 0 ∈ { - 1 , 0 , 1 } ) → ( 𝑢 ⨣ 0 ) = if ( 0 = 0 , 𝑢 , 0 ) )
13	3 12	mpan2	⊢ ( 𝑢 ∈ { - 1 , 0 , 1 } → ( 𝑢 ⨣ 0 ) = if ( 0 = 0 , 𝑢 , 0 ) )
14		eqid	⊢ 0 = 0
15	14	iftruei	⊢ if ( 0 = 0 , 𝑢 , 0 ) = 𝑢
16	13 15	eqtrdi	⊢ ( 𝑢 ∈ { - 1 , 0 , 1 } → ( 𝑢 ⨣ 0 ) = 𝑢 )
17	11 16	jca	⊢ ( 𝑢 ∈ { - 1 , 0 , 1 } → ( ( 0 ⨣ 𝑢 ) = 𝑢 ∧ ( 𝑢 ⨣ 0 ) = 𝑢 ) )
18	17	rgen	⊢ ∀ 𝑢 ∈ { - 1 , 0 , 1 } ( ( 0 ⨣ 𝑢 ) = 𝑢 ∧ ( 𝑢 ⨣ 0 ) = 𝑢 )