Metamath Proof Explorer


Theorem mhmimalem

Description: Lemma for mhmima and similar theorems, formerly part of proof for mhmima . (Contributed by Mario Carneiro, 10-Mar-2015) (Revised by AV, 16-Feb-2025)

Ref Expression
Hypotheses mhmimalem.f
|- ( ph -> F e. ( M MndHom N ) )
mhmimalem.s
|- ( ph -> X C_ ( Base ` M ) )
mhmimalem.a
|- ( ph -> .(+) = ( +g ` M ) )
mhmimalem.p
|- ( ph -> .+ = ( +g ` N ) )
mhmimalem.c
|- ( ( ph /\ z e. X /\ x e. X ) -> ( z .(+) x ) e. X )
Assertion mhmimalem
|- ( ph -> A. x e. ( F " X ) A. y e. ( F " X ) ( x .+ y ) e. ( F " X ) )

Proof

Step Hyp Ref Expression
1 mhmimalem.f
 |-  ( ph -> F e. ( M MndHom N ) )
2 mhmimalem.s
 |-  ( ph -> X C_ ( Base ` M ) )
3 mhmimalem.a
 |-  ( ph -> .(+) = ( +g ` M ) )
4 mhmimalem.p
 |-  ( ph -> .+ = ( +g ` N ) )
5 mhmimalem.c
 |-  ( ( ph /\ z e. X /\ x e. X ) -> ( z .(+) x ) e. X )
6 1 adantr
 |-  ( ( ph /\ ( z e. X /\ x e. X ) ) -> F e. ( M MndHom N ) )
7 2 adantr
 |-  ( ( ph /\ ( z e. X /\ x e. X ) ) -> X C_ ( Base ` M ) )
8 simprl
 |-  ( ( ph /\ ( z e. X /\ x e. X ) ) -> z e. X )
9 7 8 sseldd
 |-  ( ( ph /\ ( z e. X /\ x e. X ) ) -> z e. ( Base ` M ) )
10 simprr
 |-  ( ( ph /\ ( z e. X /\ x e. X ) ) -> x e. X )
11 7 10 sseldd
 |-  ( ( ph /\ ( z e. X /\ x e. X ) ) -> x e. ( Base ` M ) )
12 eqid
 |-  ( Base ` M ) = ( Base ` M )
13 eqid
 |-  ( +g ` M ) = ( +g ` M )
14 eqid
 |-  ( +g ` N ) = ( +g ` N )
15 12 13 14 mhmlin
 |-  ( ( F e. ( M MndHom N ) /\ z e. ( Base ` M ) /\ x e. ( Base ` M ) ) -> ( F ` ( z ( +g ` M ) x ) ) = ( ( F ` z ) ( +g ` N ) ( F ` x ) ) )
16 6 9 11 15 syl3anc
 |-  ( ( ph /\ ( z e. X /\ x e. X ) ) -> ( F ` ( z ( +g ` M ) x ) ) = ( ( F ` z ) ( +g ` N ) ( F ` x ) ) )
17 3 oveqd
 |-  ( ph -> ( z .(+) x ) = ( z ( +g ` M ) x ) )
18 17 fveq2d
 |-  ( ph -> ( F ` ( z .(+) x ) ) = ( F ` ( z ( +g ` M ) x ) ) )
19 4 oveqd
 |-  ( ph -> ( ( F ` z ) .+ ( F ` x ) ) = ( ( F ` z ) ( +g ` N ) ( F ` x ) ) )
20 18 19 eqeq12d
 |-  ( ph -> ( ( F ` ( z .(+) x ) ) = ( ( F ` z ) .+ ( F ` x ) ) <-> ( F ` ( z ( +g ` M ) x ) ) = ( ( F ` z ) ( +g ` N ) ( F ` x ) ) ) )
21 20 adantr
 |-  ( ( ph /\ ( z e. X /\ x e. X ) ) -> ( ( F ` ( z .(+) x ) ) = ( ( F ` z ) .+ ( F ` x ) ) <-> ( F ` ( z ( +g ` M ) x ) ) = ( ( F ` z ) ( +g ` N ) ( F ` x ) ) ) )
22 16 21 mpbird
 |-  ( ( ph /\ ( z e. X /\ x e. X ) ) -> ( F ` ( z .(+) x ) ) = ( ( F ` z ) .+ ( F ` x ) ) )
23 eqid
 |-  ( Base ` N ) = ( Base ` N )
24 12 23 mhmf
 |-  ( F e. ( M MndHom N ) -> F : ( Base ` M ) --> ( Base ` N ) )
25 1 24 syl
 |-  ( ph -> F : ( Base ` M ) --> ( Base ` N ) )
26 25 ffnd
 |-  ( ph -> F Fn ( Base ` M ) )
27 26 adantr
 |-  ( ( ph /\ ( z e. X /\ x e. X ) ) -> F Fn ( Base ` M ) )
28 5 3expb
 |-  ( ( ph /\ ( z e. X /\ x e. X ) ) -> ( z .(+) x ) e. X )
29 fnfvima
 |-  ( ( F Fn ( Base ` M ) /\ X C_ ( Base ` M ) /\ ( z .(+) x ) e. X ) -> ( F ` ( z .(+) x ) ) e. ( F " X ) )
30 27 7 28 29 syl3anc
 |-  ( ( ph /\ ( z e. X /\ x e. X ) ) -> ( F ` ( z .(+) x ) ) e. ( F " X ) )
31 22 30 eqeltrrd
 |-  ( ( ph /\ ( z e. X /\ x e. X ) ) -> ( ( F ` z ) .+ ( F ` x ) ) e. ( F " X ) )
32 31 anassrs
 |-  ( ( ( ph /\ z e. X ) /\ x e. X ) -> ( ( F ` z ) .+ ( F ` x ) ) e. ( F " X ) )
33 32 ralrimiva
 |-  ( ( ph /\ z e. X ) -> A. x e. X ( ( F ` z ) .+ ( F ` x ) ) e. ( F " X ) )
34 oveq2
 |-  ( y = ( F ` x ) -> ( ( F ` z ) .+ y ) = ( ( F ` z ) .+ ( F ` x ) ) )
35 34 eleq1d
 |-  ( y = ( F ` x ) -> ( ( ( F ` z ) .+ y ) e. ( F " X ) <-> ( ( F ` z ) .+ ( F ` x ) ) e. ( F " X ) ) )
36 35 ralima
 |-  ( ( F Fn ( Base ` M ) /\ X C_ ( Base ` M ) ) -> ( A. y e. ( F " X ) ( ( F ` z ) .+ y ) e. ( F " X ) <-> A. x e. X ( ( F ` z ) .+ ( F ` x ) ) e. ( F " X ) ) )
37 26 2 36 syl2anc
 |-  ( ph -> ( A. y e. ( F " X ) ( ( F ` z ) .+ y ) e. ( F " X ) <-> A. x e. X ( ( F ` z ) .+ ( F ` x ) ) e. ( F " X ) ) )
38 37 adantr
 |-  ( ( ph /\ z e. X ) -> ( A. y e. ( F " X ) ( ( F ` z ) .+ y ) e. ( F " X ) <-> A. x e. X ( ( F ` z ) .+ ( F ` x ) ) e. ( F " X ) ) )
39 33 38 mpbird
 |-  ( ( ph /\ z e. X ) -> A. y e. ( F " X ) ( ( F ` z ) .+ y ) e. ( F " X ) )
40 39 ralrimiva
 |-  ( ph -> A. z e. X A. y e. ( F " X ) ( ( F ` z ) .+ y ) e. ( F " X ) )
41 oveq1
 |-  ( x = ( F ` z ) -> ( x .+ y ) = ( ( F ` z ) .+ y ) )
42 41 eleq1d
 |-  ( x = ( F ` z ) -> ( ( x .+ y ) e. ( F " X ) <-> ( ( F ` z ) .+ y ) e. ( F " X ) ) )
43 42 ralbidv
 |-  ( x = ( F ` z ) -> ( A. y e. ( F " X ) ( x .+ y ) e. ( F " X ) <-> A. y e. ( F " X ) ( ( F ` z ) .+ y ) e. ( F " X ) ) )
44 43 ralima
 |-  ( ( F Fn ( Base ` M ) /\ X C_ ( Base ` M ) ) -> ( A. x e. ( F " X ) A. y e. ( F " X ) ( x .+ y ) e. ( F " X ) <-> A. z e. X A. y e. ( F " X ) ( ( F ` z ) .+ y ) e. ( F " X ) ) )
45 26 2 44 syl2anc
 |-  ( ph -> ( A. x e. ( F " X ) A. y e. ( F " X ) ( x .+ y ) e. ( F " X ) <-> A. z e. X A. y e. ( F " X ) ( ( F ` z ) .+ y ) e. ( F " X ) ) )
46 40 45 mpbird
 |-  ( ph -> A. x e. ( F " X ) A. y e. ( F " X ) ( x .+ y ) e. ( F " X ) )