Metamath Proof Explorer

Theorem signsw0glem

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

Ref Expression
Hypothesis signsw.p ⊢ ⨣ ˙ = a ∈ − 1 0 1 , b ∈ − 1 0 1 ⟼ if b = 0 a b
Assertion signsw0glem ⊢ ∀ u ∈ − 1 0 1 0 ⨣ ˙ u = u ∧ u ⨣ ˙ 0 = u

Proof

Step Hyp Ref Expression
1 signsw.p ⊢ ⨣ ˙ = a ∈ − 1 0 1 , b ∈ − 1 0 1 ⟼ if b = 0 a b
2 c0ex ⊢ 0 ∈ V
3 2 tpid2 ⊢ 0 ∈ − 1 0 1
4 1 signspval ⊢ 0 ∈ − 1 0 1 ∧ u ∈ − 1 0 1 → 0 ⨣ ˙ u = if u = 0 0 u
5 3 4 mpan ⊢ u ∈ − 1 0 1 → 0 ⨣ ˙ u = if u = 0 0 u
6 iftrue ⊢ u = 0 → if u = 0 0 u = 0
7 id ⊢ u = 0 → u = 0
8 6 7 eqtr4d ⊢ u = 0 → if u = 0 0 u = u
9 iffalse ⊢ ¬ u = 0 → if u = 0 0 u = u
10 8 9 pm2.61i ⊢ if u = 0 0 u = u
11 5 10 eqtrdi ⊢ u ∈ − 1 0 1 → 0 ⨣ ˙ u = u
12 1 signspval ⊢ u ∈ − 1 0 1 ∧ 0 ∈ − 1 0 1 → u ⨣ ˙ 0 = if 0 = 0 u 0
13 3 12 mpan2 ⊢ u ∈ − 1 0 1 → u ⨣ ˙ 0 = if 0 = 0 u 0
14 eqid ⊢ 0 = 0
15 14 iftruei ⊢ if 0 = 0 u 0 = u
16 13 15 eqtrdi ⊢ u ∈ − 1 0 1 → u ⨣ ˙ 0 = u
17 11 16 jca ⊢ u ∈ − 1 0 1 → 0 ⨣ ˙ u = u ∧ u ⨣ ˙ 0 = u
18 17 rgen ⊢ ∀ u ∈ − 1 0 1 0 ⨣ ˙ u = u ∧ u ⨣ ˙ 0 = u