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

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 ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
Assertion rhmimasubrnglem ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubRng ‘ 𝑅 ) ) → ∀ 𝑥 ∈ ( 𝐹 “ 𝑋 ) ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( 𝑥 ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 rhmimasubrnglem.b ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
2 simpll ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubRng ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) )
3 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4 3 subrngss ⊢ ( 𝑋 ∈ ( SubRng ‘ 𝑅 ) → 𝑋 ⊆ ( Base ‘ 𝑅 ) )
5 1 3 mgpbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑀 )
6 4 5 sseqtrdi ⊢ ( 𝑋 ∈ ( SubRng ‘ 𝑅 ) → 𝑋 ⊆ ( Base ‘ 𝑀 ) )
7 6 adantl ⊢ ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubRng ‘ 𝑅 ) ) → 𝑋 ⊆ ( Base ‘ 𝑀 ) )
8 7 adantr ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubRng ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → 𝑋 ⊆ ( Base ‘ 𝑀 ) )
9 simprl ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubRng ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → 𝑧 ∈ 𝑋 )
10 8 9 sseldd ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubRng ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → 𝑧 ∈ ( Base ‘ 𝑀 ) )
11 simprr ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubRng ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → 𝑥 ∈ 𝑋 )
12 8 11 sseldd ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubRng ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → 𝑥 ∈ ( Base ‘ 𝑀 ) )
13 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
14 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
15 eqid ⊢ ( +g ‘ 𝑁 ) = ( +g ‘ 𝑁 )
16 13 14 15 mhmlin ⊢ ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( 𝐹 ‘ ( 𝑧 ( +g ‘ 𝑀 ) 𝑥 ) ) = ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ 𝑥 ) ) )
17 2 10 12 16 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubRng ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑧 ( +g ‘ 𝑀 ) 𝑥 ) ) = ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ 𝑥 ) ) )
18 eqid ⊢ ( Base ‘ 𝑁 ) = ( Base ‘ 𝑁 )
19 13 18 mhmf ⊢ ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) → 𝐹 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑁 ) )
20 19 adantr ⊢ ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubRng ‘ 𝑅 ) ) → 𝐹 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑁 ) )
21 20 ffnd ⊢ ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubRng ‘ 𝑅 ) ) → 𝐹 Fn ( Base ‘ 𝑀 ) )
22 21 adantr ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubRng ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → 𝐹 Fn ( Base ‘ 𝑀 ) )
23 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
24 1 23 mgpplusg ⊢ ( .r ‘ 𝑅 ) = ( +g ‘ 𝑀 )
25 24 eqcomi ⊢ ( +g ‘ 𝑀 ) = ( .r ‘ 𝑅 )
26 25 subrngmcl ⊢ ( ( 𝑋 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑧 ( +g ‘ 𝑀 ) 𝑥 ) ∈ 𝑋 )
27 26 3expb ⊢ ( ( 𝑋 ∈ ( SubRng ‘ 𝑅 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝑧 ( +g ‘ 𝑀 ) 𝑥 ) ∈ 𝑋 )
28 27 adantll ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubRng ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝑧 ( +g ‘ 𝑀 ) 𝑥 ) ∈ 𝑋 )
29 fnfvima ⊢ ( ( 𝐹 Fn ( Base ‘ 𝑀 ) ∧ 𝑋 ⊆ ( Base ‘ 𝑀 ) ∧ ( 𝑧 ( +g ‘ 𝑀 ) 𝑥 ) ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑧 ( +g ‘ 𝑀 ) 𝑥 ) ) ∈ ( 𝐹 “ 𝑋 ) )
30 22 8 28 29 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubRng ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑧 ( +g ‘ 𝑀 ) 𝑥 ) ) ∈ ( 𝐹 “ 𝑋 ) )
31 17 30 eqeltrrd ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubRng ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐹 “ 𝑋 ) )
32 31 anassrs ⊢ ( ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubRng ‘ 𝑅 ) ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐹 “ 𝑋 ) )
33 32 ralrimiva ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubRng ‘ 𝑅 ) ) ∧ 𝑧 ∈ 𝑋 ) → ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐹 “ 𝑋 ) )
34 oveq2 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) 𝑦 ) = ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ 𝑥 ) ) )
35 34 eleq1d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ↔ ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐹 “ 𝑋 ) ) )
36 35 ralima ⊢ ( ( 𝐹 Fn ( Base ‘ 𝑀 ) ∧ 𝑋 ⊆ ( Base ‘ 𝑀 ) ) → ( ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐹 “ 𝑋 ) ) )
37 21 7 36 syl2anc ⊢ ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubRng ‘ 𝑅 ) ) → ( ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐹 “ 𝑋 ) ) )
38 37 adantr ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubRng ‘ 𝑅 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐹 “ 𝑋 ) ) )
39 33 38 mpbird ⊢ ( ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubRng ‘ 𝑅 ) ) ∧ 𝑧 ∈ 𝑋 ) → ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) )
40 39 ralrimiva ⊢ ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubRng ‘ 𝑅 ) ) → ∀ 𝑧 ∈ 𝑋 ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) )
41 oveq1 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑧 ) → ( 𝑥 ( +g ‘ 𝑁 ) 𝑦 ) = ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) 𝑦 ) )
42 41 eleq1d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑧 ) → ( ( 𝑥 ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ↔ ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ) )
43 42 ralbidv ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑧 ) → ( ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( 𝑥 ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ↔ ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ) )
44 43 ralima ⊢ ( ( 𝐹 Fn ( Base ‘ 𝑀 ) ∧ 𝑋 ⊆ ( Base ‘ 𝑀 ) ) → ( ∀ 𝑥 ∈ ( 𝐹 “ 𝑋 ) ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( 𝑥 ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ↔ ∀ 𝑧 ∈ 𝑋 ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ) )
45 21 7 44 syl2anc ⊢ ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubRng ‘ 𝑅 ) ) → ( ∀ 𝑥 ∈ ( 𝐹 “ 𝑋 ) ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( 𝑥 ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ↔ ∀ 𝑧 ∈ 𝑋 ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) ) )
46 40 45 mpbird ⊢ ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑋 ∈ ( SubRng ‘ 𝑅 ) ) → ∀ 𝑥 ∈ ( 𝐹 “ 𝑋 ) ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( 𝑥 ( +g ‘ 𝑁 ) 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) )