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 ⊢ + ˙ = + M
Assertion mndvass ⊢ M ∈ Mnd ∧ X ∈ B I ∧ Y ∈ B I ∧ Z ∈ B I → X + ˙ f Y + ˙ f Z = X + ˙ f Y + ˙ f Z

Proof

Step Hyp Ref Expression
1 mndvcl.b ⊢ B = Base M
2 mndvcl.p ⊢ + ˙ = + M
3 elmapex ⊢ X ∈ B I → B ∈ V ∧ I ∈ V
4 3 simprd ⊢ X ∈ B I → I ∈ V
5 4 3ad2ant1 ⊢ X ∈ B I ∧ Y ∈ B I ∧ Z ∈ B I → I ∈ V
6 5 adantl ⊢ M ∈ Mnd ∧ X ∈ B I ∧ Y ∈ B I ∧ Z ∈ B I → I ∈ V
7 elmapi ⊢ X ∈ B I → X : I ⟶ B
8 7 3ad2ant1 ⊢ X ∈ B I ∧ Y ∈ B I ∧ Z ∈ B I → X : I ⟶ B
9 8 adantl ⊢ M ∈ Mnd ∧ X ∈ B I ∧ Y ∈ B I ∧ Z ∈ B I → X : I ⟶ B
10 elmapi ⊢ Y ∈ B I → Y : I ⟶ B
11 10 3ad2ant2 ⊢ X ∈ B I ∧ Y ∈ B I ∧ Z ∈ B I → Y : I ⟶ B
12 11 adantl ⊢ M ∈ Mnd ∧ X ∈ B I ∧ Y ∈ B I ∧ Z ∈ B I → Y : I ⟶ B
13 elmapi ⊢ Z ∈ B I → Z : I ⟶ B
14 13 3ad2ant3 ⊢ X ∈ B I ∧ Y ∈ B I ∧ Z ∈ B I → Z : I ⟶ B
15 14 adantl ⊢ M ∈ Mnd ∧ X ∈ B I ∧ Y ∈ B I ∧ Z ∈ B I → Z : I ⟶ B
16 1 2 mndass ⊢ M ∈ Mnd ∧ x ∈ B ∧ y ∈ B ∧ z ∈ B → x + ˙ y + ˙ z = x + ˙ y + ˙ z
17 16 adantlr ⊢ M ∈ Mnd ∧ X ∈ B I ∧ Y ∈ B I ∧ Z ∈ B I ∧ x ∈ B ∧ y ∈ B ∧ z ∈ B → x + ˙ y + ˙ z = x + ˙ y + ˙ z
18 6 9 12 15 17 caofass ⊢ M ∈ Mnd ∧ X ∈ B I ∧ Y ∈ B I ∧ Z ∈ B I → X + ˙ f Y + ˙ f Z = X + ˙ f Y + ˙ f Z