This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mndvass

Description: Tuple-wise associativity in monoids. (Contributed by Stefan O'Rear, 5-Sep-2015)

Ref Expression
Hypotheses mndvcl.b 
|- B = ( Base ` M )
mndvcl.p 
|- .+ = ( +g ` M )
Assertion mndvass 
|- ( ( M e. Mnd /\ ( X e. ( B ^m I ) /\ Y e. ( B ^m I ) /\ Z e. ( B ^m I ) ) ) -> ( ( X oF .+ Y ) oF .+ Z ) = ( X oF .+ ( Y oF .+ Z ) ) )

Proof

Step Hyp Ref Expression
1 mndvcl.b 
 |-  B = ( Base ` M )
2 mndvcl.p 
 |-  .+ = ( +g ` M )
3 elmapex 
 |-  ( X e. ( B ^m I ) -> ( B e. _V /\ I e. _V ) )
4 3 simprd 
 |-  ( X e. ( B ^m I ) -> I e. _V )
5 4 3ad2ant1 
 |-  ( ( X e. ( B ^m I ) /\ Y e. ( B ^m I ) /\ Z e. ( B ^m I ) ) -> I e. _V )
6 5 adantl 
 |-  ( ( M e. Mnd /\ ( X e. ( B ^m I ) /\ Y e. ( B ^m I ) /\ Z e. ( B ^m I ) ) ) -> I e. _V )
7 elmapi 
 |-  ( X e. ( B ^m I ) -> X : I --> B )
8 7 3ad2ant1 
 |-  ( ( X e. ( B ^m I ) /\ Y e. ( B ^m I ) /\ Z e. ( B ^m I ) ) -> X : I --> B )
9 8 adantl 
 |-  ( ( M e. Mnd /\ ( X e. ( B ^m I ) /\ Y e. ( B ^m I ) /\ Z e. ( B ^m I ) ) ) -> X : I --> B )
10 elmapi 
 |-  ( Y e. ( B ^m I ) -> Y : I --> B )
11 10 3ad2ant2 
 |-  ( ( X e. ( B ^m I ) /\ Y e. ( B ^m I ) /\ Z e. ( B ^m I ) ) -> Y : I --> B )
12 11 adantl 
 |-  ( ( M e. Mnd /\ ( X e. ( B ^m I ) /\ Y e. ( B ^m I ) /\ Z e. ( B ^m I ) ) ) -> Y : I --> B )
13 elmapi 
 |-  ( Z e. ( B ^m I ) -> Z : I --> B )
14 13 3ad2ant3 
 |-  ( ( X e. ( B ^m I ) /\ Y e. ( B ^m I ) /\ Z e. ( B ^m I ) ) -> Z : I --> B )
15 14 adantl 
 |-  ( ( M e. Mnd /\ ( X e. ( B ^m I ) /\ Y e. ( B ^m I ) /\ Z e. ( B ^m I ) ) ) -> Z : I --> B )
16 1 2 mndass 
 |-  ( ( M e. Mnd /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
17 16 adantlr 
 |-  ( ( ( M e. Mnd /\ ( X e. ( B ^m I ) /\ Y e. ( B ^m I ) /\ Z e. ( B ^m I ) ) ) /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
18 6 9 12 15 17 caofass 
 |-  ( ( M e. Mnd /\ ( X e. ( B ^m I ) /\ Y e. ( B ^m I ) /\ Z e. ( B ^m I ) ) ) -> ( ( X oF .+ Y ) oF .+ Z ) = ( X oF .+ ( Y oF .+ Z ) ) )