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

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 ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐹 “ 𝑋 ) ∀ 𝑦 ∈ ( 𝐹 “ 𝑋 ) ( 𝑥 + 𝑦 ) ∈ ( 𝐹 “ 𝑋 ) )