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 ) )