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 
|- B = ( Base ` S )
lspextmo.k 
|- K = ( LSpan ` S )
Assertion lspextmo 
|- ( ( X C_ B /\ ( K ` X ) = B ) -> E* g e. ( S LMHom T ) ( g |` X ) = F )

Proof

Step Hyp Ref Expression
1 lspextmo.b 
 |-  B = ( Base ` S )
2 lspextmo.k 
 |-  K = ( LSpan ` S )
3 eqtr3 
 |-  ( ( ( g |` X ) = F /\ ( h |` X ) = F ) -> ( g |` X ) = ( h |` X ) )
4 inss1 
 |-  ( g i^i h ) C_ g
5 dmss 
 |-  ( ( g i^i h ) C_ g -> dom ( g i^i h ) C_ dom g )
6 4 5 ax-mp 
 |-  dom ( g i^i h ) C_ dom g
7 eqid 
 |-  ( Base ` T ) = ( Base ` T )
8 1 7 lmhmf 
 |-  ( g e. ( S LMHom T ) -> g : B --> ( Base ` T ) )
9 8 ad2antrl 
 |-  ( ( ( X C_ B /\ ( K ` X ) = B ) /\ ( g e. ( S LMHom T ) /\ h e. ( S LMHom T ) ) ) -> g : B --> ( Base ` T ) )
10 9 ffnd 
 |-  ( ( ( X C_ B /\ ( K ` X ) = B ) /\ ( g e. ( S LMHom T ) /\ h e. ( S LMHom T ) ) ) -> g Fn B )
11 10 adantrr 
 |-  ( ( ( X C_ B /\ ( K ` X ) = B ) /\ ( ( g e. ( S LMHom T ) /\ h e. ( S LMHom T ) ) /\ X C_ dom ( g i^i h ) ) ) -> g Fn B )
12 11 fndmd 
 |-  ( ( ( X C_ B /\ ( K ` X ) = B ) /\ ( ( g e. ( S LMHom T ) /\ h e. ( S LMHom T ) ) /\ X C_ dom ( g i^i h ) ) ) -> dom g = B )
13 6 12 sseqtrid 
 |-  ( ( ( X C_ B /\ ( K ` X ) = B ) /\ ( ( g e. ( S LMHom T ) /\ h e. ( S LMHom T ) ) /\ X C_ dom ( g i^i h ) ) ) -> dom ( g i^i h ) C_ B )
14 simplr 
 |-  ( ( ( X C_ B /\ ( K ` X ) = B ) /\ ( ( g e. ( S LMHom T ) /\ h e. ( S LMHom T ) ) /\ X C_ dom ( g i^i h ) ) ) -> ( K ` X ) = B )
15 lmhmlmod1 
 |-  ( g e. ( S LMHom T ) -> S e. LMod )
16 15 adantr 
 |-  ( ( g e. ( S LMHom T ) /\ h e. ( S LMHom T ) ) -> S e. LMod )
17 16 ad2antrl 
 |-  ( ( ( X C_ B /\ ( K ` X ) = B ) /\ ( ( g e. ( S LMHom T ) /\ h e. ( S LMHom T ) ) /\ X C_ dom ( g i^i h ) ) ) -> S e. LMod )
18 eqid 
 |-  ( LSubSp ` S ) = ( LSubSp ` S )
19 18 lmhmeql 
 |-  ( ( g e. ( S LMHom T ) /\ h e. ( S LMHom T ) ) -> dom ( g i^i h ) e. ( LSubSp ` S ) )
20 19 ad2antrl 
 |-  ( ( ( X C_ B /\ ( K ` X ) = B ) /\ ( ( g e. ( S LMHom T ) /\ h e. ( S LMHom T ) ) /\ X C_ dom ( g i^i h ) ) ) -> dom ( g i^i h ) e. ( LSubSp ` S ) )
21 simprr 
 |-  ( ( ( X C_ B /\ ( K ` X ) = B ) /\ ( ( g e. ( S LMHom T ) /\ h e. ( S LMHom T ) ) /\ X C_ dom ( g i^i h ) ) ) -> X C_ dom ( g i^i h ) )
22 18 2 lspssp 
 |-  ( ( S e. LMod /\ dom ( g i^i h ) e. ( LSubSp ` S ) /\ X C_ dom ( g i^i h ) ) -> ( K ` X ) C_ dom ( g i^i h ) )
23 17 20 21 22 syl3anc 
 |-  ( ( ( X C_ B /\ ( K ` X ) = B ) /\ ( ( g e. ( S LMHom T ) /\ h e. ( S LMHom T ) ) /\ X C_ dom ( g i^i h ) ) ) -> ( K ` X ) C_ dom ( g i^i h ) )
24 14 23 eqsstrrd 
 |-  ( ( ( X C_ B /\ ( K ` X ) = B ) /\ ( ( g e. ( S LMHom T ) /\ h e. ( S LMHom T ) ) /\ X C_ dom ( g i^i h ) ) ) -> B C_ dom ( g i^i h ) )
25 13 24 eqssd 
 |-  ( ( ( X C_ B /\ ( K ` X ) = B ) /\ ( ( g e. ( S LMHom T ) /\ h e. ( S LMHom T ) ) /\ X C_ dom ( g i^i h ) ) ) -> dom ( g i^i h ) = B )
26 25 expr 
 |-  ( ( ( X C_ B /\ ( K ` X ) = B ) /\ ( g e. ( S LMHom T ) /\ h e. ( S LMHom T ) ) ) -> ( X C_ dom ( g i^i h ) -> dom ( g i^i h ) = B ) )
27 simprr 
 |-  ( ( ( X C_ B /\ ( K ` X ) = B ) /\ ( g e. ( S LMHom T ) /\ h e. ( S LMHom T ) ) ) -> h e. ( S LMHom T ) )
28 1 7 lmhmf 
 |-  ( h e. ( S LMHom T ) -> h : B --> ( Base ` T ) )
29 ffn 
 |-  ( h : B --> ( Base ` T ) -> h Fn B )
30 27 28 29 3syl 
 |-  ( ( ( X C_ B /\ ( K ` X ) = B ) /\ ( g e. ( S LMHom T ) /\ h e. ( S LMHom T ) ) ) -> h Fn B )
31 simpll 
 |-  ( ( ( X C_ B /\ ( K ` X ) = B ) /\ ( g e. ( S LMHom T ) /\ h e. ( S LMHom T ) ) ) -> X C_ B )
32 fnreseql 
 |-  ( ( g Fn B /\ h Fn B /\ X C_ B ) -> ( ( g |` X ) = ( h |` X ) <-> X C_ dom ( g i^i h ) ) )
33 10 30 31 32 syl3anc 
 |-  ( ( ( X C_ B /\ ( K ` X ) = B ) /\ ( g e. ( S LMHom T ) /\ h e. ( S LMHom T ) ) ) -> ( ( g |` X ) = ( h |` X ) <-> X C_ dom ( g i^i h ) ) )
34 fneqeql 
 |-  ( ( g Fn B /\ h Fn B ) -> ( g = h <-> dom ( g i^i h ) = B ) )
35 10 30 34 syl2anc 
 |-  ( ( ( X C_ B /\ ( K ` X ) = B ) /\ ( g e. ( S LMHom T ) /\ h e. ( S LMHom T ) ) ) -> ( g = h <-> dom ( g i^i h ) = B ) )
36 26 33 35 3imtr4d 
 |-  ( ( ( X C_ B /\ ( K ` X ) = B ) /\ ( g e. ( S LMHom T ) /\ h e. ( S LMHom T ) ) ) -> ( ( g |` X ) = ( h |` X ) -> g = h ) )
37 3 36 syl5 
 |-  ( ( ( X C_ B /\ ( K ` X ) = B ) /\ ( g e. ( S LMHom T ) /\ h e. ( S LMHom T ) ) ) -> ( ( ( g |` X ) = F /\ ( h |` X ) = F ) -> g = h ) )
38 37 ralrimivva 
 |-  ( ( X C_ B /\ ( K ` X ) = B ) -> A. g e. ( S LMHom T ) A. h e. ( S LMHom T ) ( ( ( g |` X ) = F /\ ( h |` X ) = F ) -> g = h ) )
39 reseq1 
 |-  ( g = h -> ( g |` X ) = ( h |` X ) )
40 39 eqeq1d 
 |-  ( g = h -> ( ( g |` X ) = F <-> ( h |` X ) = F ) )
41 40 rmo4 
 |-  ( E* g e. ( S LMHom T ) ( g |` X ) = F <-> A. g e. ( S LMHom T ) A. h e. ( S LMHom T ) ( ( ( g |` X ) = F /\ ( h |` X ) = F ) -> g = h ) )
42 38 41 sylibr 
 |-  ( ( X C_ B /\ ( K ` X ) = B ) -> E* g e. ( S LMHom T ) ( g |` X ) = F )