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 𝑇 ) ( 𝑔𝑋 ) = 𝐹 )