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 ( 𝜑𝐹 ∈ ( 𝑀 MndHom 𝑁 ) )
mhmimalem.s ( 𝜑𝑋 ⊆ ( Base ‘ 𝑀 ) )
mhmimalem.a ( 𝜑 = ( +g𝑀 ) )
mhmimalem.p ( 𝜑+ = ( +g𝑁 ) )
mhmimalem.c ( ( 𝜑𝑧𝑋𝑥𝑋 ) → ( 𝑧 𝑥 ) ∈ 𝑋 )
Assertion mhmimalem ( 𝜑 → ∀ 𝑥 ∈ ( 𝐹𝑋 ) ∀ 𝑦 ∈ ( 𝐹𝑋 ) ( 𝑥 + 𝑦 ) ∈ ( 𝐹𝑋 ) )

Proof

Step Hyp Ref Expression
1 mhmimalem.f ( 𝜑𝐹 ∈ ( 𝑀 MndHom 𝑁 ) )
2 mhmimalem.s ( 𝜑𝑋 ⊆ ( Base ‘ 𝑀 ) )
3 mhmimalem.a ( 𝜑 = ( +g𝑀 ) )
4 mhmimalem.p ( 𝜑+ = ( +g𝑁 ) )
5 mhmimalem.c ( ( 𝜑𝑧𝑋𝑥𝑋 ) → ( 𝑧 𝑥 ) ∈ 𝑋 )
6 1 adantr ( ( 𝜑 ∧ ( 𝑧𝑋𝑥𝑋 ) ) → 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) )
7 2 adantr ( ( 𝜑 ∧ ( 𝑧𝑋𝑥𝑋 ) ) → 𝑋 ⊆ ( Base ‘ 𝑀 ) )
8 simprl ( ( 𝜑 ∧ ( 𝑧𝑋𝑥𝑋 ) ) → 𝑧𝑋 )
9 7 8 sseldd ( ( 𝜑 ∧ ( 𝑧𝑋𝑥𝑋 ) ) → 𝑧 ∈ ( Base ‘ 𝑀 ) )
10 simprr ( ( 𝜑 ∧ ( 𝑧𝑋𝑥𝑋 ) ) → 𝑥𝑋 )
11 7 10 sseldd ( ( 𝜑 ∧ ( 𝑧𝑋𝑥𝑋 ) ) → 𝑥 ∈ ( Base ‘ 𝑀 ) )
12 eqid ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
13 eqid ( +g𝑀 ) = ( +g𝑀 )
14 eqid ( +g𝑁 ) = ( +g𝑁 )
15 12 13 14 mhmlin ( ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ∧ 𝑧 ∈ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( 𝐹 ‘ ( 𝑧 ( +g𝑀 ) 𝑥 ) ) = ( ( 𝐹𝑧 ) ( +g𝑁 ) ( 𝐹𝑥 ) ) )
16 6 9 11 15 syl3anc ( ( 𝜑 ∧ ( 𝑧𝑋𝑥𝑋 ) ) → ( 𝐹 ‘ ( 𝑧 ( +g𝑀 ) 𝑥 ) ) = ( ( 𝐹𝑧 ) ( +g𝑁 ) ( 𝐹𝑥 ) ) )
17 3 oveqd ( 𝜑 → ( 𝑧 𝑥 ) = ( 𝑧 ( +g𝑀 ) 𝑥 ) )
18 17 fveq2d ( 𝜑 → ( 𝐹 ‘ ( 𝑧 𝑥 ) ) = ( 𝐹 ‘ ( 𝑧 ( +g𝑀 ) 𝑥 ) ) )
19 4 oveqd ( 𝜑 → ( ( 𝐹𝑧 ) + ( 𝐹𝑥 ) ) = ( ( 𝐹𝑧 ) ( +g𝑁 ) ( 𝐹𝑥 ) ) )
20 18 19 eqeq12d ( 𝜑 → ( ( 𝐹 ‘ ( 𝑧 𝑥 ) ) = ( ( 𝐹𝑧 ) + ( 𝐹𝑥 ) ) ↔ ( 𝐹 ‘ ( 𝑧 ( +g𝑀 ) 𝑥 ) ) = ( ( 𝐹𝑧 ) ( +g𝑁 ) ( 𝐹𝑥 ) ) ) )
21 20 adantr ( ( 𝜑 ∧ ( 𝑧𝑋𝑥𝑋 ) ) → ( ( 𝐹 ‘ ( 𝑧 𝑥 ) ) = ( ( 𝐹𝑧 ) + ( 𝐹𝑥 ) ) ↔ ( 𝐹 ‘ ( 𝑧 ( +g𝑀 ) 𝑥 ) ) = ( ( 𝐹𝑧 ) ( +g𝑁 ) ( 𝐹𝑥 ) ) ) )
22 16 21 mpbird ( ( 𝜑 ∧ ( 𝑧𝑋𝑥𝑋 ) ) → ( 𝐹 ‘ ( 𝑧 𝑥 ) ) = ( ( 𝐹𝑧 ) + ( 𝐹𝑥 ) ) )
23 eqid ( Base ‘ 𝑁 ) = ( Base ‘ 𝑁 )
24 12 23 mhmf ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) → 𝐹 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑁 ) )
25 1 24 syl ( 𝜑𝐹 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑁 ) )
26 25 ffnd ( 𝜑𝐹 Fn ( Base ‘ 𝑀 ) )
27 26 adantr ( ( 𝜑 ∧ ( 𝑧𝑋𝑥𝑋 ) ) → 𝐹 Fn ( Base ‘ 𝑀 ) )
28 5 3expb ( ( 𝜑 ∧ ( 𝑧𝑋𝑥𝑋 ) ) → ( 𝑧 𝑥 ) ∈ 𝑋 )
29 fnfvima ( ( 𝐹 Fn ( Base ‘ 𝑀 ) ∧ 𝑋 ⊆ ( Base ‘ 𝑀 ) ∧ ( 𝑧 𝑥 ) ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑧 𝑥 ) ) ∈ ( 𝐹𝑋 ) )
30 27 7 28 29 syl3anc ( ( 𝜑 ∧ ( 𝑧𝑋𝑥𝑋 ) ) → ( 𝐹 ‘ ( 𝑧 𝑥 ) ) ∈ ( 𝐹𝑋 ) )
31 22 30 eqeltrrd ( ( 𝜑 ∧ ( 𝑧𝑋𝑥𝑋 ) ) → ( ( 𝐹𝑧 ) + ( 𝐹𝑥 ) ) ∈ ( 𝐹𝑋 ) )
32 31 anassrs ( ( ( 𝜑𝑧𝑋 ) ∧ 𝑥𝑋 ) → ( ( 𝐹𝑧 ) + ( 𝐹𝑥 ) ) ∈ ( 𝐹𝑋 ) )
33 32 ralrimiva ( ( 𝜑𝑧𝑋 ) → ∀ 𝑥𝑋 ( ( 𝐹𝑧 ) + ( 𝐹𝑥 ) ) ∈ ( 𝐹𝑋 ) )
34 oveq2 ( 𝑦 = ( 𝐹𝑥 ) → ( ( 𝐹𝑧 ) + 𝑦 ) = ( ( 𝐹𝑧 ) + ( 𝐹𝑥 ) ) )
35 34 eleq1d ( 𝑦 = ( 𝐹𝑥 ) → ( ( ( 𝐹𝑧 ) + 𝑦 ) ∈ ( 𝐹𝑋 ) ↔ ( ( 𝐹𝑧 ) + ( 𝐹𝑥 ) ) ∈ ( 𝐹𝑋 ) ) )
36 35 ralima ( ( 𝐹 Fn ( Base ‘ 𝑀 ) ∧ 𝑋 ⊆ ( Base ‘ 𝑀 ) ) → ( ∀ 𝑦 ∈ ( 𝐹𝑋 ) ( ( 𝐹𝑧 ) + 𝑦 ) ∈ ( 𝐹𝑋 ) ↔ ∀ 𝑥𝑋 ( ( 𝐹𝑧 ) + ( 𝐹𝑥 ) ) ∈ ( 𝐹𝑋 ) ) )
37 26 2 36 syl2anc ( 𝜑 → ( ∀ 𝑦 ∈ ( 𝐹𝑋 ) ( ( 𝐹𝑧 ) + 𝑦 ) ∈ ( 𝐹𝑋 ) ↔ ∀ 𝑥𝑋 ( ( 𝐹𝑧 ) + ( 𝐹𝑥 ) ) ∈ ( 𝐹𝑋 ) ) )
38 37 adantr ( ( 𝜑𝑧𝑋 ) → ( ∀ 𝑦 ∈ ( 𝐹𝑋 ) ( ( 𝐹𝑧 ) + 𝑦 ) ∈ ( 𝐹𝑋 ) ↔ ∀ 𝑥𝑋 ( ( 𝐹𝑧 ) + ( 𝐹𝑥 ) ) ∈ ( 𝐹𝑋 ) ) )
39 33 38 mpbird ( ( 𝜑𝑧𝑋 ) → ∀ 𝑦 ∈ ( 𝐹𝑋 ) ( ( 𝐹𝑧 ) + 𝑦 ) ∈ ( 𝐹𝑋 ) )
40 39 ralrimiva ( 𝜑 → ∀ 𝑧𝑋𝑦 ∈ ( 𝐹𝑋 ) ( ( 𝐹𝑧 ) + 𝑦 ) ∈ ( 𝐹𝑋 ) )
41 oveq1 ( 𝑥 = ( 𝐹𝑧 ) → ( 𝑥 + 𝑦 ) = ( ( 𝐹𝑧 ) + 𝑦 ) )
42 41 eleq1d ( 𝑥 = ( 𝐹𝑧 ) → ( ( 𝑥 + 𝑦 ) ∈ ( 𝐹𝑋 ) ↔ ( ( 𝐹𝑧 ) + 𝑦 ) ∈ ( 𝐹𝑋 ) ) )
43 42 ralbidv ( 𝑥 = ( 𝐹𝑧 ) → ( ∀ 𝑦 ∈ ( 𝐹𝑋 ) ( 𝑥 + 𝑦 ) ∈ ( 𝐹𝑋 ) ↔ ∀ 𝑦 ∈ ( 𝐹𝑋 ) ( ( 𝐹𝑧 ) + 𝑦 ) ∈ ( 𝐹𝑋 ) ) )
44 43 ralima ( ( 𝐹 Fn ( Base ‘ 𝑀 ) ∧ 𝑋 ⊆ ( Base ‘ 𝑀 ) ) → ( ∀ 𝑥 ∈ ( 𝐹𝑋 ) ∀ 𝑦 ∈ ( 𝐹𝑋 ) ( 𝑥 + 𝑦 ) ∈ ( 𝐹𝑋 ) ↔ ∀ 𝑧𝑋𝑦 ∈ ( 𝐹𝑋 ) ( ( 𝐹𝑧 ) + 𝑦 ) ∈ ( 𝐹𝑋 ) ) )
45 26 2 44 syl2anc ( 𝜑 → ( ∀ 𝑥 ∈ ( 𝐹𝑋 ) ∀ 𝑦 ∈ ( 𝐹𝑋 ) ( 𝑥 + 𝑦 ) ∈ ( 𝐹𝑋 ) ↔ ∀ 𝑧𝑋𝑦 ∈ ( 𝐹𝑋 ) ( ( 𝐹𝑧 ) + 𝑦 ) ∈ ( 𝐹𝑋 ) ) )
46 40 45 mpbird ( 𝜑 → ∀ 𝑥 ∈ ( 𝐹𝑋 ) ∀ 𝑦 ∈ ( 𝐹𝑋 ) ( 𝑥 + 𝑦 ) ∈ ( 𝐹𝑋 ) )