Metamath Proof Explorer


Theorem frlmlbs

Description: The unit vectors comprise a basis for a free module. (Contributed by Stefan O'Rear, 6-Feb-2015) (Proof shortened by AV, 21-Jul-2019)

Ref Expression
Hypotheses frlmlbs.f โŠข ๐น = ( ๐‘… freeLMod ๐ผ )
frlmlbs.u โŠข ๐‘ˆ = ( ๐‘… unitVec ๐ผ )
frlmlbs.j โŠข ๐ฝ = ( LBasis โ€˜ ๐น )
Assertion frlmlbs ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โ†’ ran ๐‘ˆ โˆˆ ๐ฝ )

Proof

Step Hyp Ref Expression
1 frlmlbs.f โŠข ๐น = ( ๐‘… freeLMod ๐ผ )
2 frlmlbs.u โŠข ๐‘ˆ = ( ๐‘… unitVec ๐ผ )
3 frlmlbs.j โŠข ๐ฝ = ( LBasis โ€˜ ๐น )
4 eqid โŠข ( Base โ€˜ ๐น ) = ( Base โ€˜ ๐น )
5 2 1 4 uvcff โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โ†’ ๐‘ˆ : ๐ผ โŸถ ( Base โ€˜ ๐น ) )
6 5 frnd โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โ†’ ran ๐‘ˆ โІ ( Base โ€˜ ๐น ) )
7 suppssdm โŠข ( ๐‘Ž supp ( 0g โ€˜ ๐‘… ) ) โІ dom ๐‘Ž
8 eqid โŠข ( Base โ€˜ ๐‘… ) = ( Base โ€˜ ๐‘… )
9 1 8 4 frlmbasf โŠข ( ( ๐ผ โˆˆ ๐‘‰ โˆง ๐‘Ž โˆˆ ( Base โ€˜ ๐น ) ) โ†’ ๐‘Ž : ๐ผ โŸถ ( Base โ€˜ ๐‘… ) )
10 9 adantll โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ๐‘Ž โˆˆ ( Base โ€˜ ๐น ) ) โ†’ ๐‘Ž : ๐ผ โŸถ ( Base โ€˜ ๐‘… ) )
11 7 10 fssdm โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ๐‘Ž โˆˆ ( Base โ€˜ ๐น ) ) โ†’ ( ๐‘Ž supp ( 0g โ€˜ ๐‘… ) ) โІ ๐ผ )
12 11 ralrimiva โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โ†’ โˆ€ ๐‘Ž โˆˆ ( Base โ€˜ ๐น ) ( ๐‘Ž supp ( 0g โ€˜ ๐‘… ) ) โІ ๐ผ )
13 rabid2 โŠข ( ( Base โ€˜ ๐น ) = { ๐‘Ž โˆˆ ( Base โ€˜ ๐น ) โˆฃ ( ๐‘Ž supp ( 0g โ€˜ ๐‘… ) ) โІ ๐ผ } โ†” โˆ€ ๐‘Ž โˆˆ ( Base โ€˜ ๐น ) ( ๐‘Ž supp ( 0g โ€˜ ๐‘… ) ) โІ ๐ผ )
14 12 13 sylibr โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โ†’ ( Base โ€˜ ๐น ) = { ๐‘Ž โˆˆ ( Base โ€˜ ๐น ) โˆฃ ( ๐‘Ž supp ( 0g โ€˜ ๐‘… ) ) โІ ๐ผ } )
15 ssid โŠข ๐ผ โІ ๐ผ
16 eqid โŠข ( LSpan โ€˜ ๐น ) = ( LSpan โ€˜ ๐น )
17 eqid โŠข ( 0g โ€˜ ๐‘… ) = ( 0g โ€˜ ๐‘… )
18 eqid โŠข { ๐‘Ž โˆˆ ( Base โ€˜ ๐น ) โˆฃ ( ๐‘Ž supp ( 0g โ€˜ ๐‘… ) ) โІ ๐ผ } = { ๐‘Ž โˆˆ ( Base โ€˜ ๐น ) โˆฃ ( ๐‘Ž supp ( 0g โ€˜ ๐‘… ) ) โІ ๐ผ }
19 1 2 16 4 17 18 frlmsslsp โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ โˆง ๐ผ โІ ๐ผ ) โ†’ ( ( LSpan โ€˜ ๐น ) โ€˜ ( ๐‘ˆ โ€œ ๐ผ ) ) = { ๐‘Ž โˆˆ ( Base โ€˜ ๐น ) โˆฃ ( ๐‘Ž supp ( 0g โ€˜ ๐‘… ) ) โІ ๐ผ } )
20 15 19 mp3an3 โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โ†’ ( ( LSpan โ€˜ ๐น ) โ€˜ ( ๐‘ˆ โ€œ ๐ผ ) ) = { ๐‘Ž โˆˆ ( Base โ€˜ ๐น ) โˆฃ ( ๐‘Ž supp ( 0g โ€˜ ๐‘… ) ) โІ ๐ผ } )
21 ffn โŠข ( ๐‘ˆ : ๐ผ โŸถ ( Base โ€˜ ๐น ) โ†’ ๐‘ˆ Fn ๐ผ )
22 fnima โŠข ( ๐‘ˆ Fn ๐ผ โ†’ ( ๐‘ˆ โ€œ ๐ผ ) = ran ๐‘ˆ )
23 5 21 22 3syl โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โ†’ ( ๐‘ˆ โ€œ ๐ผ ) = ran ๐‘ˆ )
24 23 fveq2d โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โ†’ ( ( LSpan โ€˜ ๐น ) โ€˜ ( ๐‘ˆ โ€œ ๐ผ ) ) = ( ( LSpan โ€˜ ๐น ) โ€˜ ran ๐‘ˆ ) )
25 14 20 24 3eqtr2rd โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โ†’ ( ( LSpan โ€˜ ๐น ) โ€˜ ran ๐‘ˆ ) = ( Base โ€˜ ๐น ) )
26 eqid โŠข ( ยท๐‘  โ€˜ ๐น ) = ( ยท๐‘  โ€˜ ๐น )
27 eqid โŠข { ๐‘Ž โˆˆ ( Base โ€˜ ๐น ) โˆฃ ( ๐‘Ž supp ( 0g โ€˜ ๐‘… ) ) โІ ( ๐ผ โˆ– { ๐‘ } ) } = { ๐‘Ž โˆˆ ( Base โ€˜ ๐น ) โˆฃ ( ๐‘Ž supp ( 0g โ€˜ ๐‘… ) ) โІ ( ๐ผ โˆ– { ๐‘ } ) }
28 simpll โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ ๐ผ โˆง ๐‘ โˆˆ ( ( Base โ€˜ ( Scalar โ€˜ ๐น ) ) โˆ– { ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) } ) ) ) โ†’ ๐‘… โˆˆ Ring )
29 simplr โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ ๐ผ โˆง ๐‘ โˆˆ ( ( Base โ€˜ ( Scalar โ€˜ ๐น ) ) โˆ– { ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) } ) ) ) โ†’ ๐ผ โˆˆ ๐‘‰ )
30 difssd โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ ๐ผ โˆง ๐‘ โˆˆ ( ( Base โ€˜ ( Scalar โ€˜ ๐น ) ) โˆ– { ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) } ) ) ) โ†’ ( ๐ผ โˆ– { ๐‘ } ) โІ ๐ผ )
31 vsnid โŠข ๐‘ โˆˆ { ๐‘ }
32 snssi โŠข ( ๐‘ โˆˆ ๐ผ โ†’ { ๐‘ } โІ ๐ผ )
33 32 ad2antrl โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ ๐ผ โˆง ๐‘ โˆˆ ( ( Base โ€˜ ( Scalar โ€˜ ๐น ) ) โˆ– { ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) } ) ) ) โ†’ { ๐‘ } โІ ๐ผ )
34 dfss4 โŠข ( { ๐‘ } โІ ๐ผ โ†” ( ๐ผ โˆ– ( ๐ผ โˆ– { ๐‘ } ) ) = { ๐‘ } )
35 33 34 sylib โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ ๐ผ โˆง ๐‘ โˆˆ ( ( Base โ€˜ ( Scalar โ€˜ ๐น ) ) โˆ– { ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) } ) ) ) โ†’ ( ๐ผ โˆ– ( ๐ผ โˆ– { ๐‘ } ) ) = { ๐‘ } )
36 31 35 eleqtrrid โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ ๐ผ โˆง ๐‘ โˆˆ ( ( Base โ€˜ ( Scalar โ€˜ ๐น ) ) โˆ– { ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) } ) ) ) โ†’ ๐‘ โˆˆ ( ๐ผ โˆ– ( ๐ผ โˆ– { ๐‘ } ) ) )
37 1 frlmsca โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โ†’ ๐‘… = ( Scalar โ€˜ ๐น ) )
38 37 fveq2d โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โ†’ ( Base โ€˜ ๐‘… ) = ( Base โ€˜ ( Scalar โ€˜ ๐น ) ) )
39 37 fveq2d โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โ†’ ( 0g โ€˜ ๐‘… ) = ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) )
40 39 sneqd โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โ†’ { ( 0g โ€˜ ๐‘… ) } = { ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) } )
41 38 40 difeq12d โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โ†’ ( ( Base โ€˜ ๐‘… ) โˆ– { ( 0g โ€˜ ๐‘… ) } ) = ( ( Base โ€˜ ( Scalar โ€˜ ๐น ) ) โˆ– { ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) } ) )
42 41 eleq2d โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โ†’ ( ๐‘ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– { ( 0g โ€˜ ๐‘… ) } ) โ†” ๐‘ โˆˆ ( ( Base โ€˜ ( Scalar โ€˜ ๐น ) ) โˆ– { ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) } ) ) )
43 42 biimpar โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ๐‘ โˆˆ ( ( Base โ€˜ ( Scalar โ€˜ ๐น ) ) โˆ– { ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) } ) ) โ†’ ๐‘ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– { ( 0g โ€˜ ๐‘… ) } ) )
44 43 adantrl โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ ๐ผ โˆง ๐‘ โˆˆ ( ( Base โ€˜ ( Scalar โ€˜ ๐น ) ) โˆ– { ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) } ) ) ) โ†’ ๐‘ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– { ( 0g โ€˜ ๐‘… ) } ) )
45 1 2 4 8 26 17 27 28 29 30 36 44 frlmssuvc2 โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ ๐ผ โˆง ๐‘ โˆˆ ( ( Base โ€˜ ( Scalar โ€˜ ๐น ) ) โˆ– { ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) } ) ) ) โ†’ ยฌ ( ๐‘ ( ยท๐‘  โ€˜ ๐น ) ( ๐‘ˆ โ€˜ ๐‘ ) ) โˆˆ { ๐‘Ž โˆˆ ( Base โ€˜ ๐น ) โˆฃ ( ๐‘Ž supp ( 0g โ€˜ ๐‘… ) ) โІ ( ๐ผ โˆ– { ๐‘ } ) } )
46 17 8 ringelnzr โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘ โˆˆ ( ( Base โ€˜ ๐‘… ) โˆ– { ( 0g โ€˜ ๐‘… ) } ) ) โ†’ ๐‘… โˆˆ NzRing )
47 28 44 46 syl2anc โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ ๐ผ โˆง ๐‘ โˆˆ ( ( Base โ€˜ ( Scalar โ€˜ ๐น ) ) โˆ– { ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) } ) ) ) โ†’ ๐‘… โˆˆ NzRing )
48 2 1 4 uvcf1 โŠข ( ( ๐‘… โˆˆ NzRing โˆง ๐ผ โˆˆ ๐‘‰ ) โ†’ ๐‘ˆ : ๐ผ โ€“1-1โ†’ ( Base โ€˜ ๐น ) )
49 47 29 48 syl2anc โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ ๐ผ โˆง ๐‘ โˆˆ ( ( Base โ€˜ ( Scalar โ€˜ ๐น ) ) โˆ– { ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) } ) ) ) โ†’ ๐‘ˆ : ๐ผ โ€“1-1โ†’ ( Base โ€˜ ๐น ) )
50 df-f1 โŠข ( ๐‘ˆ : ๐ผ โ€“1-1โ†’ ( Base โ€˜ ๐น ) โ†” ( ๐‘ˆ : ๐ผ โŸถ ( Base โ€˜ ๐น ) โˆง Fun โ—ก ๐‘ˆ ) )
51 50 simprbi โŠข ( ๐‘ˆ : ๐ผ โ€“1-1โ†’ ( Base โ€˜ ๐น ) โ†’ Fun โ—ก ๐‘ˆ )
52 imadif โŠข ( Fun โ—ก ๐‘ˆ โ†’ ( ๐‘ˆ โ€œ ( ๐ผ โˆ– { ๐‘ } ) ) = ( ( ๐‘ˆ โ€œ ๐ผ ) โˆ– ( ๐‘ˆ โ€œ { ๐‘ } ) ) )
53 49 51 52 3syl โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ ๐ผ โˆง ๐‘ โˆˆ ( ( Base โ€˜ ( Scalar โ€˜ ๐น ) ) โˆ– { ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) } ) ) ) โ†’ ( ๐‘ˆ โ€œ ( ๐ผ โˆ– { ๐‘ } ) ) = ( ( ๐‘ˆ โ€œ ๐ผ ) โˆ– ( ๐‘ˆ โ€œ { ๐‘ } ) ) )
54 f1fn โŠข ( ๐‘ˆ : ๐ผ โ€“1-1โ†’ ( Base โ€˜ ๐น ) โ†’ ๐‘ˆ Fn ๐ผ )
55 49 54 22 3syl โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ ๐ผ โˆง ๐‘ โˆˆ ( ( Base โ€˜ ( Scalar โ€˜ ๐น ) ) โˆ– { ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) } ) ) ) โ†’ ( ๐‘ˆ โ€œ ๐ผ ) = ran ๐‘ˆ )
56 49 54 syl โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ ๐ผ โˆง ๐‘ โˆˆ ( ( Base โ€˜ ( Scalar โ€˜ ๐น ) ) โˆ– { ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) } ) ) ) โ†’ ๐‘ˆ Fn ๐ผ )
57 simprl โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ ๐ผ โˆง ๐‘ โˆˆ ( ( Base โ€˜ ( Scalar โ€˜ ๐น ) ) โˆ– { ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) } ) ) ) โ†’ ๐‘ โˆˆ ๐ผ )
58 fnsnfv โŠข ( ( ๐‘ˆ Fn ๐ผ โˆง ๐‘ โˆˆ ๐ผ ) โ†’ { ( ๐‘ˆ โ€˜ ๐‘ ) } = ( ๐‘ˆ โ€œ { ๐‘ } ) )
59 56 57 58 syl2anc โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ ๐ผ โˆง ๐‘ โˆˆ ( ( Base โ€˜ ( Scalar โ€˜ ๐น ) ) โˆ– { ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) } ) ) ) โ†’ { ( ๐‘ˆ โ€˜ ๐‘ ) } = ( ๐‘ˆ โ€œ { ๐‘ } ) )
60 59 eqcomd โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ ๐ผ โˆง ๐‘ โˆˆ ( ( Base โ€˜ ( Scalar โ€˜ ๐น ) ) โˆ– { ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) } ) ) ) โ†’ ( ๐‘ˆ โ€œ { ๐‘ } ) = { ( ๐‘ˆ โ€˜ ๐‘ ) } )
61 55 60 difeq12d โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ ๐ผ โˆง ๐‘ โˆˆ ( ( Base โ€˜ ( Scalar โ€˜ ๐น ) ) โˆ– { ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) } ) ) ) โ†’ ( ( ๐‘ˆ โ€œ ๐ผ ) โˆ– ( ๐‘ˆ โ€œ { ๐‘ } ) ) = ( ran ๐‘ˆ โˆ– { ( ๐‘ˆ โ€˜ ๐‘ ) } ) )
62 53 61 eqtr2d โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ ๐ผ โˆง ๐‘ โˆˆ ( ( Base โ€˜ ( Scalar โ€˜ ๐น ) ) โˆ– { ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) } ) ) ) โ†’ ( ran ๐‘ˆ โˆ– { ( ๐‘ˆ โ€˜ ๐‘ ) } ) = ( ๐‘ˆ โ€œ ( ๐ผ โˆ– { ๐‘ } ) ) )
63 62 fveq2d โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ ๐ผ โˆง ๐‘ โˆˆ ( ( Base โ€˜ ( Scalar โ€˜ ๐น ) ) โˆ– { ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) } ) ) ) โ†’ ( ( LSpan โ€˜ ๐น ) โ€˜ ( ran ๐‘ˆ โˆ– { ( ๐‘ˆ โ€˜ ๐‘ ) } ) ) = ( ( LSpan โ€˜ ๐น ) โ€˜ ( ๐‘ˆ โ€œ ( ๐ผ โˆ– { ๐‘ } ) ) ) )
64 1 2 16 4 17 27 frlmsslsp โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ โˆง ( ๐ผ โˆ– { ๐‘ } ) โІ ๐ผ ) โ†’ ( ( LSpan โ€˜ ๐น ) โ€˜ ( ๐‘ˆ โ€œ ( ๐ผ โˆ– { ๐‘ } ) ) ) = { ๐‘Ž โˆˆ ( Base โ€˜ ๐น ) โˆฃ ( ๐‘Ž supp ( 0g โ€˜ ๐‘… ) ) โІ ( ๐ผ โˆ– { ๐‘ } ) } )
65 28 29 30 64 syl3anc โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ ๐ผ โˆง ๐‘ โˆˆ ( ( Base โ€˜ ( Scalar โ€˜ ๐น ) ) โˆ– { ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) } ) ) ) โ†’ ( ( LSpan โ€˜ ๐น ) โ€˜ ( ๐‘ˆ โ€œ ( ๐ผ โˆ– { ๐‘ } ) ) ) = { ๐‘Ž โˆˆ ( Base โ€˜ ๐น ) โˆฃ ( ๐‘Ž supp ( 0g โ€˜ ๐‘… ) ) โІ ( ๐ผ โˆ– { ๐‘ } ) } )
66 63 65 eqtrd โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ ๐ผ โˆง ๐‘ โˆˆ ( ( Base โ€˜ ( Scalar โ€˜ ๐น ) ) โˆ– { ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) } ) ) ) โ†’ ( ( LSpan โ€˜ ๐น ) โ€˜ ( ran ๐‘ˆ โˆ– { ( ๐‘ˆ โ€˜ ๐‘ ) } ) ) = { ๐‘Ž โˆˆ ( Base โ€˜ ๐น ) โˆฃ ( ๐‘Ž supp ( 0g โ€˜ ๐‘… ) ) โІ ( ๐ผ โˆ– { ๐‘ } ) } )
67 45 66 neleqtrrd โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โˆง ( ๐‘ โˆˆ ๐ผ โˆง ๐‘ โˆˆ ( ( Base โ€˜ ( Scalar โ€˜ ๐น ) ) โˆ– { ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) } ) ) ) โ†’ ยฌ ( ๐‘ ( ยท๐‘  โ€˜ ๐น ) ( ๐‘ˆ โ€˜ ๐‘ ) ) โˆˆ ( ( LSpan โ€˜ ๐น ) โ€˜ ( ran ๐‘ˆ โˆ– { ( ๐‘ˆ โ€˜ ๐‘ ) } ) ) )
68 67 ralrimivva โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โ†’ โˆ€ ๐‘ โˆˆ ๐ผ โˆ€ ๐‘ โˆˆ ( ( Base โ€˜ ( Scalar โ€˜ ๐น ) ) โˆ– { ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) } ) ยฌ ( ๐‘ ( ยท๐‘  โ€˜ ๐น ) ( ๐‘ˆ โ€˜ ๐‘ ) ) โˆˆ ( ( LSpan โ€˜ ๐น ) โ€˜ ( ran ๐‘ˆ โˆ– { ( ๐‘ˆ โ€˜ ๐‘ ) } ) ) )
69 oveq2 โŠข ( ๐‘Ž = ( ๐‘ˆ โ€˜ ๐‘ ) โ†’ ( ๐‘ ( ยท๐‘  โ€˜ ๐น ) ๐‘Ž ) = ( ๐‘ ( ยท๐‘  โ€˜ ๐น ) ( ๐‘ˆ โ€˜ ๐‘ ) ) )
70 sneq โŠข ( ๐‘Ž = ( ๐‘ˆ โ€˜ ๐‘ ) โ†’ { ๐‘Ž } = { ( ๐‘ˆ โ€˜ ๐‘ ) } )
71 70 difeq2d โŠข ( ๐‘Ž = ( ๐‘ˆ โ€˜ ๐‘ ) โ†’ ( ran ๐‘ˆ โˆ– { ๐‘Ž } ) = ( ran ๐‘ˆ โˆ– { ( ๐‘ˆ โ€˜ ๐‘ ) } ) )
72 71 fveq2d โŠข ( ๐‘Ž = ( ๐‘ˆ โ€˜ ๐‘ ) โ†’ ( ( LSpan โ€˜ ๐น ) โ€˜ ( ran ๐‘ˆ โˆ– { ๐‘Ž } ) ) = ( ( LSpan โ€˜ ๐น ) โ€˜ ( ran ๐‘ˆ โˆ– { ( ๐‘ˆ โ€˜ ๐‘ ) } ) ) )
73 69 72 eleq12d โŠข ( ๐‘Ž = ( ๐‘ˆ โ€˜ ๐‘ ) โ†’ ( ( ๐‘ ( ยท๐‘  โ€˜ ๐น ) ๐‘Ž ) โˆˆ ( ( LSpan โ€˜ ๐น ) โ€˜ ( ran ๐‘ˆ โˆ– { ๐‘Ž } ) ) โ†” ( ๐‘ ( ยท๐‘  โ€˜ ๐น ) ( ๐‘ˆ โ€˜ ๐‘ ) ) โˆˆ ( ( LSpan โ€˜ ๐น ) โ€˜ ( ran ๐‘ˆ โˆ– { ( ๐‘ˆ โ€˜ ๐‘ ) } ) ) ) )
74 73 notbid โŠข ( ๐‘Ž = ( ๐‘ˆ โ€˜ ๐‘ ) โ†’ ( ยฌ ( ๐‘ ( ยท๐‘  โ€˜ ๐น ) ๐‘Ž ) โˆˆ ( ( LSpan โ€˜ ๐น ) โ€˜ ( ran ๐‘ˆ โˆ– { ๐‘Ž } ) ) โ†” ยฌ ( ๐‘ ( ยท๐‘  โ€˜ ๐น ) ( ๐‘ˆ โ€˜ ๐‘ ) ) โˆˆ ( ( LSpan โ€˜ ๐น ) โ€˜ ( ran ๐‘ˆ โˆ– { ( ๐‘ˆ โ€˜ ๐‘ ) } ) ) ) )
75 74 ralbidv โŠข ( ๐‘Ž = ( ๐‘ˆ โ€˜ ๐‘ ) โ†’ ( โˆ€ ๐‘ โˆˆ ( ( Base โ€˜ ( Scalar โ€˜ ๐น ) ) โˆ– { ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) } ) ยฌ ( ๐‘ ( ยท๐‘  โ€˜ ๐น ) ๐‘Ž ) โˆˆ ( ( LSpan โ€˜ ๐น ) โ€˜ ( ran ๐‘ˆ โˆ– { ๐‘Ž } ) ) โ†” โˆ€ ๐‘ โˆˆ ( ( Base โ€˜ ( Scalar โ€˜ ๐น ) ) โˆ– { ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) } ) ยฌ ( ๐‘ ( ยท๐‘  โ€˜ ๐น ) ( ๐‘ˆ โ€˜ ๐‘ ) ) โˆˆ ( ( LSpan โ€˜ ๐น ) โ€˜ ( ran ๐‘ˆ โˆ– { ( ๐‘ˆ โ€˜ ๐‘ ) } ) ) ) )
76 75 ralrn โŠข ( ๐‘ˆ Fn ๐ผ โ†’ ( โˆ€ ๐‘Ž โˆˆ ran ๐‘ˆ โˆ€ ๐‘ โˆˆ ( ( Base โ€˜ ( Scalar โ€˜ ๐น ) ) โˆ– { ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) } ) ยฌ ( ๐‘ ( ยท๐‘  โ€˜ ๐น ) ๐‘Ž ) โˆˆ ( ( LSpan โ€˜ ๐น ) โ€˜ ( ran ๐‘ˆ โˆ– { ๐‘Ž } ) ) โ†” โˆ€ ๐‘ โˆˆ ๐ผ โˆ€ ๐‘ โˆˆ ( ( Base โ€˜ ( Scalar โ€˜ ๐น ) ) โˆ– { ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) } ) ยฌ ( ๐‘ ( ยท๐‘  โ€˜ ๐น ) ( ๐‘ˆ โ€˜ ๐‘ ) ) โˆˆ ( ( LSpan โ€˜ ๐น ) โ€˜ ( ran ๐‘ˆ โˆ– { ( ๐‘ˆ โ€˜ ๐‘ ) } ) ) ) )
77 5 21 76 3syl โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โ†’ ( โˆ€ ๐‘Ž โˆˆ ran ๐‘ˆ โˆ€ ๐‘ โˆˆ ( ( Base โ€˜ ( Scalar โ€˜ ๐น ) ) โˆ– { ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) } ) ยฌ ( ๐‘ ( ยท๐‘  โ€˜ ๐น ) ๐‘Ž ) โˆˆ ( ( LSpan โ€˜ ๐น ) โ€˜ ( ran ๐‘ˆ โˆ– { ๐‘Ž } ) ) โ†” โˆ€ ๐‘ โˆˆ ๐ผ โˆ€ ๐‘ โˆˆ ( ( Base โ€˜ ( Scalar โ€˜ ๐น ) ) โˆ– { ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) } ) ยฌ ( ๐‘ ( ยท๐‘  โ€˜ ๐น ) ( ๐‘ˆ โ€˜ ๐‘ ) ) โˆˆ ( ( LSpan โ€˜ ๐น ) โ€˜ ( ran ๐‘ˆ โˆ– { ( ๐‘ˆ โ€˜ ๐‘ ) } ) ) ) )
78 68 77 mpbird โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โ†’ โˆ€ ๐‘Ž โˆˆ ran ๐‘ˆ โˆ€ ๐‘ โˆˆ ( ( Base โ€˜ ( Scalar โ€˜ ๐น ) ) โˆ– { ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) } ) ยฌ ( ๐‘ ( ยท๐‘  โ€˜ ๐น ) ๐‘Ž ) โˆˆ ( ( LSpan โ€˜ ๐น ) โ€˜ ( ran ๐‘ˆ โˆ– { ๐‘Ž } ) ) )
79 1 ovexi โŠข ๐น โˆˆ V
80 eqid โŠข ( Scalar โ€˜ ๐น ) = ( Scalar โ€˜ ๐น )
81 eqid โŠข ( Base โ€˜ ( Scalar โ€˜ ๐น ) ) = ( Base โ€˜ ( Scalar โ€˜ ๐น ) )
82 eqid โŠข ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) = ( 0g โ€˜ ( Scalar โ€˜ ๐น ) )
83 4 80 26 81 3 16 82 islbs โŠข ( ๐น โˆˆ V โ†’ ( ran ๐‘ˆ โˆˆ ๐ฝ โ†” ( ran ๐‘ˆ โІ ( Base โ€˜ ๐น ) โˆง ( ( LSpan โ€˜ ๐น ) โ€˜ ran ๐‘ˆ ) = ( Base โ€˜ ๐น ) โˆง โˆ€ ๐‘Ž โˆˆ ran ๐‘ˆ โˆ€ ๐‘ โˆˆ ( ( Base โ€˜ ( Scalar โ€˜ ๐น ) ) โˆ– { ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) } ) ยฌ ( ๐‘ ( ยท๐‘  โ€˜ ๐น ) ๐‘Ž ) โˆˆ ( ( LSpan โ€˜ ๐น ) โ€˜ ( ran ๐‘ˆ โˆ– { ๐‘Ž } ) ) ) ) )
84 79 83 ax-mp โŠข ( ran ๐‘ˆ โˆˆ ๐ฝ โ†” ( ran ๐‘ˆ โІ ( Base โ€˜ ๐น ) โˆง ( ( LSpan โ€˜ ๐น ) โ€˜ ran ๐‘ˆ ) = ( Base โ€˜ ๐น ) โˆง โˆ€ ๐‘Ž โˆˆ ran ๐‘ˆ โˆ€ ๐‘ โˆˆ ( ( Base โ€˜ ( Scalar โ€˜ ๐น ) ) โˆ– { ( 0g โ€˜ ( Scalar โ€˜ ๐น ) ) } ) ยฌ ( ๐‘ ( ยท๐‘  โ€˜ ๐น ) ๐‘Ž ) โˆˆ ( ( LSpan โ€˜ ๐น ) โ€˜ ( ran ๐‘ˆ โˆ– { ๐‘Ž } ) ) ) )
85 6 25 78 84 syl3anbrc โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐‘‰ ) โ†’ ran ๐‘ˆ โˆˆ ๐ฝ )