Metamath Proof Explorer

Theorem lspextmo

Description: A linear function is completely determined (or overdetermined) by its values on a spanning subset. (Contributed by Stefan O'Rear, 7-Mar-2015) (Revised by NM, 17-Jun-2017)

Ref Expression
Hypotheses lspextmo.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
lspextmo.k ⊢ 𝐾 = ( LSpan ‘ 𝑆 )
Assertion lspextmo ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) → ∃* 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ( 𝑔 ↾ 𝑋 ) = 𝐹 )

Proof

Step Hyp Ref Expression
1 lspextmo.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
2 lspextmo.k ⊢ 𝐾 = ( LSpan ‘ 𝑆 )
3 eqtr3 ⊢ ( ( ( 𝑔 ↾ 𝑋 ) = 𝐹 ∧ ( ℎ ↾ 𝑋 ) = 𝐹 ) → ( 𝑔 ↾ 𝑋 ) = ( ℎ ↾ 𝑋 ) )
4 inss1 ⊢ ( 𝑔 ∩ ℎ ) ⊆ 𝑔
5 dmss ⊢ ( ( 𝑔 ∩ ℎ ) ⊆ 𝑔 → dom ( 𝑔 ∩ ℎ ) ⊆ dom 𝑔 )
6 4 5 ax-mp ⊢ dom ( 𝑔 ∩ ℎ ) ⊆ dom 𝑔
7 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
8 1 7 lmhmf ⊢ ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑔 : 𝐵 ⟶ ( Base ‘ 𝑇 ) )
9 8 ad2antrl ⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ) → 𝑔 : 𝐵 ⟶ ( Base ‘ 𝑇 ) )
10 9 ffnd ⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ) → 𝑔 Fn 𝐵 )
11 10 adantrr ⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ 𝑋 ⊆ dom ( 𝑔 ∩ ℎ ) ) ) → 𝑔 Fn 𝐵 )
12 11 fndmd ⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ 𝑋 ⊆ dom ( 𝑔 ∩ ℎ ) ) ) → dom 𝑔 = 𝐵 )
13 6 12 sseqtrid ⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ 𝑋 ⊆ dom ( 𝑔 ∩ ℎ ) ) ) → dom ( 𝑔 ∩ ℎ ) ⊆ 𝐵 )
14 simplr ⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ 𝑋 ⊆ dom ( 𝑔 ∩ ℎ ) ) ) → ( 𝐾 ‘ 𝑋 ) = 𝐵 )
15 lmhmlmod1 ⊢ ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑆 ∈ LMod )
16 15 adantr ⊢ ( ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) → 𝑆 ∈ LMod )
17 16 ad2antrl ⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ 𝑋 ⊆ dom ( 𝑔 ∩ ℎ ) ) ) → 𝑆 ∈ LMod )
18 eqid ⊢ ( LSubSp ‘ 𝑆 ) = ( LSubSp ‘ 𝑆 )
19 18 lmhmeql ⊢ ( ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) → dom ( 𝑔 ∩ ℎ ) ∈ ( LSubSp ‘ 𝑆 ) )
20 19 ad2antrl ⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ 𝑋 ⊆ dom ( 𝑔 ∩ ℎ ) ) ) → dom ( 𝑔 ∩ ℎ ) ∈ ( LSubSp ‘ 𝑆 ) )
21 simprr ⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ 𝑋 ⊆ dom ( 𝑔 ∩ ℎ ) ) ) → 𝑋 ⊆ dom ( 𝑔 ∩ ℎ ) )
22 18 2 lspssp ⊢ ( ( 𝑆 ∈ LMod ∧ dom ( 𝑔 ∩ ℎ ) ∈ ( LSubSp ‘ 𝑆 ) ∧ 𝑋 ⊆ dom ( 𝑔 ∩ ℎ ) ) → ( 𝐾 ‘ 𝑋 ) ⊆ dom ( 𝑔 ∩ ℎ ) )
23 17 20 21 22 syl3anc ⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ 𝑋 ⊆ dom ( 𝑔 ∩ ℎ ) ) ) → ( 𝐾 ‘ 𝑋 ) ⊆ dom ( 𝑔 ∩ ℎ ) )
24 14 23 eqsstrrd ⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ 𝑋 ⊆ dom ( 𝑔 ∩ ℎ ) ) ) → 𝐵 ⊆ dom ( 𝑔 ∩ ℎ ) )
25 13 24 eqssd ⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ∧ 𝑋 ⊆ dom ( 𝑔 ∩ ℎ ) ) ) → dom ( 𝑔 ∩ ℎ ) = 𝐵 )
26 25 expr ⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ) → ( 𝑋 ⊆ dom ( 𝑔 ∩ ℎ ) → dom ( 𝑔 ∩ ℎ ) = 𝐵 ) )
27 simprr ⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ) → ℎ ∈ ( 𝑆 LMHom 𝑇 ) )
28 1 7 lmhmf ⊢ ( ℎ ∈ ( 𝑆 LMHom 𝑇 ) → ℎ : 𝐵 ⟶ ( Base ‘ 𝑇 ) )
29 ffn ⊢ ( ℎ : 𝐵 ⟶ ( Base ‘ 𝑇 ) → ℎ Fn 𝐵 )
30 27 28 29 3syl ⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ) → ℎ Fn 𝐵 )
31 simpll ⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ) → 𝑋 ⊆ 𝐵 )
32 fnreseql ⊢ ( ( 𝑔 Fn 𝐵 ∧ ℎ Fn 𝐵 ∧ 𝑋 ⊆ 𝐵 ) → ( ( 𝑔 ↾ 𝑋 ) = ( ℎ ↾ 𝑋 ) ↔ 𝑋 ⊆ dom ( 𝑔 ∩ ℎ ) ) )
33 10 30 31 32 syl3anc ⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ) → ( ( 𝑔 ↾ 𝑋 ) = ( ℎ ↾ 𝑋 ) ↔ 𝑋 ⊆ dom ( 𝑔 ∩ ℎ ) ) )
34 fneqeql ⊢ ( ( 𝑔 Fn 𝐵 ∧ ℎ Fn 𝐵 ) → ( 𝑔 = ℎ ↔ dom ( 𝑔 ∩ ℎ ) = 𝐵 ) )
35 10 30 34 syl2anc ⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ) → ( 𝑔 = ℎ ↔ dom ( 𝑔 ∩ ℎ ) = 𝐵 ) )
36 26 33 35 3imtr4d ⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ) → ( ( 𝑔 ↾ 𝑋 ) = ( ℎ ↾ 𝑋 ) → 𝑔 = ℎ ) )
37 3 36 syl5 ⊢ ( ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∧ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ) ) → ( ( ( 𝑔 ↾ 𝑋 ) = 𝐹 ∧ ( ℎ ↾ 𝑋 ) = 𝐹 ) → 𝑔 = ℎ ) )
38 37 ralrimivva ⊢ ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) → ∀ 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∀ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ( ( ( 𝑔 ↾ 𝑋 ) = 𝐹 ∧ ( ℎ ↾ 𝑋 ) = 𝐹 ) → 𝑔 = ℎ ) )
39 reseq1 ⊢ ( 𝑔 = ℎ → ( 𝑔 ↾ 𝑋 ) = ( ℎ ↾ 𝑋 ) )
40 39 eqeq1d ⊢ ( 𝑔 = ℎ → ( ( 𝑔 ↾ 𝑋 ) = 𝐹 ↔ ( ℎ ↾ 𝑋 ) = 𝐹 ) )
41 40 rmo4 ⊢ ( ∃* 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ( 𝑔 ↾ 𝑋 ) = 𝐹 ↔ ∀ 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ∀ ℎ ∈ ( 𝑆 LMHom 𝑇 ) ( ( ( 𝑔 ↾ 𝑋 ) = 𝐹 ∧ ( ℎ ↾ 𝑋 ) = 𝐹 ) → 𝑔 = ℎ ) )
42 38 41 sylibr ⊢ ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) → ∃* 𝑔 ∈ ( 𝑆 LMHom 𝑇 ) ( 𝑔 ↾ 𝑋 ) = 𝐹 )