Theorem 2arwcatlem5

Description: Lemma for 2arwcat . (Contributed by Zhi Wang, 5-Nov-2025)

	Ref	Expression
Hypotheses	2arwcatlem5.1	⊢ ( 𝜑 → ( 1 · 0 ) = 0 )
	2arwcatlem5.2	⊢ ( 𝜑 → ( 0 · 1 ) = 0 )
	2arwcatlem5.3	⊢ ( 𝜑 → ( 0 · 0 ) ∈ { 0 , 1 } )
Assertion	2arwcatlem5	⊢ ( 𝜑 → ( ( 0 · 0 ) · 0 ) = ( 0 · ( 0 · 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		2arwcatlem5.1	⊢ ( 𝜑 → ( 1 · 0 ) = 0 )
2		2arwcatlem5.2	⊢ ( 𝜑 → ( 0 · 1 ) = 0 )
3		2arwcatlem5.3	⊢ ( 𝜑 → ( 0 · 0 ) ∈ { 0 , 1 } )
4		simpr	⊢ ( ( 𝜑 ∧ ( 0 · 0 ) = 0 ) → ( 0 · 0 ) = 0 )
5	4	oveq1d	⊢ ( ( 𝜑 ∧ ( 0 · 0 ) = 0 ) → ( ( 0 · 0 ) · 0 ) = ( 0 · 0 ) )
6	4	oveq2d	⊢ ( ( 𝜑 ∧ ( 0 · 0 ) = 0 ) → ( 0 · ( 0 · 0 ) ) = ( 0 · 0 ) )
7	5 6	eqtr4d	⊢ ( ( 𝜑 ∧ ( 0 · 0 ) = 0 ) → ( ( 0 · 0 ) · 0 ) = ( 0 · ( 0 · 0 ) ) )
8	1 2	eqtr4d	⊢ ( 𝜑 → ( 1 · 0 ) = ( 0 · 1 ) )
9	8	adantr	⊢ ( ( 𝜑 ∧ ( 0 · 0 ) = 1 ) → ( 1 · 0 ) = ( 0 · 1 ) )
10		simpr	⊢ ( ( 𝜑 ∧ ( 0 · 0 ) = 1 ) → ( 0 · 0 ) = 1 )
11	10	oveq1d	⊢ ( ( 𝜑 ∧ ( 0 · 0 ) = 1 ) → ( ( 0 · 0 ) · 0 ) = ( 1 · 0 ) )
12	10	oveq2d	⊢ ( ( 𝜑 ∧ ( 0 · 0 ) = 1 ) → ( 0 · ( 0 · 0 ) ) = ( 0 · 1 ) )
13	9 11 12	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 0 · 0 ) = 1 ) → ( ( 0 · 0 ) · 0 ) = ( 0 · ( 0 · 0 ) ) )
14		ovex	⊢ ( 0 · 0 ) ∈ V
15	14	elpr	⊢ ( ( 0 · 0 ) ∈ { 0 , 1 } ↔ ( ( 0 · 0 ) = 0 ∨ ( 0 · 0 ) = 1 ) )
16	3 15	sylib	⊢ ( 𝜑 → ( ( 0 · 0 ) = 0 ∨ ( 0 · 0 ) = 1 ) )
17	7 13 16	mpjaodan	⊢ ( 𝜑 → ( ( 0 · 0 ) · 0 ) = ( 0 · ( 0 · 0 ) ) )