Metamath Proof Explorer


Theorem isclmi0

Description: Properties that determine a subcomplex module. (Contributed by NM, 5-Nov-2006) (Revised by AV, 4-Oct-2021)

Ref Expression
Hypotheses isclmp.t โŠข ยท = ( ยท๐‘  โ€˜ ๐‘Š )
isclmp.a โŠข + = ( +g โ€˜ ๐‘Š )
isclmp.v โŠข ๐‘‰ = ( Base โ€˜ ๐‘Š )
isclmp.s โŠข ๐‘† = ( Scalar โ€˜ ๐‘Š )
isclmp.k โŠข ๐พ = ( Base โ€˜ ๐‘† )
isclmi0.1 โŠข ๐‘† = ( โ„‚fld โ†พs ๐พ )
isclmi0.2 โŠข ๐‘Š โˆˆ Grp
isclmi0.3 โŠข ๐พ โˆˆ ( SubRing โ€˜ โ„‚fld )
isclmi0.4 โŠข ( ๐‘ฅ โˆˆ ๐‘‰ โ†’ ( 1 ยท ๐‘ฅ ) = ๐‘ฅ )
isclmi0.5 โŠข ( ( ๐‘ฆ โˆˆ ๐พ โˆง ๐‘ฅ โˆˆ ๐‘‰ ) โ†’ ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ๐‘‰ )
isclmi0.6 โŠข ( ( ๐‘ฆ โˆˆ ๐พ โˆง ๐‘ฅ โˆˆ ๐‘‰ โˆง ๐‘ง โˆˆ ๐‘‰ ) โ†’ ( ๐‘ฆ ยท ( ๐‘ฅ + ๐‘ง ) ) = ( ( ๐‘ฆ ยท ๐‘ฅ ) + ( ๐‘ฆ ยท ๐‘ง ) ) )
isclmi0.7 โŠข ( ( ๐‘ฆ โˆˆ ๐พ โˆง ๐‘ง โˆˆ ๐พ โˆง ๐‘ฅ โˆˆ ๐‘‰ ) โ†’ ( ( ๐‘ง + ๐‘ฆ ) ยท ๐‘ฅ ) = ( ( ๐‘ง ยท ๐‘ฅ ) + ( ๐‘ฆ ยท ๐‘ฅ ) ) )
isclmi0.8 โŠข ( ( ๐‘ฆ โˆˆ ๐พ โˆง ๐‘ง โˆˆ ๐พ โˆง ๐‘ฅ โˆˆ ๐‘‰ ) โ†’ ( ( ๐‘ง ยท ๐‘ฆ ) ยท ๐‘ฅ ) = ( ๐‘ง ยท ( ๐‘ฆ ยท ๐‘ฅ ) ) )
Assertion isclmi0 ๐‘Š โˆˆ โ„‚Mod

Proof

Step Hyp Ref Expression
1 isclmp.t โŠข ยท = ( ยท๐‘  โ€˜ ๐‘Š )
2 isclmp.a โŠข + = ( +g โ€˜ ๐‘Š )
3 isclmp.v โŠข ๐‘‰ = ( Base โ€˜ ๐‘Š )
4 isclmp.s โŠข ๐‘† = ( Scalar โ€˜ ๐‘Š )
5 isclmp.k โŠข ๐พ = ( Base โ€˜ ๐‘† )
6 isclmi0.1 โŠข ๐‘† = ( โ„‚fld โ†พs ๐พ )
7 isclmi0.2 โŠข ๐‘Š โˆˆ Grp
8 isclmi0.3 โŠข ๐พ โˆˆ ( SubRing โ€˜ โ„‚fld )
9 isclmi0.4 โŠข ( ๐‘ฅ โˆˆ ๐‘‰ โ†’ ( 1 ยท ๐‘ฅ ) = ๐‘ฅ )
10 isclmi0.5 โŠข ( ( ๐‘ฆ โˆˆ ๐พ โˆง ๐‘ฅ โˆˆ ๐‘‰ ) โ†’ ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ๐‘‰ )
11 isclmi0.6 โŠข ( ( ๐‘ฆ โˆˆ ๐พ โˆง ๐‘ฅ โˆˆ ๐‘‰ โˆง ๐‘ง โˆˆ ๐‘‰ ) โ†’ ( ๐‘ฆ ยท ( ๐‘ฅ + ๐‘ง ) ) = ( ( ๐‘ฆ ยท ๐‘ฅ ) + ( ๐‘ฆ ยท ๐‘ง ) ) )
12 isclmi0.7 โŠข ( ( ๐‘ฆ โˆˆ ๐พ โˆง ๐‘ง โˆˆ ๐พ โˆง ๐‘ฅ โˆˆ ๐‘‰ ) โ†’ ( ( ๐‘ง + ๐‘ฆ ) ยท ๐‘ฅ ) = ( ( ๐‘ง ยท ๐‘ฅ ) + ( ๐‘ฆ ยท ๐‘ฅ ) ) )
13 isclmi0.8 โŠข ( ( ๐‘ฆ โˆˆ ๐พ โˆง ๐‘ง โˆˆ ๐พ โˆง ๐‘ฅ โˆˆ ๐‘‰ ) โ†’ ( ( ๐‘ง ยท ๐‘ฆ ) ยท ๐‘ฅ ) = ( ๐‘ง ยท ( ๐‘ฆ ยท ๐‘ฅ ) ) )
14 7 6 8 3pm3.2i โŠข ( ๐‘Š โˆˆ Grp โˆง ๐‘† = ( โ„‚fld โ†พs ๐พ ) โˆง ๐พ โˆˆ ( SubRing โ€˜ โ„‚fld ) )
15 10 ancoms โŠข ( ( ๐‘ฅ โˆˆ ๐‘‰ โˆง ๐‘ฆ โˆˆ ๐พ ) โ†’ ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ๐‘‰ )
16 11 3com12 โŠข ( ( ๐‘ฅ โˆˆ ๐‘‰ โˆง ๐‘ฆ โˆˆ ๐พ โˆง ๐‘ง โˆˆ ๐‘‰ ) โ†’ ( ๐‘ฆ ยท ( ๐‘ฅ + ๐‘ง ) ) = ( ( ๐‘ฆ ยท ๐‘ฅ ) + ( ๐‘ฆ ยท ๐‘ง ) ) )
17 16 3expa โŠข ( ( ( ๐‘ฅ โˆˆ ๐‘‰ โˆง ๐‘ฆ โˆˆ ๐พ ) โˆง ๐‘ง โˆˆ ๐‘‰ ) โ†’ ( ๐‘ฆ ยท ( ๐‘ฅ + ๐‘ง ) ) = ( ( ๐‘ฆ ยท ๐‘ฅ ) + ( ๐‘ฆ ยท ๐‘ง ) ) )
18 17 ralrimiva โŠข ( ( ๐‘ฅ โˆˆ ๐‘‰ โˆง ๐‘ฆ โˆˆ ๐พ ) โ†’ โˆ€ ๐‘ง โˆˆ ๐‘‰ ( ๐‘ฆ ยท ( ๐‘ฅ + ๐‘ง ) ) = ( ( ๐‘ฆ ยท ๐‘ฅ ) + ( ๐‘ฆ ยท ๐‘ง ) ) )
19 12 13 jca โŠข ( ( ๐‘ฆ โˆˆ ๐พ โˆง ๐‘ง โˆˆ ๐พ โˆง ๐‘ฅ โˆˆ ๐‘‰ ) โ†’ ( ( ( ๐‘ง + ๐‘ฆ ) ยท ๐‘ฅ ) = ( ( ๐‘ง ยท ๐‘ฅ ) + ( ๐‘ฆ ยท ๐‘ฅ ) ) โˆง ( ( ๐‘ง ยท ๐‘ฆ ) ยท ๐‘ฅ ) = ( ๐‘ง ยท ( ๐‘ฆ ยท ๐‘ฅ ) ) ) )
20 19 3comr โŠข ( ( ๐‘ฅ โˆˆ ๐‘‰ โˆง ๐‘ฆ โˆˆ ๐พ โˆง ๐‘ง โˆˆ ๐พ ) โ†’ ( ( ( ๐‘ง + ๐‘ฆ ) ยท ๐‘ฅ ) = ( ( ๐‘ง ยท ๐‘ฅ ) + ( ๐‘ฆ ยท ๐‘ฅ ) ) โˆง ( ( ๐‘ง ยท ๐‘ฆ ) ยท ๐‘ฅ ) = ( ๐‘ง ยท ( ๐‘ฆ ยท ๐‘ฅ ) ) ) )
21 20 3expa โŠข ( ( ( ๐‘ฅ โˆˆ ๐‘‰ โˆง ๐‘ฆ โˆˆ ๐พ ) โˆง ๐‘ง โˆˆ ๐พ ) โ†’ ( ( ( ๐‘ง + ๐‘ฆ ) ยท ๐‘ฅ ) = ( ( ๐‘ง ยท ๐‘ฅ ) + ( ๐‘ฆ ยท ๐‘ฅ ) ) โˆง ( ( ๐‘ง ยท ๐‘ฆ ) ยท ๐‘ฅ ) = ( ๐‘ง ยท ( ๐‘ฆ ยท ๐‘ฅ ) ) ) )
22 21 ralrimiva โŠข ( ( ๐‘ฅ โˆˆ ๐‘‰ โˆง ๐‘ฆ โˆˆ ๐พ ) โ†’ โˆ€ ๐‘ง โˆˆ ๐พ ( ( ( ๐‘ง + ๐‘ฆ ) ยท ๐‘ฅ ) = ( ( ๐‘ง ยท ๐‘ฅ ) + ( ๐‘ฆ ยท ๐‘ฅ ) ) โˆง ( ( ๐‘ง ยท ๐‘ฆ ) ยท ๐‘ฅ ) = ( ๐‘ง ยท ( ๐‘ฆ ยท ๐‘ฅ ) ) ) )
23 15 18 22 3jca โŠข ( ( ๐‘ฅ โˆˆ ๐‘‰ โˆง ๐‘ฆ โˆˆ ๐พ ) โ†’ ( ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ๐‘‰ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‰ ( ๐‘ฆ ยท ( ๐‘ฅ + ๐‘ง ) ) = ( ( ๐‘ฆ ยท ๐‘ฅ ) + ( ๐‘ฆ ยท ๐‘ง ) ) โˆง โˆ€ ๐‘ง โˆˆ ๐พ ( ( ( ๐‘ง + ๐‘ฆ ) ยท ๐‘ฅ ) = ( ( ๐‘ง ยท ๐‘ฅ ) + ( ๐‘ฆ ยท ๐‘ฅ ) ) โˆง ( ( ๐‘ง ยท ๐‘ฆ ) ยท ๐‘ฅ ) = ( ๐‘ง ยท ( ๐‘ฆ ยท ๐‘ฅ ) ) ) ) )
24 23 ralrimiva โŠข ( ๐‘ฅ โˆˆ ๐‘‰ โ†’ โˆ€ ๐‘ฆ โˆˆ ๐พ ( ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ๐‘‰ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‰ ( ๐‘ฆ ยท ( ๐‘ฅ + ๐‘ง ) ) = ( ( ๐‘ฆ ยท ๐‘ฅ ) + ( ๐‘ฆ ยท ๐‘ง ) ) โˆง โˆ€ ๐‘ง โˆˆ ๐พ ( ( ( ๐‘ง + ๐‘ฆ ) ยท ๐‘ฅ ) = ( ( ๐‘ง ยท ๐‘ฅ ) + ( ๐‘ฆ ยท ๐‘ฅ ) ) โˆง ( ( ๐‘ง ยท ๐‘ฆ ) ยท ๐‘ฅ ) = ( ๐‘ง ยท ( ๐‘ฆ ยท ๐‘ฅ ) ) ) ) )
25 9 24 jca โŠข ( ๐‘ฅ โˆˆ ๐‘‰ โ†’ ( ( 1 ยท ๐‘ฅ ) = ๐‘ฅ โˆง โˆ€ ๐‘ฆ โˆˆ ๐พ ( ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ๐‘‰ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‰ ( ๐‘ฆ ยท ( ๐‘ฅ + ๐‘ง ) ) = ( ( ๐‘ฆ ยท ๐‘ฅ ) + ( ๐‘ฆ ยท ๐‘ง ) ) โˆง โˆ€ ๐‘ง โˆˆ ๐พ ( ( ( ๐‘ง + ๐‘ฆ ) ยท ๐‘ฅ ) = ( ( ๐‘ง ยท ๐‘ฅ ) + ( ๐‘ฆ ยท ๐‘ฅ ) ) โˆง ( ( ๐‘ง ยท ๐‘ฆ ) ยท ๐‘ฅ ) = ( ๐‘ง ยท ( ๐‘ฆ ยท ๐‘ฅ ) ) ) ) ) )
26 25 rgen โŠข โˆ€ ๐‘ฅ โˆˆ ๐‘‰ ( ( 1 ยท ๐‘ฅ ) = ๐‘ฅ โˆง โˆ€ ๐‘ฆ โˆˆ ๐พ ( ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ๐‘‰ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‰ ( ๐‘ฆ ยท ( ๐‘ฅ + ๐‘ง ) ) = ( ( ๐‘ฆ ยท ๐‘ฅ ) + ( ๐‘ฆ ยท ๐‘ง ) ) โˆง โˆ€ ๐‘ง โˆˆ ๐พ ( ( ( ๐‘ง + ๐‘ฆ ) ยท ๐‘ฅ ) = ( ( ๐‘ง ยท ๐‘ฅ ) + ( ๐‘ฆ ยท ๐‘ฅ ) ) โˆง ( ( ๐‘ง ยท ๐‘ฆ ) ยท ๐‘ฅ ) = ( ๐‘ง ยท ( ๐‘ฆ ยท ๐‘ฅ ) ) ) ) )
27 1 2 3 4 5 isclmp โŠข ( ๐‘Š โˆˆ โ„‚Mod โ†” ( ( ๐‘Š โˆˆ Grp โˆง ๐‘† = ( โ„‚fld โ†พs ๐พ ) โˆง ๐พ โˆˆ ( SubRing โ€˜ โ„‚fld ) ) โˆง โˆ€ ๐‘ฅ โˆˆ ๐‘‰ ( ( 1 ยท ๐‘ฅ ) = ๐‘ฅ โˆง โˆ€ ๐‘ฆ โˆˆ ๐พ ( ( ๐‘ฆ ยท ๐‘ฅ ) โˆˆ ๐‘‰ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‰ ( ๐‘ฆ ยท ( ๐‘ฅ + ๐‘ง ) ) = ( ( ๐‘ฆ ยท ๐‘ฅ ) + ( ๐‘ฆ ยท ๐‘ง ) ) โˆง โˆ€ ๐‘ง โˆˆ ๐พ ( ( ( ๐‘ง + ๐‘ฆ ) ยท ๐‘ฅ ) = ( ( ๐‘ง ยท ๐‘ฅ ) + ( ๐‘ฆ ยท ๐‘ฅ ) ) โˆง ( ( ๐‘ง ยท ๐‘ฆ ) ยท ๐‘ฅ ) = ( ๐‘ง ยท ( ๐‘ฆ ยท ๐‘ฅ ) ) ) ) ) ) )
28 14 26 27 mpbir2an โŠข ๐‘Š โˆˆ โ„‚Mod