Metamath Proof Explorer


Theorem islbs

Description: The predicate " B is a basis for the left module or vector space W ". A subset of the base set is a basis if zero is not in the set, it spans the set, and no nonzero multiple of an element of the basis is in the span of the rest of the family. (Contributed by Mario Carneiro, 24-Jun-2014) (Revised by Mario Carneiro, 14-Jan-2015)

Ref Expression
Hypotheses islbs.v โŠข ๐‘‰ = ( Base โ€˜ ๐‘Š )
islbs.f โŠข ๐น = ( Scalar โ€˜ ๐‘Š )
islbs.s โŠข ยท = ( ยท๐‘  โ€˜ ๐‘Š )
islbs.k โŠข ๐พ = ( Base โ€˜ ๐น )
islbs.j โŠข ๐ฝ = ( LBasis โ€˜ ๐‘Š )
islbs.n โŠข ๐‘ = ( LSpan โ€˜ ๐‘Š )
islbs.z โŠข 0 = ( 0g โ€˜ ๐น )
Assertion islbs ( ๐‘Š โˆˆ ๐‘‹ โ†’ ( ๐ต โˆˆ ๐ฝ โ†” ( ๐ต โŠ† ๐‘‰ โˆง ( ๐‘ โ€˜ ๐ต ) = ๐‘‰ โˆง โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ( ๐พ โˆ– { 0 } ) ยฌ ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ( ๐‘ โ€˜ ( ๐ต โˆ– { ๐‘ฅ } ) ) ) ) )

Proof

Step Hyp Ref Expression
1 islbs.v โŠข ๐‘‰ = ( Base โ€˜ ๐‘Š )
2 islbs.f โŠข ๐น = ( Scalar โ€˜ ๐‘Š )
3 islbs.s โŠข ยท = ( ยท๐‘  โ€˜ ๐‘Š )
4 islbs.k โŠข ๐พ = ( Base โ€˜ ๐น )
5 islbs.j โŠข ๐ฝ = ( LBasis โ€˜ ๐‘Š )
6 islbs.n โŠข ๐‘ = ( LSpan โ€˜ ๐‘Š )
7 islbs.z โŠข 0 = ( 0g โ€˜ ๐น )
8 elex โŠข ( ๐‘Š โˆˆ ๐‘‹ โ†’ ๐‘Š โˆˆ V )
9 fveq2 โŠข ( ๐‘ค = ๐‘Š โ†’ ( Base โ€˜ ๐‘ค ) = ( Base โ€˜ ๐‘Š ) )
10 9 1 eqtr4di โŠข ( ๐‘ค = ๐‘Š โ†’ ( Base โ€˜ ๐‘ค ) = ๐‘‰ )
11 10 pweqd โŠข ( ๐‘ค = ๐‘Š โ†’ ๐’ซ ( Base โ€˜ ๐‘ค ) = ๐’ซ ๐‘‰ )
12 fvexd โŠข ( ๐‘ค = ๐‘Š โ†’ ( LSpan โ€˜ ๐‘ค ) โˆˆ V )
13 fveq2 โŠข ( ๐‘ค = ๐‘Š โ†’ ( LSpan โ€˜ ๐‘ค ) = ( LSpan โ€˜ ๐‘Š ) )
14 13 6 eqtr4di โŠข ( ๐‘ค = ๐‘Š โ†’ ( LSpan โ€˜ ๐‘ค ) = ๐‘ )
15 fvexd โŠข ( ( ๐‘ค = ๐‘Š โˆง ๐‘› = ๐‘ ) โ†’ ( Scalar โ€˜ ๐‘ค ) โˆˆ V )
16 fveq2 โŠข ( ๐‘ค = ๐‘Š โ†’ ( Scalar โ€˜ ๐‘ค ) = ( Scalar โ€˜ ๐‘Š ) )
17 16 adantr โŠข ( ( ๐‘ค = ๐‘Š โˆง ๐‘› = ๐‘ ) โ†’ ( Scalar โ€˜ ๐‘ค ) = ( Scalar โ€˜ ๐‘Š ) )
18 17 2 eqtr4di โŠข ( ( ๐‘ค = ๐‘Š โˆง ๐‘› = ๐‘ ) โ†’ ( Scalar โ€˜ ๐‘ค ) = ๐น )
19 simplr โŠข ( ( ( ๐‘ค = ๐‘Š โˆง ๐‘› = ๐‘ ) โˆง ๐‘“ = ๐น ) โ†’ ๐‘› = ๐‘ )
20 19 fveq1d โŠข ( ( ( ๐‘ค = ๐‘Š โˆง ๐‘› = ๐‘ ) โˆง ๐‘“ = ๐น ) โ†’ ( ๐‘› โ€˜ ๐‘ ) = ( ๐‘ โ€˜ ๐‘ ) )
21 10 ad2antrr โŠข ( ( ( ๐‘ค = ๐‘Š โˆง ๐‘› = ๐‘ ) โˆง ๐‘“ = ๐น ) โ†’ ( Base โ€˜ ๐‘ค ) = ๐‘‰ )
22 20 21 eqeq12d โŠข ( ( ( ๐‘ค = ๐‘Š โˆง ๐‘› = ๐‘ ) โˆง ๐‘“ = ๐น ) โ†’ ( ( ๐‘› โ€˜ ๐‘ ) = ( Base โ€˜ ๐‘ค ) โ†” ( ๐‘ โ€˜ ๐‘ ) = ๐‘‰ ) )
23 simpr โŠข ( ( ( ๐‘ค = ๐‘Š โˆง ๐‘› = ๐‘ ) โˆง ๐‘“ = ๐น ) โ†’ ๐‘“ = ๐น )
24 23 fveq2d โŠข ( ( ( ๐‘ค = ๐‘Š โˆง ๐‘› = ๐‘ ) โˆง ๐‘“ = ๐น ) โ†’ ( Base โ€˜ ๐‘“ ) = ( Base โ€˜ ๐น ) )
25 24 4 eqtr4di โŠข ( ( ( ๐‘ค = ๐‘Š โˆง ๐‘› = ๐‘ ) โˆง ๐‘“ = ๐น ) โ†’ ( Base โ€˜ ๐‘“ ) = ๐พ )
26 23 fveq2d โŠข ( ( ( ๐‘ค = ๐‘Š โˆง ๐‘› = ๐‘ ) โˆง ๐‘“ = ๐น ) โ†’ ( 0g โ€˜ ๐‘“ ) = ( 0g โ€˜ ๐น ) )
27 26 7 eqtr4di โŠข ( ( ( ๐‘ค = ๐‘Š โˆง ๐‘› = ๐‘ ) โˆง ๐‘“ = ๐น ) โ†’ ( 0g โ€˜ ๐‘“ ) = 0 )
28 27 sneqd โŠข ( ( ( ๐‘ค = ๐‘Š โˆง ๐‘› = ๐‘ ) โˆง ๐‘“ = ๐น ) โ†’ { ( 0g โ€˜ ๐‘“ ) } = { 0 } )
29 25 28 difeq12d โŠข ( ( ( ๐‘ค = ๐‘Š โˆง ๐‘› = ๐‘ ) โˆง ๐‘“ = ๐น ) โ†’ ( ( Base โ€˜ ๐‘“ ) โˆ– { ( 0g โ€˜ ๐‘“ ) } ) = ( ๐พ โˆ– { 0 } ) )
30 fveq2 โŠข ( ๐‘ค = ๐‘Š โ†’ ( ยท๐‘  โ€˜ ๐‘ค ) = ( ยท๐‘  โ€˜ ๐‘Š ) )
31 30 3 eqtr4di โŠข ( ๐‘ค = ๐‘Š โ†’ ( ยท๐‘  โ€˜ ๐‘ค ) = ยท )
32 31 ad2antrr โŠข ( ( ( ๐‘ค = ๐‘Š โˆง ๐‘› = ๐‘ ) โˆง ๐‘“ = ๐น ) โ†’ ( ยท๐‘  โ€˜ ๐‘ค ) = ยท )
33 32 oveqd โŠข ( ( ( ๐‘ค = ๐‘Š โˆง ๐‘› = ๐‘ ) โˆง ๐‘“ = ๐น ) โ†’ ( ๐‘ฆ ( ยท๐‘  โ€˜ ๐‘ค ) ๐‘ฅ ) = ( ๐‘ฆ ยท ๐‘ฅ ) )
34 19 fveq1d โŠข ( ( ( ๐‘ค = ๐‘Š โˆง ๐‘› = ๐‘ ) โˆง ๐‘“ = ๐น ) โ†’ ( ๐‘› โ€˜ ( ๐‘ โˆ– { ๐‘ฅ } ) ) = ( ๐‘ โ€˜ ( ๐‘ โˆ– { ๐‘ฅ } ) ) )
35 33 34 eleq12d โŠข ( ( ( ๐‘ค = ๐‘Š โˆง ๐‘› = ๐‘ ) โˆง ๐‘“ = ๐น ) โ†’ ( ( ๐‘ฆ ( ยท๐‘  โ€˜ ๐‘ค ) ๐‘ฅ ) โˆˆ ( ๐‘› โ€˜ ( ๐‘ โˆ– { ๐‘ฅ } ) ) โ†” ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ( ๐‘ โ€˜ ( ๐‘ โˆ– { ๐‘ฅ } ) ) ) )
36 35 notbid โŠข ( ( ( ๐‘ค = ๐‘Š โˆง ๐‘› = ๐‘ ) โˆง ๐‘“ = ๐น ) โ†’ ( ยฌ ( ๐‘ฆ ( ยท๐‘  โ€˜ ๐‘ค ) ๐‘ฅ ) โˆˆ ( ๐‘› โ€˜ ( ๐‘ โˆ– { ๐‘ฅ } ) ) โ†” ยฌ ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ( ๐‘ โ€˜ ( ๐‘ โˆ– { ๐‘ฅ } ) ) ) )
37 29 36 raleqbidv โŠข ( ( ( ๐‘ค = ๐‘Š โˆง ๐‘› = ๐‘ ) โˆง ๐‘“ = ๐น ) โ†’ ( โˆ€ ๐‘ฆ โˆˆ ( ( Base โ€˜ ๐‘“ ) โˆ– { ( 0g โ€˜ ๐‘“ ) } ) ยฌ ( ๐‘ฆ ( ยท๐‘  โ€˜ ๐‘ค ) ๐‘ฅ ) โˆˆ ( ๐‘› โ€˜ ( ๐‘ โˆ– { ๐‘ฅ } ) ) โ†” โˆ€ ๐‘ฆ โˆˆ ( ๐พ โˆ– { 0 } ) ยฌ ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ( ๐‘ โ€˜ ( ๐‘ โˆ– { ๐‘ฅ } ) ) ) )
38 37 ralbidv โŠข ( ( ( ๐‘ค = ๐‘Š โˆง ๐‘› = ๐‘ ) โˆง ๐‘“ = ๐น ) โ†’ ( โˆ€ ๐‘ฅ โˆˆ ๐‘ โˆ€ ๐‘ฆ โˆˆ ( ( Base โ€˜ ๐‘“ ) โˆ– { ( 0g โ€˜ ๐‘“ ) } ) ยฌ ( ๐‘ฆ ( ยท๐‘  โ€˜ ๐‘ค ) ๐‘ฅ ) โˆˆ ( ๐‘› โ€˜ ( ๐‘ โˆ– { ๐‘ฅ } ) ) โ†” โˆ€ ๐‘ฅ โˆˆ ๐‘ โˆ€ ๐‘ฆ โˆˆ ( ๐พ โˆ– { 0 } ) ยฌ ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ( ๐‘ โ€˜ ( ๐‘ โˆ– { ๐‘ฅ } ) ) ) )
39 22 38 anbi12d โŠข ( ( ( ๐‘ค = ๐‘Š โˆง ๐‘› = ๐‘ ) โˆง ๐‘“ = ๐น ) โ†’ ( ( ( ๐‘› โ€˜ ๐‘ ) = ( Base โ€˜ ๐‘ค ) โˆง โˆ€ ๐‘ฅ โˆˆ ๐‘ โˆ€ ๐‘ฆ โˆˆ ( ( Base โ€˜ ๐‘“ ) โˆ– { ( 0g โ€˜ ๐‘“ ) } ) ยฌ ( ๐‘ฆ ( ยท๐‘  โ€˜ ๐‘ค ) ๐‘ฅ ) โˆˆ ( ๐‘› โ€˜ ( ๐‘ โˆ– { ๐‘ฅ } ) ) ) โ†” ( ( ๐‘ โ€˜ ๐‘ ) = ๐‘‰ โˆง โˆ€ ๐‘ฅ โˆˆ ๐‘ โˆ€ ๐‘ฆ โˆˆ ( ๐พ โˆ– { 0 } ) ยฌ ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ( ๐‘ โ€˜ ( ๐‘ โˆ– { ๐‘ฅ } ) ) ) ) )
40 15 18 39 sbcied2 โŠข ( ( ๐‘ค = ๐‘Š โˆง ๐‘› = ๐‘ ) โ†’ ( [ ( Scalar โ€˜ ๐‘ค ) / ๐‘“ ] ( ( ๐‘› โ€˜ ๐‘ ) = ( Base โ€˜ ๐‘ค ) โˆง โˆ€ ๐‘ฅ โˆˆ ๐‘ โˆ€ ๐‘ฆ โˆˆ ( ( Base โ€˜ ๐‘“ ) โˆ– { ( 0g โ€˜ ๐‘“ ) } ) ยฌ ( ๐‘ฆ ( ยท๐‘  โ€˜ ๐‘ค ) ๐‘ฅ ) โˆˆ ( ๐‘› โ€˜ ( ๐‘ โˆ– { ๐‘ฅ } ) ) ) โ†” ( ( ๐‘ โ€˜ ๐‘ ) = ๐‘‰ โˆง โˆ€ ๐‘ฅ โˆˆ ๐‘ โˆ€ ๐‘ฆ โˆˆ ( ๐พ โˆ– { 0 } ) ยฌ ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ( ๐‘ โ€˜ ( ๐‘ โˆ– { ๐‘ฅ } ) ) ) ) )
41 12 14 40 sbcied2 โŠข ( ๐‘ค = ๐‘Š โ†’ ( [ ( LSpan โ€˜ ๐‘ค ) / ๐‘› ] [ ( Scalar โ€˜ ๐‘ค ) / ๐‘“ ] ( ( ๐‘› โ€˜ ๐‘ ) = ( Base โ€˜ ๐‘ค ) โˆง โˆ€ ๐‘ฅ โˆˆ ๐‘ โˆ€ ๐‘ฆ โˆˆ ( ( Base โ€˜ ๐‘“ ) โˆ– { ( 0g โ€˜ ๐‘“ ) } ) ยฌ ( ๐‘ฆ ( ยท๐‘  โ€˜ ๐‘ค ) ๐‘ฅ ) โˆˆ ( ๐‘› โ€˜ ( ๐‘ โˆ– { ๐‘ฅ } ) ) ) โ†” ( ( ๐‘ โ€˜ ๐‘ ) = ๐‘‰ โˆง โˆ€ ๐‘ฅ โˆˆ ๐‘ โˆ€ ๐‘ฆ โˆˆ ( ๐พ โˆ– { 0 } ) ยฌ ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ( ๐‘ โ€˜ ( ๐‘ โˆ– { ๐‘ฅ } ) ) ) ) )
42 11 41 rabeqbidv โŠข ( ๐‘ค = ๐‘Š โ†’ { ๐‘ โˆˆ ๐’ซ ( Base โ€˜ ๐‘ค ) โˆฃ [ ( LSpan โ€˜ ๐‘ค ) / ๐‘› ] [ ( Scalar โ€˜ ๐‘ค ) / ๐‘“ ] ( ( ๐‘› โ€˜ ๐‘ ) = ( Base โ€˜ ๐‘ค ) โˆง โˆ€ ๐‘ฅ โˆˆ ๐‘ โˆ€ ๐‘ฆ โˆˆ ( ( Base โ€˜ ๐‘“ ) โˆ– { ( 0g โ€˜ ๐‘“ ) } ) ยฌ ( ๐‘ฆ ( ยท๐‘  โ€˜ ๐‘ค ) ๐‘ฅ ) โˆˆ ( ๐‘› โ€˜ ( ๐‘ โˆ– { ๐‘ฅ } ) ) ) } = { ๐‘ โˆˆ ๐’ซ ๐‘‰ โˆฃ ( ( ๐‘ โ€˜ ๐‘ ) = ๐‘‰ โˆง โˆ€ ๐‘ฅ โˆˆ ๐‘ โˆ€ ๐‘ฆ โˆˆ ( ๐พ โˆ– { 0 } ) ยฌ ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ( ๐‘ โ€˜ ( ๐‘ โˆ– { ๐‘ฅ } ) ) ) } )
43 df-lbs โŠข LBasis = ( ๐‘ค โˆˆ V โ†ฆ { ๐‘ โˆˆ ๐’ซ ( Base โ€˜ ๐‘ค ) โˆฃ [ ( LSpan โ€˜ ๐‘ค ) / ๐‘› ] [ ( Scalar โ€˜ ๐‘ค ) / ๐‘“ ] ( ( ๐‘› โ€˜ ๐‘ ) = ( Base โ€˜ ๐‘ค ) โˆง โˆ€ ๐‘ฅ โˆˆ ๐‘ โˆ€ ๐‘ฆ โˆˆ ( ( Base โ€˜ ๐‘“ ) โˆ– { ( 0g โ€˜ ๐‘“ ) } ) ยฌ ( ๐‘ฆ ( ยท๐‘  โ€˜ ๐‘ค ) ๐‘ฅ ) โˆˆ ( ๐‘› โ€˜ ( ๐‘ โˆ– { ๐‘ฅ } ) ) ) } )
44 1 fvexi โŠข ๐‘‰ โˆˆ V
45 44 pwex โŠข ๐’ซ ๐‘‰ โˆˆ V
46 45 rabex โŠข { ๐‘ โˆˆ ๐’ซ ๐‘‰ โˆฃ ( ( ๐‘ โ€˜ ๐‘ ) = ๐‘‰ โˆง โˆ€ ๐‘ฅ โˆˆ ๐‘ โˆ€ ๐‘ฆ โˆˆ ( ๐พ โˆ– { 0 } ) ยฌ ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ( ๐‘ โ€˜ ( ๐‘ โˆ– { ๐‘ฅ } ) ) ) } โˆˆ V
47 42 43 46 fvmpt โŠข ( ๐‘Š โˆˆ V โ†’ ( LBasis โ€˜ ๐‘Š ) = { ๐‘ โˆˆ ๐’ซ ๐‘‰ โˆฃ ( ( ๐‘ โ€˜ ๐‘ ) = ๐‘‰ โˆง โˆ€ ๐‘ฅ โˆˆ ๐‘ โˆ€ ๐‘ฆ โˆˆ ( ๐พ โˆ– { 0 } ) ยฌ ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ( ๐‘ โ€˜ ( ๐‘ โˆ– { ๐‘ฅ } ) ) ) } )
48 5 47 eqtrid โŠข ( ๐‘Š โˆˆ V โ†’ ๐ฝ = { ๐‘ โˆˆ ๐’ซ ๐‘‰ โˆฃ ( ( ๐‘ โ€˜ ๐‘ ) = ๐‘‰ โˆง โˆ€ ๐‘ฅ โˆˆ ๐‘ โˆ€ ๐‘ฆ โˆˆ ( ๐พ โˆ– { 0 } ) ยฌ ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ( ๐‘ โ€˜ ( ๐‘ โˆ– { ๐‘ฅ } ) ) ) } )
49 8 48 syl โŠข ( ๐‘Š โˆˆ ๐‘‹ โ†’ ๐ฝ = { ๐‘ โˆˆ ๐’ซ ๐‘‰ โˆฃ ( ( ๐‘ โ€˜ ๐‘ ) = ๐‘‰ โˆง โˆ€ ๐‘ฅ โˆˆ ๐‘ โˆ€ ๐‘ฆ โˆˆ ( ๐พ โˆ– { 0 } ) ยฌ ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ( ๐‘ โ€˜ ( ๐‘ โˆ– { ๐‘ฅ } ) ) ) } )
50 49 eleq2d โŠข ( ๐‘Š โˆˆ ๐‘‹ โ†’ ( ๐ต โˆˆ ๐ฝ โ†” ๐ต โˆˆ { ๐‘ โˆˆ ๐’ซ ๐‘‰ โˆฃ ( ( ๐‘ โ€˜ ๐‘ ) = ๐‘‰ โˆง โˆ€ ๐‘ฅ โˆˆ ๐‘ โˆ€ ๐‘ฆ โˆˆ ( ๐พ โˆ– { 0 } ) ยฌ ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ( ๐‘ โ€˜ ( ๐‘ โˆ– { ๐‘ฅ } ) ) ) } ) )
51 44 elpw2 โŠข ( ๐ต โˆˆ ๐’ซ ๐‘‰ โ†” ๐ต โŠ† ๐‘‰ )
52 51 anbi1i โŠข ( ( ๐ต โˆˆ ๐’ซ ๐‘‰ โˆง ( ( ๐‘ โ€˜ ๐ต ) = ๐‘‰ โˆง โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ( ๐พ โˆ– { 0 } ) ยฌ ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ( ๐‘ โ€˜ ( ๐ต โˆ– { ๐‘ฅ } ) ) ) ) โ†” ( ๐ต โŠ† ๐‘‰ โˆง ( ( ๐‘ โ€˜ ๐ต ) = ๐‘‰ โˆง โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ( ๐พ โˆ– { 0 } ) ยฌ ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ( ๐‘ โ€˜ ( ๐ต โˆ– { ๐‘ฅ } ) ) ) ) )
53 fveqeq2 โŠข ( ๐‘ = ๐ต โ†’ ( ( ๐‘ โ€˜ ๐‘ ) = ๐‘‰ โ†” ( ๐‘ โ€˜ ๐ต ) = ๐‘‰ ) )
54 difeq1 โŠข ( ๐‘ = ๐ต โ†’ ( ๐‘ โˆ– { ๐‘ฅ } ) = ( ๐ต โˆ– { ๐‘ฅ } ) )
55 54 fveq2d โŠข ( ๐‘ = ๐ต โ†’ ( ๐‘ โ€˜ ( ๐‘ โˆ– { ๐‘ฅ } ) ) = ( ๐‘ โ€˜ ( ๐ต โˆ– { ๐‘ฅ } ) ) )
56 55 eleq2d โŠข ( ๐‘ = ๐ต โ†’ ( ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ( ๐‘ โ€˜ ( ๐‘ โˆ– { ๐‘ฅ } ) ) โ†” ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ( ๐‘ โ€˜ ( ๐ต โˆ– { ๐‘ฅ } ) ) ) )
57 56 notbid โŠข ( ๐‘ = ๐ต โ†’ ( ยฌ ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ( ๐‘ โ€˜ ( ๐‘ โˆ– { ๐‘ฅ } ) ) โ†” ยฌ ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ( ๐‘ โ€˜ ( ๐ต โˆ– { ๐‘ฅ } ) ) ) )
58 57 ralbidv โŠข ( ๐‘ = ๐ต โ†’ ( โˆ€ ๐‘ฆ โˆˆ ( ๐พ โˆ– { 0 } ) ยฌ ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ( ๐‘ โ€˜ ( ๐‘ โˆ– { ๐‘ฅ } ) ) โ†” โˆ€ ๐‘ฆ โˆˆ ( ๐พ โˆ– { 0 } ) ยฌ ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ( ๐‘ โ€˜ ( ๐ต โˆ– { ๐‘ฅ } ) ) ) )
59 58 raleqbi1dv โŠข ( ๐‘ = ๐ต โ†’ ( โˆ€ ๐‘ฅ โˆˆ ๐‘ โˆ€ ๐‘ฆ โˆˆ ( ๐พ โˆ– { 0 } ) ยฌ ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ( ๐‘ โ€˜ ( ๐‘ โˆ– { ๐‘ฅ } ) ) โ†” โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ( ๐พ โˆ– { 0 } ) ยฌ ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ( ๐‘ โ€˜ ( ๐ต โˆ– { ๐‘ฅ } ) ) ) )
60 53 59 anbi12d โŠข ( ๐‘ = ๐ต โ†’ ( ( ( ๐‘ โ€˜ ๐‘ ) = ๐‘‰ โˆง โˆ€ ๐‘ฅ โˆˆ ๐‘ โˆ€ ๐‘ฆ โˆˆ ( ๐พ โˆ– { 0 } ) ยฌ ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ( ๐‘ โ€˜ ( ๐‘ โˆ– { ๐‘ฅ } ) ) ) โ†” ( ( ๐‘ โ€˜ ๐ต ) = ๐‘‰ โˆง โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ( ๐พ โˆ– { 0 } ) ยฌ ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ( ๐‘ โ€˜ ( ๐ต โˆ– { ๐‘ฅ } ) ) ) ) )
61 60 elrab โŠข ( ๐ต โˆˆ { ๐‘ โˆˆ ๐’ซ ๐‘‰ โˆฃ ( ( ๐‘ โ€˜ ๐‘ ) = ๐‘‰ โˆง โˆ€ ๐‘ฅ โˆˆ ๐‘ โˆ€ ๐‘ฆ โˆˆ ( ๐พ โˆ– { 0 } ) ยฌ ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ( ๐‘ โ€˜ ( ๐‘ โˆ– { ๐‘ฅ } ) ) ) } โ†” ( ๐ต โˆˆ ๐’ซ ๐‘‰ โˆง ( ( ๐‘ โ€˜ ๐ต ) = ๐‘‰ โˆง โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ( ๐พ โˆ– { 0 } ) ยฌ ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ( ๐‘ โ€˜ ( ๐ต โˆ– { ๐‘ฅ } ) ) ) ) )
62 3anass โŠข ( ( ๐ต โŠ† ๐‘‰ โˆง ( ๐‘ โ€˜ ๐ต ) = ๐‘‰ โˆง โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ( ๐พ โˆ– { 0 } ) ยฌ ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ( ๐‘ โ€˜ ( ๐ต โˆ– { ๐‘ฅ } ) ) ) โ†” ( ๐ต โŠ† ๐‘‰ โˆง ( ( ๐‘ โ€˜ ๐ต ) = ๐‘‰ โˆง โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ( ๐พ โˆ– { 0 } ) ยฌ ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ( ๐‘ โ€˜ ( ๐ต โˆ– { ๐‘ฅ } ) ) ) ) )
63 52 61 62 3bitr4i โŠข ( ๐ต โˆˆ { ๐‘ โˆˆ ๐’ซ ๐‘‰ โˆฃ ( ( ๐‘ โ€˜ ๐‘ ) = ๐‘‰ โˆง โˆ€ ๐‘ฅ โˆˆ ๐‘ โˆ€ ๐‘ฆ โˆˆ ( ๐พ โˆ– { 0 } ) ยฌ ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ( ๐‘ โ€˜ ( ๐‘ โˆ– { ๐‘ฅ } ) ) ) } โ†” ( ๐ต โŠ† ๐‘‰ โˆง ( ๐‘ โ€˜ ๐ต ) = ๐‘‰ โˆง โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ( ๐พ โˆ– { 0 } ) ยฌ ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ( ๐‘ โ€˜ ( ๐ต โˆ– { ๐‘ฅ } ) ) ) )
64 50 63 bitrdi โŠข ( ๐‘Š โˆˆ ๐‘‹ โ†’ ( ๐ต โˆˆ ๐ฝ โ†” ( ๐ต โŠ† ๐‘‰ โˆง ( ๐‘ โ€˜ ๐ต ) = ๐‘‰ โˆง โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ( ๐พ โˆ– { 0 } ) ยฌ ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ( ๐‘ โ€˜ ( ๐ต โˆ– { ๐‘ฅ } ) ) ) ) )