Metamath Proof Explorer

Theorem caonncan

Description: Transfer nncan -shaped laws to vectors of numbers. (Contributed by Stefan O'Rear, 27-Mar-2015)

Ref Expression
Hypotheses caonncan.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
caonncan.a ⊢ ( 𝜑 → 𝐴 : 𝐼 ⟶ 𝑆 )
caonncan.b ⊢ ( 𝜑 → 𝐵 : 𝐼 ⟶ 𝑆 )
caonncan.z ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 𝑀 ( 𝑥 𝑀 𝑦 ) ) = 𝑦 )
Assertion caonncan ( 𝜑 → ( 𝐴 ∘f 𝑀 ( 𝐴 ∘f 𝑀 𝐵 ) ) = 𝐵 )

Proof

Step Hyp Ref Expression
1 caonncan.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
2 caonncan.a ⊢ ( 𝜑 → 𝐴 : 𝐼 ⟶ 𝑆 )
3 caonncan.b ⊢ ( 𝜑 → 𝐵 : 𝐼 ⟶ 𝑆 )
4 caonncan.z ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 𝑀 ( 𝑥 𝑀 𝑦 ) ) = 𝑦 )
5 2 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐼 ) → ( 𝐴 ‘ 𝑧 ) ∈ 𝑆 )
6 3 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐼 ) → ( 𝐵 ‘ 𝑧 ) ∈ 𝑆 )
7 4 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 𝑀 ( 𝑥 𝑀 𝑦 ) ) = 𝑦 )
8 7 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐼 ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 𝑀 ( 𝑥 𝑀 𝑦 ) ) = 𝑦 )
9 id ⊢ ( 𝑥 = ( 𝐴 ‘ 𝑧 ) → 𝑥 = ( 𝐴 ‘ 𝑧 ) )
10 oveq1 ⊢ ( 𝑥 = ( 𝐴 ‘ 𝑧 ) → ( 𝑥 𝑀 𝑦 ) = ( ( 𝐴 ‘ 𝑧 ) 𝑀 𝑦 ) )
11 9 10 oveq12d ⊢ ( 𝑥 = ( 𝐴 ‘ 𝑧 ) → ( 𝑥 𝑀 ( 𝑥 𝑀 𝑦 ) ) = ( ( 𝐴 ‘ 𝑧 ) 𝑀 ( ( 𝐴 ‘ 𝑧 ) 𝑀 𝑦 ) ) )
12 11 eqeq1d ⊢ ( 𝑥 = ( 𝐴 ‘ 𝑧 ) → ( ( 𝑥 𝑀 ( 𝑥 𝑀 𝑦 ) ) = 𝑦 ↔ ( ( 𝐴 ‘ 𝑧 ) 𝑀 ( ( 𝐴 ‘ 𝑧 ) 𝑀 𝑦 ) ) = 𝑦 ) )
13 oveq2 ⊢ ( 𝑦 = ( 𝐵 ‘ 𝑧 ) → ( ( 𝐴 ‘ 𝑧 ) 𝑀 𝑦 ) = ( ( 𝐴 ‘ 𝑧 ) 𝑀 ( 𝐵 ‘ 𝑧 ) ) )
14 13 oveq2d ⊢ ( 𝑦 = ( 𝐵 ‘ 𝑧 ) → ( ( 𝐴 ‘ 𝑧 ) 𝑀 ( ( 𝐴 ‘ 𝑧 ) 𝑀 𝑦 ) ) = ( ( 𝐴 ‘ 𝑧 ) 𝑀 ( ( 𝐴 ‘ 𝑧 ) 𝑀 ( 𝐵 ‘ 𝑧 ) ) ) )
15 id ⊢ ( 𝑦 = ( 𝐵 ‘ 𝑧 ) → 𝑦 = ( 𝐵 ‘ 𝑧 ) )
16 14 15 eqeq12d ⊢ ( 𝑦 = ( 𝐵 ‘ 𝑧 ) → ( ( ( 𝐴 ‘ 𝑧 ) 𝑀 ( ( 𝐴 ‘ 𝑧 ) 𝑀 𝑦 ) ) = 𝑦 ↔ ( ( 𝐴 ‘ 𝑧 ) 𝑀 ( ( 𝐴 ‘ 𝑧 ) 𝑀 ( 𝐵 ‘ 𝑧 ) ) ) = ( 𝐵 ‘ 𝑧 ) ) )
17 12 16 rspc2va ⊢ ( ( ( ( 𝐴 ‘ 𝑧 ) ∈ 𝑆 ∧ ( 𝐵 ‘ 𝑧 ) ∈ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 𝑀 ( 𝑥 𝑀 𝑦 ) ) = 𝑦 ) → ( ( 𝐴 ‘ 𝑧 ) 𝑀 ( ( 𝐴 ‘ 𝑧 ) 𝑀 ( 𝐵 ‘ 𝑧 ) ) ) = ( 𝐵 ‘ 𝑧 ) )
18 5 6 8 17 syl21anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐼 ) → ( ( 𝐴 ‘ 𝑧 ) 𝑀 ( ( 𝐴 ‘ 𝑧 ) 𝑀 ( 𝐵 ‘ 𝑧 ) ) ) = ( 𝐵 ‘ 𝑧 ) )
19 18 mpteq2dva ⊢ ( 𝜑 → ( 𝑧 ∈ 𝐼 ↦ ( ( 𝐴 ‘ 𝑧 ) 𝑀 ( ( 𝐴 ‘ 𝑧 ) 𝑀 ( 𝐵 ‘ 𝑧 ) ) ) ) = ( 𝑧 ∈ 𝐼 ↦ ( 𝐵 ‘ 𝑧 ) ) )
20 fvexd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐼 ) → ( 𝐴 ‘ 𝑧 ) ∈ V )
21 ovexd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐼 ) → ( ( 𝐴 ‘ 𝑧 ) 𝑀 ( 𝐵 ‘ 𝑧 ) ) ∈ V )
22 2 feqmptd ⊢ ( 𝜑 → 𝐴 = ( 𝑧 ∈ 𝐼 ↦ ( 𝐴 ‘ 𝑧 ) ) )
23 fvexd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐼 ) → ( 𝐵 ‘ 𝑧 ) ∈ V )
24 3 feqmptd ⊢ ( 𝜑 → 𝐵 = ( 𝑧 ∈ 𝐼 ↦ ( 𝐵 ‘ 𝑧 ) ) )
25 1 20 23 22 24 offval2 ⊢ ( 𝜑 → ( 𝐴 ∘f 𝑀 𝐵 ) = ( 𝑧 ∈ 𝐼 ↦ ( ( 𝐴 ‘ 𝑧 ) 𝑀 ( 𝐵 ‘ 𝑧 ) ) ) )
26 1 20 21 22 25 offval2 ⊢ ( 𝜑 → ( 𝐴 ∘f 𝑀 ( 𝐴 ∘f 𝑀 𝐵 ) ) = ( 𝑧 ∈ 𝐼 ↦ ( ( 𝐴 ‘ 𝑧 ) 𝑀 ( ( 𝐴 ‘ 𝑧 ) 𝑀 ( 𝐵 ‘ 𝑧 ) ) ) ) )
27 19 26 24 3eqtr4d ⊢ ( 𝜑 → ( 𝐴 ∘f 𝑀 ( 𝐴 ∘f 𝑀 𝐵 ) ) = 𝐵 )