Metamath Proof Explorer

Theorem rhmimasubrnglem

Description: Lemma for rhmimasubrng : Modified part of mhmima . (Contributed by Mario Carneiro, 10-Mar-2015) (Revised by AV, 16-Feb-2025)

Ref Expression
Hypothesis rhmimasubrnglem.b 
|- M = ( mulGrp ` R )
Assertion rhmimasubrnglem 
|- ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) -> A. x e. ( F " X ) A. y e. ( F " X ) ( x ( +g ` N ) y ) e. ( F " X ) )

Proof

Step Hyp Ref Expression
1 rhmimasubrnglem.b 
 |-  M = ( mulGrp ` R )
2 simpll 
 |-  ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ ( z e. X /\ x e. X ) ) -> F e. ( M MndHom N ) )
3 eqid 
 |-  ( Base ` R ) = ( Base ` R )
4 3 subrngss 
 |-  ( X e. ( SubRng ` R ) -> X C_ ( Base ` R ) )
5 1 3 mgpbas 
 |-  ( Base ` R ) = ( Base ` M )
6 4 5 sseqtrdi 
 |-  ( X e. ( SubRng ` R ) -> X C_ ( Base ` M ) )
7 6 adantl 
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) -> X C_ ( Base ` M ) )
8 7 adantr 
 |-  ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ ( z e. X /\ x e. X ) ) -> X C_ ( Base ` M ) )
9 simprl 
 |-  ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ ( z e. X /\ x e. X ) ) -> z e. X )
10 8 9 sseldd 
 |-  ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ ( z e. X /\ x e. X ) ) -> z e. ( Base ` M ) )
11 simprr 
 |-  ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ ( z e. X /\ x e. X ) ) -> x e. X )
12 8 11 sseldd 
 |-  ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ ( z e. X /\ x e. X ) ) -> x e. ( Base ` M ) )
13 eqid 
 |-  ( Base ` M ) = ( Base ` M )
14 eqid 
 |-  ( +g ` M ) = ( +g ` M )
15 eqid 
 |-  ( +g ` N ) = ( +g ` N )
16 13 14 15 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 ) ) )
17 2 10 12 16 syl3anc 
 |-  ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ ( z e. X /\ x e. X ) ) -> ( F ` ( z ( +g ` M ) x ) ) = ( ( F ` z ) ( +g ` N ) ( F ` x ) ) )
18 eqid 
 |-  ( Base ` N ) = ( Base ` N )
19 13 18 mhmf 
 |-  ( F e. ( M MndHom N ) -> F : ( Base ` M ) --> ( Base ` N ) )
20 19 adantr 
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) -> F : ( Base ` M ) --> ( Base ` N ) )
21 20 ffnd 
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) -> F Fn ( Base ` M ) )
22 21 adantr 
 |-  ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ ( z e. X /\ x e. X ) ) -> F Fn ( Base ` M ) )
23 eqid 
 |-  ( .r ` R ) = ( .r ` R )
24 1 23 mgpplusg 
 |-  ( .r ` R ) = ( +g ` M )
25 24 eqcomi 
 |-  ( +g ` M ) = ( .r ` R )
26 25 subrngmcl 
 |-  ( ( X e. ( SubRng ` R ) /\ z e. X /\ x e. X ) -> ( z ( +g ` M ) x ) e. X )
27 26 3expb 
 |-  ( ( X e. ( SubRng ` R ) /\ ( z e. X /\ x e. X ) ) -> ( z ( +g ` M ) x ) e. X )
28 27 adantll 
 |-  ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ ( z e. X /\ x e. X ) ) -> ( z ( +g ` M ) x ) e. X )
29 fnfvima 
 |-  ( ( F Fn ( Base ` M ) /\ X C_ ( Base ` M ) /\ ( z ( +g ` M ) x ) e. X ) -> ( F ` ( z ( +g ` M ) x ) ) e. ( F " X ) )
30 22 8 28 29 syl3anc 
 |-  ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ ( z e. X /\ x e. X ) ) -> ( F ` ( z ( +g ` M ) x ) ) e. ( F " X ) )
31 17 30 eqeltrrd 
 |-  ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ ( z e. X /\ x e. X ) ) -> ( ( F ` z ) ( +g ` N ) ( F ` x ) ) e. ( F " X ) )
32 31 anassrs 
 |-  ( ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ z e. X ) /\ x e. X ) -> ( ( F ` z ) ( +g ` N ) ( F ` x ) ) e. ( F " X ) )
33 32 ralrimiva 
 |-  ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ z e. X ) -> A. x e. X ( ( F ` z ) ( +g ` N ) ( F ` x ) ) e. ( F " X ) )
34 oveq2 
 |-  ( y = ( F ` x ) -> ( ( F ` z ) ( +g ` N ) y ) = ( ( F ` z ) ( +g ` N ) ( F ` x ) ) )
35 34 eleq1d 
 |-  ( y = ( F ` x ) -> ( ( ( F ` z ) ( +g ` N ) y ) e. ( F " X ) <-> ( ( F ` z ) ( +g ` N ) ( F ` x ) ) e. ( F " X ) ) )
36 35 ralima 
 |-  ( ( F Fn ( Base ` M ) /\ X C_ ( Base ` M ) ) -> ( A. y e. ( F " X ) ( ( F ` z ) ( +g ` N ) y ) e. ( F " X ) <-> A. x e. X ( ( F ` z ) ( +g ` N ) ( F ` x ) ) e. ( F " X ) ) )
37 21 7 36 syl2anc 
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) -> ( A. y e. ( F " X ) ( ( F ` z ) ( +g ` N ) y ) e. ( F " X ) <-> A. x e. X ( ( F ` z ) ( +g ` N ) ( F ` x ) ) e. ( F " X ) ) )
38 37 adantr 
 |-  ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ z e. X ) -> ( A. y e. ( F " X ) ( ( F ` z ) ( +g ` N ) y ) e. ( F " X ) <-> A. x e. X ( ( F ` z ) ( +g ` N ) ( F ` x ) ) e. ( F " X ) ) )
39 33 38 mpbird 
 |-  ( ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) /\ z e. X ) -> A. y e. ( F " X ) ( ( F ` z ) ( +g ` N ) y ) e. ( F " X ) )
40 39 ralrimiva 
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) -> A. z e. X A. y e. ( F " X ) ( ( F ` z ) ( +g ` N ) y ) e. ( F " X ) )
41 oveq1 
 |-  ( x = ( F ` z ) -> ( x ( +g ` N ) y ) = ( ( F ` z ) ( +g ` N ) y ) )
42 41 eleq1d 
 |-  ( x = ( F ` z ) -> ( ( x ( +g ` N ) y ) e. ( F " X ) <-> ( ( F ` z ) ( +g ` N ) y ) e. ( F " X ) ) )
43 42 ralbidv 
 |-  ( x = ( F ` z ) -> ( A. y e. ( F " X ) ( x ( +g ` N ) y ) e. ( F " X ) <-> A. y e. ( F " X ) ( ( F ` z ) ( +g ` N ) 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 ( +g ` N ) y ) e. ( F " X ) <-> A. z e. X A. y e. ( F " X ) ( ( F ` z ) ( +g ` N ) y ) e. ( F " X ) ) )
45 21 7 44 syl2anc 
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) -> ( A. x e. ( F " X ) A. y e. ( F " X ) ( x ( +g ` N ) y ) e. ( F " X ) <-> A. z e. X A. y e. ( F " X ) ( ( F ` z ) ( +g ` N ) y ) e. ( F " X ) ) )
46 40 45 mpbird 
 |-  ( ( F e. ( M MndHom N ) /\ X e. ( SubRng ` R ) ) -> A. x e. ( F " X ) A. y e. ( F " X ) ( x ( +g ` N ) y ) e. ( F " X ) )