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 
|- ( ph -> I e. V )
caonncan.a 
|- ( ph -> A : I --> S )
caonncan.b 
|- ( ph -> B : I --> S )
caonncan.z 
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x M ( x M y ) ) = y )
Assertion caonncan 
|- ( ph -> ( A oF M ( A oF M B ) ) = B )

Proof

Step Hyp Ref Expression
1 caonncan.i 
 |-  ( ph -> I e. V )
2 caonncan.a 
 |-  ( ph -> A : I --> S )
3 caonncan.b 
 |-  ( ph -> B : I --> S )
4 caonncan.z 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x M ( x M y ) ) = y )
5 2 ffvelcdmda 
 |-  ( ( ph /\ z e. I ) -> ( A ` z ) e. S )
6 3 ffvelcdmda 
 |-  ( ( ph /\ z e. I ) -> ( B ` z ) e. S )
7 4 ralrimivva 
 |-  ( ph -> A. x e. S A. y e. S ( x M ( x M y ) ) = y )
8 7 adantr 
 |-  ( ( ph /\ z e. I ) -> A. x e. S A. y e. S ( x M ( x M y ) ) = y )
9 id 
 |-  ( x = ( A ` z ) -> x = ( A ` z ) )
10 oveq1 
 |-  ( x = ( A ` z ) -> ( x M y ) = ( ( A ` z ) M y ) )
11 9 10 oveq12d 
 |-  ( x = ( A ` z ) -> ( x M ( x M y ) ) = ( ( A ` z ) M ( ( A ` z ) M y ) ) )
12 11 eqeq1d 
 |-  ( x = ( A ` z ) -> ( ( x M ( x M y ) ) = y <-> ( ( A ` z ) M ( ( A ` z ) M y ) ) = y ) )
13 oveq2 
 |-  ( y = ( B ` z ) -> ( ( A ` z ) M y ) = ( ( A ` z ) M ( B ` z ) ) )
14 13 oveq2d 
 |-  ( y = ( B ` z ) -> ( ( A ` z ) M ( ( A ` z ) M y ) ) = ( ( A ` z ) M ( ( A ` z ) M ( B ` z ) ) ) )
15 id 
 |-  ( y = ( B ` z ) -> y = ( B ` z ) )
16 14 15 eqeq12d 
 |-  ( y = ( B ` z ) -> ( ( ( A ` z ) M ( ( A ` z ) M y ) ) = y <-> ( ( A ` z ) M ( ( A ` z ) M ( B ` z ) ) ) = ( B ` z ) ) )
17 12 16 rspc2va 
 |-  ( ( ( ( A ` z ) e. S /\ ( B ` z ) e. S ) /\ A. x e. S A. y e. S ( x M ( x M y ) ) = y ) -> ( ( A ` z ) M ( ( A ` z ) M ( B ` z ) ) ) = ( B ` z ) )
18 5 6 8 17 syl21anc 
 |-  ( ( ph /\ z e. I ) -> ( ( A ` z ) M ( ( A ` z ) M ( B ` z ) ) ) = ( B ` z ) )
19 18 mpteq2dva 
 |-  ( ph -> ( z e. I |-> ( ( A ` z ) M ( ( A ` z ) M ( B ` z ) ) ) ) = ( z e. I |-> ( B ` z ) ) )
20 fvexd 
 |-  ( ( ph /\ z e. I ) -> ( A ` z ) e. _V )
21 ovexd 
 |-  ( ( ph /\ z e. I ) -> ( ( A ` z ) M ( B ` z ) ) e. _V )
22 2 feqmptd 
 |-  ( ph -> A = ( z e. I |-> ( A ` z ) ) )
23 fvexd 
 |-  ( ( ph /\ z e. I ) -> ( B ` z ) e. _V )
24 3 feqmptd 
 |-  ( ph -> B = ( z e. I |-> ( B ` z ) ) )
25 1 20 23 22 24 offval2 
 |-  ( ph -> ( A oF M B ) = ( z e. I |-> ( ( A ` z ) M ( B ` z ) ) ) )
26 1 20 21 22 25 offval2 
 |-  ( ph -> ( A oF M ( A oF M B ) ) = ( z e. I |-> ( ( A ` z ) M ( ( A ` z ) M ( B ` z ) ) ) ) )
27 19 26 24 3eqtr4d 
 |-  ( ph -> ( A oF M ( A oF M B ) ) = B )