Metamath Proof Explorer

Theorem lmhmimasvsca

Description: Value of the scalar product of the surjective image of a module. (Contributed by Thierry Arnoux, 2-Apr-2025)

Ref Expression
Hypotheses lmhmimasvsca.w 
|- W = ( F "s V )
lmhmimasvsca.b 
|- B = ( Base ` V )
lmhmimasvsca.c 
|- C = ( Base ` W )
lmhmimasvsca.x 
|- ( ph -> X e. K )
lmhmimasvsca.y 
|- ( ph -> Y e. B )
lmhmimasvsca.1 
|- ( ph -> F : B -onto-> C )
lmhmimasvsca.f 
|- ( ph -> F e. ( V LMHom W ) )
lmhmimasvsca.2 
|- .x. = ( .s ` V )
lmhmimasvsca.3 
|- .X. = ( .s ` W )
lmhmimasvsca.k 
|- K = ( Base ` ( Scalar ` V ) )
Assertion lmhmimasvsca 
|- ( ph -> ( X .X. ( F ` Y ) ) = ( F ` ( X .x. Y ) ) )

Proof

Step Hyp Ref Expression
1 lmhmimasvsca.w 
 |-  W = ( F "s V )
2 lmhmimasvsca.b 
 |-  B = ( Base ` V )
3 lmhmimasvsca.c 
 |-  C = ( Base ` W )
4 lmhmimasvsca.x 
 |-  ( ph -> X e. K )
5 lmhmimasvsca.y 
 |-  ( ph -> Y e. B )
6 lmhmimasvsca.1 
 |-  ( ph -> F : B -onto-> C )
7 lmhmimasvsca.f 
 |-  ( ph -> F e. ( V LMHom W ) )
8 lmhmimasvsca.2 
 |-  .x. = ( .s ` V )
9 lmhmimasvsca.3 
 |-  .X. = ( .s ` W )
10 lmhmimasvsca.k 
 |-  K = ( Base ` ( Scalar ` V ) )
11 1 a1i 
 |-  ( ph -> W = ( F "s V ) )
12 2 a1i 
 |-  ( ph -> B = ( Base ` V ) )
13 lmhmlmod1 
 |-  ( F e. ( V LMHom W ) -> V e. LMod )
14 7 13 syl 
 |-  ( ph -> V e. LMod )
15 eqid 
 |-  ( Scalar ` V ) = ( Scalar ` V )
16 simpr 
 |-  ( ( ( ph /\ ( p e. K /\ a e. B /\ q e. B ) ) /\ ( F ` a ) = ( F ` q ) ) -> ( F ` a ) = ( F ` q ) )
17 16 oveq2d 
 |-  ( ( ( ph /\ ( p e. K /\ a e. B /\ q e. B ) ) /\ ( F ` a ) = ( F ` q ) ) -> ( p .X. ( F ` a ) ) = ( p .X. ( F ` q ) ) )
18 7 ad2antrr 
 |-  ( ( ( ph /\ ( p e. K /\ a e. B /\ q e. B ) ) /\ ( F ` a ) = ( F ` q ) ) -> F e. ( V LMHom W ) )
19 simplr1 
 |-  ( ( ( ph /\ ( p e. K /\ a e. B /\ q e. B ) ) /\ ( F ` a ) = ( F ` q ) ) -> p e. K )
20 simplr2 
 |-  ( ( ( ph /\ ( p e. K /\ a e. B /\ q e. B ) ) /\ ( F ` a ) = ( F ` q ) ) -> a e. B )
21 15 10 2 8 9 lmhmlin 
 |-  ( ( F e. ( V LMHom W ) /\ p e. K /\ a e. B ) -> ( F ` ( p .x. a ) ) = ( p .X. ( F ` a ) ) )
22 18 19 20 21 syl3anc 
 |-  ( ( ( ph /\ ( p e. K /\ a e. B /\ q e. B ) ) /\ ( F ` a ) = ( F ` q ) ) -> ( F ` ( p .x. a ) ) = ( p .X. ( F ` a ) ) )
23 simplr3 
 |-  ( ( ( ph /\ ( p e. K /\ a e. B /\ q e. B ) ) /\ ( F ` a ) = ( F ` q ) ) -> q e. B )
24 15 10 2 8 9 lmhmlin 
 |-  ( ( F e. ( V LMHom W ) /\ p e. K /\ q e. B ) -> ( F ` ( p .x. q ) ) = ( p .X. ( F ` q ) ) )
25 18 19 23 24 syl3anc 
 |-  ( ( ( ph /\ ( p e. K /\ a e. B /\ q e. B ) ) /\ ( F ` a ) = ( F ` q ) ) -> ( F ` ( p .x. q ) ) = ( p .X. ( F ` q ) ) )
26 17 22 25 3eqtr4d 
 |-  ( ( ( ph /\ ( p e. K /\ a e. B /\ q e. B ) ) /\ ( F ` a ) = ( F ` q ) ) -> ( F ` ( p .x. a ) ) = ( F ` ( p .x. q ) ) )
27 26 ex 
 |-  ( ( ph /\ ( p e. K /\ a e. B /\ q e. B ) ) -> ( ( F ` a ) = ( F ` q ) -> ( F ` ( p .x. a ) ) = ( F ` ( p .x. q ) ) ) )
28 11 12 6 14 15 10 8 9 27 imasvscaval 
 |-  ( ( ph /\ X e. K /\ Y e. B ) -> ( X .X. ( F ` Y ) ) = ( F ` ( X .x. Y ) ) )
29 4 5 28 mpd3an23 
 |-  ( ph -> ( X .X. ( F ` Y ) ) = ( F ` ( X .x. Y ) ) )