Metamath Proof Explorer


Theorem hdmap14lem4a

Description: Simplify ( A \ { Q } ) in hdmap14lem3 to provide a slightly simpler definition later. (Contributed by NM, 31-May-2015)

Ref Expression
Hypotheses hdmap14lem1.h โŠข ๐ป = ( LHyp โ€˜ ๐พ )
hdmap14lem1.u โŠข ๐‘ˆ = ( ( DVecH โ€˜ ๐พ ) โ€˜ ๐‘Š )
hdmap14lem1.v โŠข ๐‘‰ = ( Base โ€˜ ๐‘ˆ )
hdmap14lem1.t โŠข ยท = ( ยท๐‘  โ€˜ ๐‘ˆ )
hdmap14lem3.o โŠข 0 = ( 0g โ€˜ ๐‘ˆ )
hdmap14lem1.r โŠข ๐‘… = ( Scalar โ€˜ ๐‘ˆ )
hdmap14lem1.b โŠข ๐ต = ( Base โ€˜ ๐‘… )
hdmap14lem1.z โŠข ๐‘ = ( 0g โ€˜ ๐‘… )
hdmap14lem1.c โŠข ๐ถ = ( ( LCDual โ€˜ ๐พ ) โ€˜ ๐‘Š )
hdmap14lem2.e โŠข โˆ™ = ( ยท๐‘  โ€˜ ๐ถ )
hdmap14lem1.l โŠข ๐ฟ = ( LSpan โ€˜ ๐ถ )
hdmap14lem2.p โŠข ๐‘ƒ = ( Scalar โ€˜ ๐ถ )
hdmap14lem2.a โŠข ๐ด = ( Base โ€˜ ๐‘ƒ )
hdmap14lem2.q โŠข ๐‘„ = ( 0g โ€˜ ๐‘ƒ )
hdmap14lem1.s โŠข ๐‘† = ( ( HDMap โ€˜ ๐พ ) โ€˜ ๐‘Š )
hdmap14lem1.k โŠข ( ๐œ‘ โ†’ ( ๐พ โˆˆ HL โˆง ๐‘Š โˆˆ ๐ป ) )
hdmap14lem3.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ( ๐‘‰ โˆ– { 0 } ) )
hdmap14lem1.f โŠข ( ๐œ‘ โ†’ ๐น โˆˆ ( ๐ต โˆ– { ๐‘ } ) )
Assertion hdmap14lem4a ( ๐œ‘ โ†’ ( โˆƒ! ๐‘” โˆˆ ( ๐ด โˆ– { ๐‘„ } ) ( ๐‘† โ€˜ ( ๐น ยท ๐‘‹ ) ) = ( ๐‘” โˆ™ ( ๐‘† โ€˜ ๐‘‹ ) ) โ†” โˆƒ! ๐‘” โˆˆ ๐ด ( ๐‘† โ€˜ ( ๐น ยท ๐‘‹ ) ) = ( ๐‘” โˆ™ ( ๐‘† โ€˜ ๐‘‹ ) ) ) )

Proof

Step Hyp Ref Expression
1 hdmap14lem1.h โŠข ๐ป = ( LHyp โ€˜ ๐พ )
2 hdmap14lem1.u โŠข ๐‘ˆ = ( ( DVecH โ€˜ ๐พ ) โ€˜ ๐‘Š )
3 hdmap14lem1.v โŠข ๐‘‰ = ( Base โ€˜ ๐‘ˆ )
4 hdmap14lem1.t โŠข ยท = ( ยท๐‘  โ€˜ ๐‘ˆ )
5 hdmap14lem3.o โŠข 0 = ( 0g โ€˜ ๐‘ˆ )
6 hdmap14lem1.r โŠข ๐‘… = ( Scalar โ€˜ ๐‘ˆ )
7 hdmap14lem1.b โŠข ๐ต = ( Base โ€˜ ๐‘… )
8 hdmap14lem1.z โŠข ๐‘ = ( 0g โ€˜ ๐‘… )
9 hdmap14lem1.c โŠข ๐ถ = ( ( LCDual โ€˜ ๐พ ) โ€˜ ๐‘Š )
10 hdmap14lem2.e โŠข โˆ™ = ( ยท๐‘  โ€˜ ๐ถ )
11 hdmap14lem1.l โŠข ๐ฟ = ( LSpan โ€˜ ๐ถ )
12 hdmap14lem2.p โŠข ๐‘ƒ = ( Scalar โ€˜ ๐ถ )
13 hdmap14lem2.a โŠข ๐ด = ( Base โ€˜ ๐‘ƒ )
14 hdmap14lem2.q โŠข ๐‘„ = ( 0g โ€˜ ๐‘ƒ )
15 hdmap14lem1.s โŠข ๐‘† = ( ( HDMap โ€˜ ๐พ ) โ€˜ ๐‘Š )
16 hdmap14lem1.k โŠข ( ๐œ‘ โ†’ ( ๐พ โˆˆ HL โˆง ๐‘Š โˆˆ ๐ป ) )
17 hdmap14lem3.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ( ๐‘‰ โˆ– { 0 } ) )
18 hdmap14lem1.f โŠข ( ๐œ‘ โ†’ ๐น โˆˆ ( ๐ต โˆ– { ๐‘ } ) )
19 eqid โŠข ( 0g โ€˜ ๐ถ ) = ( 0g โ€˜ ๐ถ )
20 eqid โŠข ( Base โ€˜ ๐ถ ) = ( Base โ€˜ ๐ถ )
21 1 2 16 dvhlmod โŠข ( ๐œ‘ โ†’ ๐‘ˆ โˆˆ LMod )
22 18 eldifad โŠข ( ๐œ‘ โ†’ ๐น โˆˆ ๐ต )
23 17 eldifad โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ๐‘‰ )
24 3 6 4 7 lmodvscl โŠข ( ( ๐‘ˆ โˆˆ LMod โˆง ๐น โˆˆ ๐ต โˆง ๐‘‹ โˆˆ ๐‘‰ ) โ†’ ( ๐น ยท ๐‘‹ ) โˆˆ ๐‘‰ )
25 21 22 23 24 syl3anc โŠข ( ๐œ‘ โ†’ ( ๐น ยท ๐‘‹ ) โˆˆ ๐‘‰ )
26 eldifsni โŠข ( ๐น โˆˆ ( ๐ต โˆ– { ๐‘ } ) โ†’ ๐น โ‰  ๐‘ )
27 18 26 syl โŠข ( ๐œ‘ โ†’ ๐น โ‰  ๐‘ )
28 eldifsni โŠข ( ๐‘‹ โˆˆ ( ๐‘‰ โˆ– { 0 } ) โ†’ ๐‘‹ โ‰  0 )
29 17 28 syl โŠข ( ๐œ‘ โ†’ ๐‘‹ โ‰  0 )
30 1 2 16 dvhlvec โŠข ( ๐œ‘ โ†’ ๐‘ˆ โˆˆ LVec )
31 3 4 6 7 8 5 30 22 23 lvecvsn0 โŠข ( ๐œ‘ โ†’ ( ( ๐น ยท ๐‘‹ ) โ‰  0 โ†” ( ๐น โ‰  ๐‘ โˆง ๐‘‹ โ‰  0 ) ) )
32 27 29 31 mpbir2and โŠข ( ๐œ‘ โ†’ ( ๐น ยท ๐‘‹ ) โ‰  0 )
33 eldifsn โŠข ( ( ๐น ยท ๐‘‹ ) โˆˆ ( ๐‘‰ โˆ– { 0 } ) โ†” ( ( ๐น ยท ๐‘‹ ) โˆˆ ๐‘‰ โˆง ( ๐น ยท ๐‘‹ ) โ‰  0 ) )
34 25 32 33 sylanbrc โŠข ( ๐œ‘ โ†’ ( ๐น ยท ๐‘‹ ) โˆˆ ( ๐‘‰ โˆ– { 0 } ) )
35 1 2 3 5 9 19 20 15 16 34 hdmapnzcl โŠข ( ๐œ‘ โ†’ ( ๐‘† โ€˜ ( ๐น ยท ๐‘‹ ) ) โˆˆ ( ( Base โ€˜ ๐ถ ) โˆ– { ( 0g โ€˜ ๐ถ ) } ) )
36 eldifsni โŠข ( ( ๐‘† โ€˜ ( ๐น ยท ๐‘‹ ) ) โˆˆ ( ( Base โ€˜ ๐ถ ) โˆ– { ( 0g โ€˜ ๐ถ ) } ) โ†’ ( ๐‘† โ€˜ ( ๐น ยท ๐‘‹ ) ) โ‰  ( 0g โ€˜ ๐ถ ) )
37 35 36 syl โŠข ( ๐œ‘ โ†’ ( ๐‘† โ€˜ ( ๐น ยท ๐‘‹ ) ) โ‰  ( 0g โ€˜ ๐ถ ) )
38 37 adantr โŠข ( ( ๐œ‘ โˆง ๐‘” โˆˆ { ๐‘„ } ) โ†’ ( ๐‘† โ€˜ ( ๐น ยท ๐‘‹ ) ) โ‰  ( 0g โ€˜ ๐ถ ) )
39 elsni โŠข ( ๐‘” โˆˆ { ๐‘„ } โ†’ ๐‘” = ๐‘„ )
40 39 oveq1d โŠข ( ๐‘” โˆˆ { ๐‘„ } โ†’ ( ๐‘” โˆ™ ( ๐‘† โ€˜ ๐‘‹ ) ) = ( ๐‘„ โˆ™ ( ๐‘† โ€˜ ๐‘‹ ) ) )
41 1 9 16 lcdlmod โŠข ( ๐œ‘ โ†’ ๐ถ โˆˆ LMod )
42 1 2 3 9 20 15 16 23 hdmapcl โŠข ( ๐œ‘ โ†’ ( ๐‘† โ€˜ ๐‘‹ ) โˆˆ ( Base โ€˜ ๐ถ ) )
43 20 12 10 14 19 lmod0vs โŠข ( ( ๐ถ โˆˆ LMod โˆง ( ๐‘† โ€˜ ๐‘‹ ) โˆˆ ( Base โ€˜ ๐ถ ) ) โ†’ ( ๐‘„ โˆ™ ( ๐‘† โ€˜ ๐‘‹ ) ) = ( 0g โ€˜ ๐ถ ) )
44 41 42 43 syl2anc โŠข ( ๐œ‘ โ†’ ( ๐‘„ โˆ™ ( ๐‘† โ€˜ ๐‘‹ ) ) = ( 0g โ€˜ ๐ถ ) )
45 40 44 sylan9eqr โŠข ( ( ๐œ‘ โˆง ๐‘” โˆˆ { ๐‘„ } ) โ†’ ( ๐‘” โˆ™ ( ๐‘† โ€˜ ๐‘‹ ) ) = ( 0g โ€˜ ๐ถ ) )
46 38 45 neeqtrrd โŠข ( ( ๐œ‘ โˆง ๐‘” โˆˆ { ๐‘„ } ) โ†’ ( ๐‘† โ€˜ ( ๐น ยท ๐‘‹ ) ) โ‰  ( ๐‘” โˆ™ ( ๐‘† โ€˜ ๐‘‹ ) ) )
47 46 neneqd โŠข ( ( ๐œ‘ โˆง ๐‘” โˆˆ { ๐‘„ } ) โ†’ ยฌ ( ๐‘† โ€˜ ( ๐น ยท ๐‘‹ ) ) = ( ๐‘” โˆ™ ( ๐‘† โ€˜ ๐‘‹ ) ) )
48 47 nrexdv โŠข ( ๐œ‘ โ†’ ยฌ โˆƒ ๐‘” โˆˆ { ๐‘„ } ( ๐‘† โ€˜ ( ๐น ยท ๐‘‹ ) ) = ( ๐‘” โˆ™ ( ๐‘† โ€˜ ๐‘‹ ) ) )
49 reuun2 โŠข ( ยฌ โˆƒ ๐‘” โˆˆ { ๐‘„ } ( ๐‘† โ€˜ ( ๐น ยท ๐‘‹ ) ) = ( ๐‘” โˆ™ ( ๐‘† โ€˜ ๐‘‹ ) ) โ†’ ( โˆƒ! ๐‘” โˆˆ ( ( ๐ด โˆ– { ๐‘„ } ) โˆช { ๐‘„ } ) ( ๐‘† โ€˜ ( ๐น ยท ๐‘‹ ) ) = ( ๐‘” โˆ™ ( ๐‘† โ€˜ ๐‘‹ ) ) โ†” โˆƒ! ๐‘” โˆˆ ( ๐ด โˆ– { ๐‘„ } ) ( ๐‘† โ€˜ ( ๐น ยท ๐‘‹ ) ) = ( ๐‘” โˆ™ ( ๐‘† โ€˜ ๐‘‹ ) ) ) )
50 48 49 syl โŠข ( ๐œ‘ โ†’ ( โˆƒ! ๐‘” โˆˆ ( ( ๐ด โˆ– { ๐‘„ } ) โˆช { ๐‘„ } ) ( ๐‘† โ€˜ ( ๐น ยท ๐‘‹ ) ) = ( ๐‘” โˆ™ ( ๐‘† โ€˜ ๐‘‹ ) ) โ†” โˆƒ! ๐‘” โˆˆ ( ๐ด โˆ– { ๐‘„ } ) ( ๐‘† โ€˜ ( ๐น ยท ๐‘‹ ) ) = ( ๐‘” โˆ™ ( ๐‘† โ€˜ ๐‘‹ ) ) ) )
51 12 13 14 lmod0cl โŠข ( ๐ถ โˆˆ LMod โ†’ ๐‘„ โˆˆ ๐ด )
52 difsnid โŠข ( ๐‘„ โˆˆ ๐ด โ†’ ( ( ๐ด โˆ– { ๐‘„ } ) โˆช { ๐‘„ } ) = ๐ด )
53 reueq1 โŠข ( ( ( ๐ด โˆ– { ๐‘„ } ) โˆช { ๐‘„ } ) = ๐ด โ†’ ( โˆƒ! ๐‘” โˆˆ ( ( ๐ด โˆ– { ๐‘„ } ) โˆช { ๐‘„ } ) ( ๐‘† โ€˜ ( ๐น ยท ๐‘‹ ) ) = ( ๐‘” โˆ™ ( ๐‘† โ€˜ ๐‘‹ ) ) โ†” โˆƒ! ๐‘” โˆˆ ๐ด ( ๐‘† โ€˜ ( ๐น ยท ๐‘‹ ) ) = ( ๐‘” โˆ™ ( ๐‘† โ€˜ ๐‘‹ ) ) ) )
54 41 51 52 53 4syl โŠข ( ๐œ‘ โ†’ ( โˆƒ! ๐‘” โˆˆ ( ( ๐ด โˆ– { ๐‘„ } ) โˆช { ๐‘„ } ) ( ๐‘† โ€˜ ( ๐น ยท ๐‘‹ ) ) = ( ๐‘” โˆ™ ( ๐‘† โ€˜ ๐‘‹ ) ) โ†” โˆƒ! ๐‘” โˆˆ ๐ด ( ๐‘† โ€˜ ( ๐น ยท ๐‘‹ ) ) = ( ๐‘” โˆ™ ( ๐‘† โ€˜ ๐‘‹ ) ) ) )
55 50 54 bitr3d โŠข ( ๐œ‘ โ†’ ( โˆƒ! ๐‘” โˆˆ ( ๐ด โˆ– { ๐‘„ } ) ( ๐‘† โ€˜ ( ๐น ยท ๐‘‹ ) ) = ( ๐‘” โˆ™ ( ๐‘† โ€˜ ๐‘‹ ) ) โ†” โˆƒ! ๐‘” โˆˆ ๐ด ( ๐‘† โ€˜ ( ๐น ยท ๐‘‹ ) ) = ( ๐‘” โˆ™ ( ๐‘† โ€˜ ๐‘‹ ) ) ) )