Theorem signsw0g

Description: The neutral element of W . (Contributed by Thierry Arnoux, 9-Sep-2018)

	Ref	Expression
Hypotheses	signsw.p	⊢ ⨣ = ( 𝑎 ∈ { - 1 , 0 , 1 } , 𝑏 ∈ { - 1 , 0 , 1 } ↦ if ( 𝑏 = 0 , 𝑎 , 𝑏 ) )
	signsw.w	⊢ 𝑊 = { ⟨ ( Base ‘ ndx ) , { - 1 , 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ⨣ ⟩ }
Assertion	signsw0g	⊢ 0 = ( 0g ‘ 𝑊 )

Proof

Step	Hyp	Ref	Expression
1		signsw.p	⊢ ⨣ = ( 𝑎 ∈ { - 1 , 0 , 1 } , 𝑏 ∈ { - 1 , 0 , 1 } ↦ if ( 𝑏 = 0 , 𝑎 , 𝑏 ) )
2		signsw.w	⊢ 𝑊 = { ⟨ ( Base ‘ ndx ) , { - 1 , 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ⨣ ⟩ }
3		c0ex	⊢ 0 ∈ V
4	3	tpid2	⊢ 0 ∈ { - 1 , 0 , 1 }
5	1	signsw0glem	⊢ ∀ 𝑢 ∈ { - 1 , 0 , 1 } ( ( 0 ⨣ 𝑢 ) = 𝑢 ∧ ( 𝑢 ⨣ 0 ) = 𝑢 )
6	4 5	pm3.2i	⊢ ( 0 ∈ { - 1 , 0 , 1 } ∧ ∀ 𝑢 ∈ { - 1 , 0 , 1 } ( ( 0 ⨣ 𝑢 ) = 𝑢 ∧ ( 𝑢 ⨣ 0 ) = 𝑢 ) )
7	1 2	signswbase	⊢ { - 1 , 0 , 1 } = ( Base ‘ 𝑊 )
8		eqid	⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
9	1 2	signswplusg	⊢ ⨣ = ( +g ‘ 𝑊 )
10		oveq1	⊢ ( 𝑒 = 0 → ( 𝑒 ⨣ 𝑢 ) = ( 0 ⨣ 𝑢 ) )
11	10	eqeq1d	⊢ ( 𝑒 = 0 → ( ( 𝑒 ⨣ 𝑢 ) = 𝑢 ↔ ( 0 ⨣ 𝑢 ) = 𝑢 ) )
12	11	ovanraleqv	⊢ ( 𝑒 = 0 → ( ∀ 𝑢 ∈ { - 1 , 0 , 1 } ( ( 𝑒 ⨣ 𝑢 ) = 𝑢 ∧ ( 𝑢 ⨣ 𝑒 ) = 𝑢 ) ↔ ∀ 𝑢 ∈ { - 1 , 0 , 1 } ( ( 0 ⨣ 𝑢 ) = 𝑢 ∧ ( 𝑢 ⨣ 0 ) = 𝑢 ) ) )
13	12	rspcev	⊢ ( ( 0 ∈ { - 1 , 0 , 1 } ∧ ∀ 𝑢 ∈ { - 1 , 0 , 1 } ( ( 0 ⨣ 𝑢 ) = 𝑢 ∧ ( 𝑢 ⨣ 0 ) = 𝑢 ) ) → ∃ 𝑒 ∈ { - 1 , 0 , 1 } ∀ 𝑢 ∈ { - 1 , 0 , 1 } ( ( 𝑒 ⨣ 𝑢 ) = 𝑢 ∧ ( 𝑢 ⨣ 𝑒 ) = 𝑢 ) )
14	4 5 13	mp2an	⊢ ∃ 𝑒 ∈ { - 1 , 0 , 1 } ∀ 𝑢 ∈ { - 1 , 0 , 1 } ( ( 𝑒 ⨣ 𝑢 ) = 𝑢 ∧ ( 𝑢 ⨣ 𝑒 ) = 𝑢 )
15	14	a1i	⊢ ( ⊤ → ∃ 𝑒 ∈ { - 1 , 0 , 1 } ∀ 𝑢 ∈ { - 1 , 0 , 1 } ( ( 𝑒 ⨣ 𝑢 ) = 𝑢 ∧ ( 𝑢 ⨣ 𝑒 ) = 𝑢 ) )
16	7 8 9 15	ismgmid	⊢ ( ⊤ → ( ( 0 ∈ { - 1 , 0 , 1 } ∧ ∀ 𝑢 ∈ { - 1 , 0 , 1 } ( ( 0 ⨣ 𝑢 ) = 𝑢 ∧ ( 𝑢 ⨣ 0 ) = 𝑢 ) ) ↔ ( 0g ‘ 𝑊 ) = 0 ) )
17	16	mptru	⊢ ( ( 0 ∈ { - 1 , 0 , 1 } ∧ ∀ 𝑢 ∈ { - 1 , 0 , 1 } ( ( 0 ⨣ 𝑢 ) = 𝑢 ∧ ( 𝑢 ⨣ 0 ) = 𝑢 ) ) ↔ ( 0g ‘ 𝑊 ) = 0 )
18	6 17	mpbi	⊢ ( 0g ‘ 𝑊 ) = 0
19	18	eqcomi	⊢ 0 = ( 0g ‘ 𝑊 )