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

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 
|- ( ( ph /\ x e. X /\ y e. X ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )
mhmlem.a 
|- ( ph -> A e. X )
mhmlem.b 
|- ( ph -> B e. X )
Assertion mhmlem 
|- ( ph -> ( F ` ( A .+ B ) ) = ( ( F ` A ) .+^ ( F ` B ) ) )

Proof

Step Hyp Ref Expression
1 ghmgrp.f 
 |-  ( ( ph /\ x e. X /\ y e. X ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )
2 mhmlem.a 
 |-  ( ph -> A e. X )
3 mhmlem.b 
 |-  ( ph -> B e. X )
4 id 
 |-  ( ph -> ph )
5 eleq1 
 |-  ( x = A -> ( x e. X <-> A e. X ) )
6 5 3anbi2d 
 |-  ( x = A -> ( ( ph /\ x e. X /\ y e. X ) <-> ( ph /\ A e. X /\ y e. 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 -> ( ( ( ph /\ x e. X /\ y e. X ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) ) <-> ( ( ph /\ A e. X /\ y e. X ) -> ( F ` ( A .+ y ) ) = ( ( F ` A ) .+^ ( F ` y ) ) ) ) )
12 eleq1 
 |-  ( y = B -> ( y e. X <-> B e. X ) )
13 12 3anbi3d 
 |-  ( y = B -> ( ( ph /\ A e. X /\ y e. X ) <-> ( ph /\ A e. X /\ B e. 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 -> ( ( ( ph /\ A e. X /\ y e. X ) -> ( F ` ( A .+ y ) ) = ( ( F ` A ) .+^ ( F ` y ) ) ) <-> ( ( ph /\ A e. X /\ B e. X ) -> ( F ` ( A .+ B ) ) = ( ( F ` A ) .+^ ( F ` B ) ) ) ) )
20 11 19 1 vtocl2g 
 |-  ( ( A e. X /\ B e. X ) -> ( ( ph /\ A e. X /\ B e. X ) -> ( F ` ( A .+ B ) ) = ( ( F ` A ) .+^ ( F ` B ) ) ) )
21 2 3 20 syl2anc 
 |-  ( ph -> ( ( ph /\ A e. X /\ B e. X ) -> ( F ` ( A .+ B ) ) = ( ( F ` A ) .+^ ( F ` B ) ) ) )
22 4 2 3 21 mp3and 
 |-  ( ph -> ( F ` ( A .+ B ) ) = ( ( F ` A ) .+^ ( F ` B ) ) )