Metamath Proof Explorer

Theorem 2arwcatlem4

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 )
2arwcatlem3.0 ⊢ ( 𝜑 → ( 0 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 1 ) = 0 )
2arwcatlem4.0 ⊢ ( 𝜑 → ( 1 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 0 ) = 0 )
2arwcatlem4.00 ⊢ ( 𝜑 → ( 0 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 0 ) ∈ { 0 , 1 } )
2arwcatlem4.g ⊢ ( 𝜑 → ( 𝐺 = 0 ∨ 𝐺 = 1 ) )
Assertion 2arwcatlem4 ( 𝜑 → ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ · 𝐶 ) 𝐹 ) ∈ { 0 , 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 2arwcatlem3.0 ⊢ ( 𝜑 → ( 0 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 1 ) = 0 )
7 2arwcatlem4.0 ⊢ ( 𝜑 → ( 1 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 0 ) = 0 )
8 2arwcatlem4.00 ⊢ ( 𝜑 → ( 0 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 0 ) ∈ { 0 , 1 } )
9 2arwcatlem4.g ⊢ ( 𝜑 → ( 𝐺 = 0 ∨ 𝐺 = 1 ) )
10 1 2 opeq12d ⊢ ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑋 , 𝑌 ⟩ )
11 10 3 oveq12d ⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ · 𝐶 ) = ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) )
12 11 oveqd ⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ · 𝐶 ) 𝐹 ) = ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) )
13 simpr ⊢ ( ( ( 𝜑 ∧ 𝐹 = 0 ) ∧ 𝐺 = 0 ) → 𝐺 = 0 )
14 simplr ⊢ ( ( ( 𝜑 ∧ 𝐹 = 0 ) ∧ 𝐺 = 0 ) → 𝐹 = 0 )
15 13 14 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝐹 = 0 ) ∧ 𝐺 = 0 ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) = ( 0 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 0 ) )
16 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 = 0 ) ∧ 𝐺 = 0 ) → ( 0 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 0 ) ∈ { 0 , 1 } )
17 15 16 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝐹 = 0 ) ∧ 𝐺 = 0 ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ { 0 , 1 } )
18 simpr ⊢ ( ( ( 𝜑 ∧ 𝐹 = 0 ) ∧ 𝐺 = 1 ) → 𝐺 = 1 )
19 simplr ⊢ ( ( ( 𝜑 ∧ 𝐹 = 0 ) ∧ 𝐺 = 1 ) → 𝐹 = 0 )
20 18 19 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝐹 = 0 ) ∧ 𝐺 = 1 ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) = ( 1 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 0 ) )
21 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 = 0 ) ∧ 𝐺 = 1 ) → ( 1 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 0 ) = 0 )
22 20 21 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝐹 = 0 ) ∧ 𝐺 = 1 ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) = 0 )
23 ovex ⊢ ( 1 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 0 ) ∈ V
24 7 23 eqeltrrdi ⊢ ( 𝜑 → 0 ∈ V )
25 prid1g ⊢ ( 0 ∈ V → 0 ∈ { 0 , 1 } )
26 24 25 syl ⊢ ( 𝜑 → 0 ∈ { 0 , 1 } )
27 26 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 = 0 ) ∧ 𝐺 = 1 ) → 0 ∈ { 0 , 1 } )
28 22 27 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝐹 = 0 ) ∧ 𝐺 = 1 ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ { 0 , 1 } )
29 9 adantr ⊢ ( ( 𝜑 ∧ 𝐹 = 0 ) → ( 𝐺 = 0 ∨ 𝐺 = 1 ) )
30 17 28 29 mpjaodan ⊢ ( ( 𝜑 ∧ 𝐹 = 0 ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ { 0 , 1 } )
31 simpr ⊢ ( ( ( 𝜑 ∧ 𝐹 = 1 ) ∧ 𝐺 = 0 ) → 𝐺 = 0 )
32 simplr ⊢ ( ( ( 𝜑 ∧ 𝐹 = 1 ) ∧ 𝐺 = 0 ) → 𝐹 = 1 )
33 31 32 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝐹 = 1 ) ∧ 𝐺 = 0 ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) = ( 0 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 1 ) )
34 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 = 1 ) ∧ 𝐺 = 0 ) → ( 0 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 1 ) = 0 )
35 33 34 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝐹 = 1 ) ∧ 𝐺 = 0 ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) = 0 )
36 26 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 = 1 ) ∧ 𝐺 = 0 ) → 0 ∈ { 0 , 1 } )
37 35 36 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝐹 = 1 ) ∧ 𝐺 = 0 ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ { 0 , 1 } )
38 simpr ⊢ ( ( ( 𝜑 ∧ 𝐹 = 1 ) ∧ 𝐺 = 1 ) → 𝐺 = 1 )
39 simplr ⊢ ( ( ( 𝜑 ∧ 𝐹 = 1 ) ∧ 𝐺 = 1 ) → 𝐹 = 1 )
40 38 39 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝐹 = 1 ) ∧ 𝐺 = 1 ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) = ( 1 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 1 ) )
41 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 = 1 ) ∧ 𝐺 = 1 ) → ( 1 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 1 ) = 1 )
42 40 41 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝐹 = 1 ) ∧ 𝐺 = 1 ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) = 1 )
43 ovex ⊢ ( 1 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 1 ) ∈ V
44 5 43 eqeltrrdi ⊢ ( 𝜑 → 1 ∈ V )
45 prid2g ⊢ ( 1 ∈ V → 1 ∈ { 0 , 1 } )
46 44 45 syl ⊢ ( 𝜑 → 1 ∈ { 0 , 1 } )
47 46 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 = 1 ) ∧ 𝐺 = 1 ) → 1 ∈ { 0 , 1 } )
48 42 47 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝐹 = 1 ) ∧ 𝐺 = 1 ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ { 0 , 1 } )
49 9 adantr ⊢ ( ( 𝜑 ∧ 𝐹 = 1 ) → ( 𝐺 = 0 ∨ 𝐺 = 1 ) )
50 37 48 49 mpjaodan ⊢ ( ( 𝜑 ∧ 𝐹 = 1 ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ { 0 , 1 } )
51 30 50 4 mpjaodan ⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ∈ { 0 , 1 } )
52 12 51 eqeltrd ⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝐴 , 𝐵 ⟩ · 𝐶 ) 𝐹 ) ∈ { 0 , 1 } )