Metamath Proof Explorer


Theorem mhmlem

Description: Lemma for mhmmnd and ghmgrp . (Contributed by Paul Chapman, 25-Apr-2008) (Revised by Mario Carneiro, 12-May-2014) (Revised by Thierry Arnoux, 25-Jan-2020)

Ref Expression
Hypotheses ghmgrp.f φ x X y X F x + ˙ y = F x ˙ F y
mhmlem.a φ A X
mhmlem.b φ B X
Assertion mhmlem φ F A + ˙ B = F A ˙ F B

Proof

Step Hyp Ref Expression
1 ghmgrp.f φ x X y X F x + ˙ y = F x ˙ F y
2 mhmlem.a φ A X
3 mhmlem.b φ B X
4 id φ φ
5 eleq1 x = A x X A X
6 5 3anbi2d x = A φ x X y X φ A X y X
7 fvoveq1 x = A F x + ˙ y = F A + ˙ y
8 fveq2 x = A F x = F A
9 8 oveq1d x = A F x ˙ F y = F A ˙ F y
10 7 9 eqeq12d x = A F x + ˙ y = F x ˙ F y F A + ˙ y = F A ˙ F y
11 6 10 imbi12d x = A φ x X y X F x + ˙ y = F x ˙ F y φ A X y X F A + ˙ y = F A ˙ F y
12 eleq1 y = B y X B X
13 12 3anbi3d y = B φ A X y X φ A X B X
14 oveq2 y = B A + ˙ y = A + ˙ B
15 14 fveq2d y = B F A + ˙ y = F A + ˙ B
16 fveq2 y = B F y = F B
17 16 oveq2d y = B F A ˙ F y = F A ˙ F B
18 15 17 eqeq12d y = B F A + ˙ y = F A ˙ F y F A + ˙ B = F A ˙ F B
19 13 18 imbi12d y = B φ A X y X F A + ˙ y = F A ˙ F y φ A X B X F A + ˙ B = F A ˙ F B
20 11 19 1 vtocl2g A X B X φ A X B X F A + ˙ B = F A ˙ F B
21 2 3 20 syl2anc φ φ A X B X F A + ˙ B = F A ˙ F B
22 4 2 3 21 mp3and φ F A + ˙ B = F A ˙ F B