Metamath Proof Explorer

Theorem lcdvs

Description: Scalar product for the closed kernel vector space dual. (Contributed by NM, 28-Mar-2015)

Ref Expression
Hypotheses lcdvs.h โŠข ๐ป = ( LHyp โ€˜ ๐พ )
lcdvs.u โŠข ๐‘ˆ = ( ( DVecH โ€˜ ๐พ ) โ€˜ ๐‘Š )
lcdvs.d โŠข ๐ท = ( LDual โ€˜ ๐‘ˆ )
lcdvs.t โŠข ยท = ( ยท๐‘  โ€˜ ๐ท )
lcdvs.c โŠข ๐ถ = ( ( LCDual โ€˜ ๐พ ) โ€˜ ๐‘Š )
lcdvs.m โŠข โˆ™ = ( ยท๐‘  โ€˜ ๐ถ )
lcdvs.k โŠข ( ๐œ‘ โ†’ ( ๐พ โˆˆ HL โˆง ๐‘Š โˆˆ ๐ป ) )
Assertion lcdvs ( ๐œ‘ โ†’ โˆ™ = ยท )

Proof

Step Hyp Ref Expression
1 lcdvs.h โŠข ๐ป = ( LHyp โ€˜ ๐พ )
2 lcdvs.u โŠข ๐‘ˆ = ( ( DVecH โ€˜ ๐พ ) โ€˜ ๐‘Š )
3 lcdvs.d โŠข ๐ท = ( LDual โ€˜ ๐‘ˆ )
4 lcdvs.t โŠข ยท = ( ยท๐‘  โ€˜ ๐ท )
5 lcdvs.c โŠข ๐ถ = ( ( LCDual โ€˜ ๐พ ) โ€˜ ๐‘Š )
6 lcdvs.m โŠข โˆ™ = ( ยท๐‘  โ€˜ ๐ถ )
7 lcdvs.k โŠข ( ๐œ‘ โ†’ ( ๐พ โˆˆ HL โˆง ๐‘Š โˆˆ ๐ป ) )
8 eqid โŠข ( ( ocH โ€˜ ๐พ ) โ€˜ ๐‘Š ) = ( ( ocH โ€˜ ๐พ ) โ€˜ ๐‘Š )
9 eqid โŠข ( LFnl โ€˜ ๐‘ˆ ) = ( LFnl โ€˜ ๐‘ˆ )
10 eqid โŠข ( LKer โ€˜ ๐‘ˆ ) = ( LKer โ€˜ ๐‘ˆ )
11 1 8 5 2 9 10 3 7 lcdval โŠข ( ๐œ‘ โ†’ ๐ถ = ( ๐ท โ†พs { ๐‘“ โˆˆ ( LFnl โ€˜ ๐‘ˆ ) โˆฃ ( ( ( ocH โ€˜ ๐พ ) โ€˜ ๐‘Š ) โ€˜ ( ( ( ocH โ€˜ ๐พ ) โ€˜ ๐‘Š ) โ€˜ ( ( LKer โ€˜ ๐‘ˆ ) โ€˜ ๐‘“ ) ) ) = ( ( LKer โ€˜ ๐‘ˆ ) โ€˜ ๐‘“ ) } ) )
12 11 fveq2d โŠข ( ๐œ‘ โ†’ ( ยท๐‘  โ€˜ ๐ถ ) = ( ยท๐‘  โ€˜ ( ๐ท โ†พs { ๐‘“ โˆˆ ( LFnl โ€˜ ๐‘ˆ ) โˆฃ ( ( ( ocH โ€˜ ๐พ ) โ€˜ ๐‘Š ) โ€˜ ( ( ( ocH โ€˜ ๐พ ) โ€˜ ๐‘Š ) โ€˜ ( ( LKer โ€˜ ๐‘ˆ ) โ€˜ ๐‘“ ) ) ) = ( ( LKer โ€˜ ๐‘ˆ ) โ€˜ ๐‘“ ) } ) ) )
13 fvex โŠข ( LFnl โ€˜ ๐‘ˆ ) โˆˆ V
14 13 rabex โŠข { ๐‘“ โˆˆ ( LFnl โ€˜ ๐‘ˆ ) โˆฃ ( ( ( ocH โ€˜ ๐พ ) โ€˜ ๐‘Š ) โ€˜ ( ( ( ocH โ€˜ ๐พ ) โ€˜ ๐‘Š ) โ€˜ ( ( LKer โ€˜ ๐‘ˆ ) โ€˜ ๐‘“ ) ) ) = ( ( LKer โ€˜ ๐‘ˆ ) โ€˜ ๐‘“ ) } โˆˆ V
15 eqid โŠข ( ๐ท โ†พs { ๐‘“ โˆˆ ( LFnl โ€˜ ๐‘ˆ ) โˆฃ ( ( ( ocH โ€˜ ๐พ ) โ€˜ ๐‘Š ) โ€˜ ( ( ( ocH โ€˜ ๐พ ) โ€˜ ๐‘Š ) โ€˜ ( ( LKer โ€˜ ๐‘ˆ ) โ€˜ ๐‘“ ) ) ) = ( ( LKer โ€˜ ๐‘ˆ ) โ€˜ ๐‘“ ) } ) = ( ๐ท โ†พs { ๐‘“ โˆˆ ( LFnl โ€˜ ๐‘ˆ ) โˆฃ ( ( ( ocH โ€˜ ๐พ ) โ€˜ ๐‘Š ) โ€˜ ( ( ( ocH โ€˜ ๐พ ) โ€˜ ๐‘Š ) โ€˜ ( ( LKer โ€˜ ๐‘ˆ ) โ€˜ ๐‘“ ) ) ) = ( ( LKer โ€˜ ๐‘ˆ ) โ€˜ ๐‘“ ) } )
16 15 4 ressvsca โŠข ( { ๐‘“ โˆˆ ( LFnl โ€˜ ๐‘ˆ ) โˆฃ ( ( ( ocH โ€˜ ๐พ ) โ€˜ ๐‘Š ) โ€˜ ( ( ( ocH โ€˜ ๐พ ) โ€˜ ๐‘Š ) โ€˜ ( ( LKer โ€˜ ๐‘ˆ ) โ€˜ ๐‘“ ) ) ) = ( ( LKer โ€˜ ๐‘ˆ ) โ€˜ ๐‘“ ) } โˆˆ V โ†’ ยท = ( ยท๐‘  โ€˜ ( ๐ท โ†พs { ๐‘“ โˆˆ ( LFnl โ€˜ ๐‘ˆ ) โˆฃ ( ( ( ocH โ€˜ ๐พ ) โ€˜ ๐‘Š ) โ€˜ ( ( ( ocH โ€˜ ๐พ ) โ€˜ ๐‘Š ) โ€˜ ( ( LKer โ€˜ ๐‘ˆ ) โ€˜ ๐‘“ ) ) ) = ( ( LKer โ€˜ ๐‘ˆ ) โ€˜ ๐‘“ ) } ) ) )
17 14 16 ax-mp โŠข ยท = ( ยท๐‘  โ€˜ ( ๐ท โ†พs { ๐‘“ โˆˆ ( LFnl โ€˜ ๐‘ˆ ) โˆฃ ( ( ( ocH โ€˜ ๐พ ) โ€˜ ๐‘Š ) โ€˜ ( ( ( ocH โ€˜ ๐พ ) โ€˜ ๐‘Š ) โ€˜ ( ( LKer โ€˜ ๐‘ˆ ) โ€˜ ๐‘“ ) ) ) = ( ( LKer โ€˜ ๐‘ˆ ) โ€˜ ๐‘“ ) } ) )
18 12 6 17 3eqtr4g โŠข ( ๐œ‘ โ†’ โˆ™ = ยท )