Theorem 2arwcatlem2

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

	Ref	Expression
Hypotheses	2arwcatlem2.a	⊢ ( 𝜑 → 𝐴 = 𝑋 )
	2arwcatlem2.b	⊢ ( 𝜑 → 𝐵 = 𝑌 )
	2arwcatlem2.c	⊢ ( 𝜑 → 𝐶 = 𝑍 )
	2arwcatlem2.f	⊢ ( 𝜑 → ( 𝐹 = 0 ∨ 𝐹 = 1 ) )
	2arwcatlem2.1	⊢ ( 𝜑 → ( 1 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 1 ) = 1 )
	2arwcatlem2.0	⊢ ( 𝜑 → ( 1 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 0 ) = 0 )
Assertion	2arwcatlem2	⊢ ( 𝜑 → ( 1 ( ⟨ 𝐴 , 𝐵 ⟩ · 𝐶 ) 𝐹 ) = 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		2arwcatlem2.a	⊢ ( 𝜑 → 𝐴 = 𝑋 )
2		2arwcatlem2.b	⊢ ( 𝜑 → 𝐵 = 𝑌 )
3		2arwcatlem2.c	⊢ ( 𝜑 → 𝐶 = 𝑍 )
4		2arwcatlem2.f	⊢ ( 𝜑 → ( 𝐹 = 0 ∨ 𝐹 = 1 ) )
5		2arwcatlem2.1	⊢ ( 𝜑 → ( 1 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 1 ) = 1 )
6		2arwcatlem2.0	⊢ ( 𝜑 → ( 1 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 0 ) = 0 )
7	1 2	opeq12d	⊢ ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑋 , 𝑌 ⟩ )
8	7 3	oveq12d	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ · 𝐶 ) = ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) )
9	8	oveqd	⊢ ( 𝜑 → ( 1 ( ⟨ 𝐴 , 𝐵 ⟩ · 𝐶 ) 𝐹 ) = ( 1 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) )
10	6	adantr	⊢ ( ( 𝜑 ∧ 𝐹 = 0 ) → ( 1 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 0 ) = 0 )
11		simpr	⊢ ( ( 𝜑 ∧ 𝐹 = 0 ) → 𝐹 = 0 )
12	11	oveq2d	⊢ ( ( 𝜑 ∧ 𝐹 = 0 ) → ( 1 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) = ( 1 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 0 ) )
13	10 12 11	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝐹 = 0 ) → ( 1 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) = 𝐹 )
14	5	adantr	⊢ ( ( 𝜑 ∧ 𝐹 = 1 ) → ( 1 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 1 ) = 1 )
15		simpr	⊢ ( ( 𝜑 ∧ 𝐹 = 1 ) → 𝐹 = 1 )
16	15	oveq2d	⊢ ( ( 𝜑 ∧ 𝐹 = 1 ) → ( 1 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) = ( 1 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 1 ) )
17	14 16 15	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝐹 = 1 ) → ( 1 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) = 𝐹 )
18	13 17 4	mpjaodan	⊢ ( 𝜑 → ( 1 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) = 𝐹 )
19	9 18	eqtrd	⊢ ( 𝜑 → ( 1 ( ⟨ 𝐴 , 𝐵 ⟩ · 𝐶 ) 𝐹 ) = 𝐹 )