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