Metamath Proof Explorer

Theorem isclmp

Description: The predicate "is a subcomplex module". (Contributed by NM, 31-May-2008) (Revised by AV, 4-Oct-2021)

Ref Expression
Hypotheses isclmp.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
isclmp.a ⊢ + = ( +g ‘ 𝑊 )
isclmp.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
isclmp.s ⊢ 𝑆 = ( Scalar ‘ 𝑊 )
isclmp.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
Assertion isclmp ( 𝑊 ∈ ℂMod ↔ ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ∧ ∀ 𝑥 ∈ 𝑉 ( ( 1 · 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝐾 ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) ) ) ) )

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 4 5 isclm ⊢ ( 𝑊 ∈ ℂMod ↔ ( 𝑊 ∈ LMod ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) )
7 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
8 eqid ⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
9 eqid ⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
10 3 2 1 4 5 7 8 9 islmod ⊢ ( 𝑊 ∈ LMod ↔ ( 𝑊 ∈ Grp ∧ 𝑆 ∈ Ring ∧ ∀ 𝑟 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ) ∧ ( ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ∧ ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ) ) ) )
11 10 3anbi1i ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ↔ ( ( 𝑊 ∈ Grp ∧ 𝑆 ∈ Ring ∧ ∀ 𝑟 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ) ∧ ( ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ∧ ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ) ) ) ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) )
12 3anass ⊢ ( ( ( 𝑊 ∈ Grp ∧ 𝑆 ∈ Ring ∧ ∀ 𝑟 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ) ∧ ( ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ∧ ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ) ) ) ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ↔ ( ( 𝑊 ∈ Grp ∧ 𝑆 ∈ Ring ∧ ∀ 𝑟 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ) ∧ ( ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ∧ ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ) ) ) ∧ ( 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ) )
13 df-3an ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑆 ∈ Ring ∧ ∀ 𝑟 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ) ∧ ( ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ∧ ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ) ) ) ↔ ( ( 𝑊 ∈ Grp ∧ 𝑆 ∈ Ring ) ∧ ∀ 𝑟 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ) ∧ ( ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ∧ ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ) ) ) )
14 13 anbi1i ⊢ ( ( ( 𝑊 ∈ Grp ∧ 𝑆 ∈ Ring ∧ ∀ 𝑟 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ) ∧ ( ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ∧ ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ) ) ) ∧ ( 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ) ↔ ( ( ( 𝑊 ∈ Grp ∧ 𝑆 ∈ Ring ) ∧ ∀ 𝑟 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ) ∧ ( ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ∧ ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ) ) ) ∧ ( 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ) )
15 12 14 bitri ⊢ ( ( ( 𝑊 ∈ Grp ∧ 𝑆 ∈ Ring ∧ ∀ 𝑟 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ) ∧ ( ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ∧ ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ) ) ) ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ↔ ( ( ( 𝑊 ∈ Grp ∧ 𝑆 ∈ Ring ) ∧ ∀ 𝑟 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ) ∧ ( ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ∧ ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ) ) ) ∧ ( 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ) )
16 an32 ⊢ ( ( ( ( 𝑊 ∈ Grp ∧ 𝑆 ∈ Ring ) ∧ ∀ 𝑟 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ) ∧ ( ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ∧ ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ) ) ) ∧ ( 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ) ↔ ( ( ( 𝑊 ∈ Grp ∧ 𝑆 ∈ Ring ) ∧ ( 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ) ∧ ∀ 𝑟 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ) ∧ ( ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ∧ ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ) ) ) )
17 11 15 16 3bitri ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ↔ ( ( ( 𝑊 ∈ Grp ∧ 𝑆 ∈ Ring ) ∧ ( 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ) ∧ ∀ 𝑟 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ) ∧ ( ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ∧ ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ) ) ) )
18 an32 ⊢ ( ( ( 𝑊 ∈ Grp ∧ 𝑆 ∈ Ring ) ∧ ( 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ) ↔ ( ( 𝑊 ∈ Grp ∧ ( 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ) ∧ 𝑆 ∈ Ring ) )
19 3anass ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ↔ ( 𝑊 ∈ Grp ∧ ( 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ) )
20 19 bicomi ⊢ ( ( 𝑊 ∈ Grp ∧ ( 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ) ↔ ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) )
21 20 anbi1i ⊢ ( ( ( 𝑊 ∈ Grp ∧ ( 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ) ∧ 𝑆 ∈ Ring ) ↔ ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ∧ 𝑆 ∈ Ring ) )
22 18 21 bitri ⊢ ( ( ( 𝑊 ∈ Grp ∧ 𝑆 ∈ Ring ) ∧ ( 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ) ↔ ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ∧ 𝑆 ∈ Ring ) )
23 22 anbi1i ⊢ ( ( ( ( 𝑊 ∈ Grp ∧ 𝑆 ∈ Ring ) ∧ ( 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ) ∧ ∀ 𝑟 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ) ∧ ( ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ∧ ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ) ) ) ↔ ( ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ∧ 𝑆 ∈ Ring ) ∧ ∀ 𝑟 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ) ∧ ( ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ∧ ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ) ) ) )
24 anass ⊢ ( ( ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ∧ 𝑆 ∈ Ring ) ∧ ∀ 𝑟 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ) ∧ ( ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ∧ ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ) ) ) ↔ ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ∧ ( 𝑆 ∈ Ring ∧ ∀ 𝑟 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ) ∧ ( ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ∧ ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ) ) ) ) )
25 df-3an ⊢ ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ) ↔ ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ) )
26 ancom ⊢ ( ( ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ∧ ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ) ↔ ( ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ∧ ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) )
27 25 26 anbi12i ⊢ ( ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ) ∧ ( ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ∧ ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ) ) ↔ ( ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ) ∧ ( ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ∧ ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) )
28 an4 ⊢ ( ( ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ) ∧ ( ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ∧ ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ↔ ( ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ) ∧ ( ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) )
29 an32 ⊢ ( ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ) ↔ ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) )
30 ancom ⊢ ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ) ↔ ( ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) )
31 30 anbi1i ⊢ ( ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ↔ ( ( ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) )
32 29 31 bitri ⊢ ( ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ) ↔ ( ( ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) )
33 32 anbi1i ⊢ ( ( ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ) ∧ ( ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ↔ ( ( ( ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) )
34 27 28 33 3bitri ⊢ ( ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ) ∧ ( ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ∧ ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ) ) ↔ ( ( ( ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) )
35 fveq2 ⊢ ( 𝑆 = ( ℂfld ↾s 𝐾 ) → ( 1r ‘ 𝑆 ) = ( 1r ‘ ( ℂfld ↾s 𝐾 ) ) )
36 eqid ⊢ ( ℂfld ↾s 𝐾 ) = ( ℂfld ↾s 𝐾 )
37 eqid ⊢ ( 1r ‘ ℂfld ) = ( 1r ‘ ℂfld )
38 36 37 subrg1 ⊢ ( 𝐾 ∈ ( SubRing ‘ ℂfld ) → ( 1r ‘ ℂfld ) = ( 1r ‘ ( ℂfld ↾s 𝐾 ) ) )
39 38 eqcomd ⊢ ( 𝐾 ∈ ( SubRing ‘ ℂfld ) → ( 1r ‘ ( ℂfld ↾s 𝐾 ) ) = ( 1r ‘ ℂfld ) )
40 35 39 sylan9eq ⊢ ( ( 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → ( 1r ‘ 𝑆 ) = ( 1r ‘ ℂfld ) )
41 cnfld1 ⊢ 1 = ( 1r ‘ ℂfld )
42 40 41 eqtr4di ⊢ ( ( 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → ( 1r ‘ 𝑆 ) = 1 )
43 42 oveq1d ⊢ ( ( 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → ( ( 1r ‘ 𝑆 ) · 𝑥 ) = ( 1 · 𝑥 ) )
44 43 eqeq1d ⊢ ( ( 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → ( ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ↔ ( 1 · 𝑥 ) = 𝑥 ) )
45 44 3adant1 ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → ( ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ↔ ( 1 · 𝑥 ) = 𝑥 ) )
46 45 ad2antrr ⊢ ( ( ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) ∧ ( 𝑧 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) ) → ( ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ↔ ( 1 · 𝑥 ) = 𝑥 ) )
47 46 anbi1d ⊢ ( ( ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) ∧ ( 𝑧 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) ) → ( ( ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ↔ ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ) )
48 47 anbi1d ⊢ ( ( ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) ∧ ( 𝑧 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) ) → ( ( ( ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ↔ ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ) )
49 eqid ⊢ ( +g ‘ ℂfld ) = ( +g ‘ ℂfld )
50 36 49 ressplusg ⊢ ( 𝐾 ∈ ( SubRing ‘ ℂfld ) → ( +g ‘ ℂfld ) = ( +g ‘ ( ℂfld ↾s 𝐾 ) ) )
51 50 adantl ⊢ ( ( 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → ( +g ‘ ℂfld ) = ( +g ‘ ( ℂfld ↾s 𝐾 ) ) )
52 cnfldadd ⊢ + = ( +g ‘ ℂfld )
53 52 a1i ⊢ ( ( 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → + = ( +g ‘ ℂfld ) )
54 fveq2 ⊢ ( 𝑆 = ( ℂfld ↾s 𝐾 ) → ( +g ‘ 𝑆 ) = ( +g ‘ ( ℂfld ↾s 𝐾 ) ) )
55 54 adantr ⊢ ( ( 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → ( +g ‘ 𝑆 ) = ( +g ‘ ( ℂfld ↾s 𝐾 ) ) )
56 51 53 55 3eqtr4rd ⊢ ( ( 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → ( +g ‘ 𝑆 ) = + )
57 56 3adant1 ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → ( +g ‘ 𝑆 ) = + )
58 57 oveqd ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) = ( 𝑟 + 𝑦 ) )
59 58 ad2antrr ⊢ ( ( ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) ∧ ( 𝑧 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) ) → ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) = ( 𝑟 + 𝑦 ) )
60 59 oveq1d ⊢ ( ( ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) ∧ ( 𝑧 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) ) → ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 + 𝑦 ) · 𝑥 ) )
61 60 eqeq1d ⊢ ( ( ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) ∧ ( 𝑧 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) ) → ( ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ↔ ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ) )
62 eqid ⊢ ( .r ‘ ℂfld ) = ( .r ‘ ℂfld )
63 36 62 ressmulr ⊢ ( 𝐾 ∈ ( SubRing ‘ ℂfld ) → ( .r ‘ ℂfld ) = ( .r ‘ ( ℂfld ↾s 𝐾 ) ) )
64 63 3ad2ant3 ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → ( .r ‘ ℂfld ) = ( .r ‘ ( ℂfld ↾s 𝐾 ) ) )
65 cnfldmul ⊢ · = ( .r ‘ ℂfld )
66 65 a1i ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → · = ( .r ‘ ℂfld ) )
67 fveq2 ⊢ ( 𝑆 = ( ℂfld ↾s 𝐾 ) → ( .r ‘ 𝑆 ) = ( .r ‘ ( ℂfld ↾s 𝐾 ) ) )
68 67 3ad2ant2 ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → ( .r ‘ 𝑆 ) = ( .r ‘ ( ℂfld ↾s 𝐾 ) ) )
69 64 66 68 3eqtr4rd ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → ( .r ‘ 𝑆 ) = · )
70 69 oveqd ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) = ( 𝑟 · 𝑦 ) )
71 70 ad2antrr ⊢ ( ( ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) ∧ ( 𝑧 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) ) → ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) = ( 𝑟 · 𝑦 ) )
72 71 oveq1d ⊢ ( ( ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) ∧ ( 𝑧 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) ) → ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑦 ) · 𝑥 ) )
73 72 eqeq1d ⊢ ( ( ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) ∧ ( 𝑧 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) ) → ( ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ↔ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) )
74 61 73 anbi12d ⊢ ( ( ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) ∧ ( 𝑧 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) ) → ( ( ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ↔ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) )
75 48 74 anbi12d ⊢ ( ( ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) ∧ ( 𝑧 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) ) → ( ( ( ( ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ↔ ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ) )
76 34 75 syl5bb ⊢ ( ( ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) ∧ ( 𝑧 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) ) → ( ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ) ∧ ( ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ∧ ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ) ) ↔ ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ) )
77 76 2ralbidva ⊢ ( ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ∧ ( 𝑟 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( ∀ 𝑧 ∈ 𝑉 ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ) ∧ ( ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ∧ ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ) ) ↔ ∀ 𝑧 ∈ 𝑉 ∀ 𝑥 ∈ 𝑉 ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ) )
78 77 2ralbidva ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → ( ∀ 𝑟 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ) ∧ ( ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ∧ ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ) ) ↔ ∀ 𝑟 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ∀ 𝑥 ∈ 𝑉 ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ) )
79 ralrot3 ⊢ ( ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ∀ 𝑥 ∈ 𝑉 ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ↔ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) )
80 79 ralbii ⊢ ( ∀ 𝑟 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ∀ 𝑥 ∈ 𝑉 ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ↔ ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) )
81 ralcom ⊢ ( ∀ 𝑟 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ↔ ∀ 𝑥 ∈ 𝑉 ∀ 𝑟 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) )
82 80 81 bitri ⊢ ( ∀ 𝑟 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ∀ 𝑥 ∈ 𝑉 ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ↔ ∀ 𝑥 ∈ 𝑉 ∀ 𝑟 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) )
83 ralcom ⊢ ( ∀ 𝑟 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ↔ ∀ 𝑦 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) )
84 83 ralbii ⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑟 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ↔ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) )
85 ralcom ⊢ ( ∀ 𝑟 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ↔ ∀ 𝑧 ∈ 𝑉 ∀ 𝑟 ∈ 𝐾 ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) )
86 85 2ralbii ⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝐾 ∀ 𝑟 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ↔ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ∀ 𝑟 ∈ 𝐾 ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) )
87 82 84 86 3bitri ⊢ ( ∀ 𝑟 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ∀ 𝑥 ∈ 𝑉 ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ↔ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ∀ 𝑟 ∈ 𝐾 ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) )
88 78 87 bitrdi ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → ( ∀ 𝑟 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ) ∧ ( ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ∧ ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ∀ 𝑟 ∈ 𝐾 ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ) )
89 36 subrgring ⊢ ( 𝐾 ∈ ( SubRing ‘ ℂfld ) → ( ℂfld ↾s 𝐾 ) ∈ Ring )
90 89 3ad2ant3 ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → ( ℂfld ↾s 𝐾 ) ∈ Ring )
91 eleq1 ⊢ ( 𝑆 = ( ℂfld ↾s 𝐾 ) → ( 𝑆 ∈ Ring ↔ ( ℂfld ↾s 𝐾 ) ∈ Ring ) )
92 91 3ad2ant2 ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → ( 𝑆 ∈ Ring ↔ ( ℂfld ↾s 𝐾 ) ∈ Ring ) )
93 90 92 mpbird ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → 𝑆 ∈ Ring )
94 93 biantrurd ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → ( ∀ 𝑟 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ) ∧ ( ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ∧ ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ) ) ↔ ( 𝑆 ∈ Ring ∧ ∀ 𝑟 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ) ∧ ( ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ∧ ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ) ) ) ) )
95 3 grpbn0 ⊢ ( 𝑊 ∈ Grp → 𝑉 ≠ ∅ )
96 95 3ad2ant1 ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → 𝑉 ≠ ∅ )
97 37 subrg1cl ⊢ ( 𝐾 ∈ ( SubRing ‘ ℂfld ) → ( 1r ‘ ℂfld ) ∈ 𝐾 )
98 97 ne0d ⊢ ( 𝐾 ∈ ( SubRing ‘ ℂfld ) → 𝐾 ≠ ∅ )
99 98 3ad2ant3 ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → 𝐾 ≠ ∅ )
100 ancom ⊢ ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ↔ ( ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ) )
101 100 anbi1i ⊢ ( ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ↔ ( ( ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) )
102 101 a1i ⊢ ( ( 𝑉 ≠ ∅ ∧ 𝐾 ≠ ∅ ) → ( ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ↔ ( ( ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ) )
103 102 ralbidv ⊢ ( ( 𝑉 ≠ ∅ ∧ 𝐾 ≠ ∅ ) → ( ∀ 𝑟 ∈ 𝐾 ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ↔ ∀ 𝑟 ∈ 𝐾 ( ( ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ) )
104 r19.28zv ⊢ ( 𝐾 ≠ ∅ → ( ∀ 𝑟 ∈ 𝐾 ( ( ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ↔ ( ( ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ) ∧ ∀ 𝑟 ∈ 𝐾 ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ) )
105 104 adantl ⊢ ( ( 𝑉 ≠ ∅ ∧ 𝐾 ≠ ∅ ) → ( ∀ 𝑟 ∈ 𝐾 ( ( ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ↔ ( ( ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ) ∧ ∀ 𝑟 ∈ 𝐾 ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ) )
106 103 105 bitrd ⊢ ( ( 𝑉 ≠ ∅ ∧ 𝐾 ≠ ∅ ) → ( ∀ 𝑟 ∈ 𝐾 ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ↔ ( ( ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ) ∧ ∀ 𝑟 ∈ 𝐾 ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ) )
107 anass ⊢ ( ( ( ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ) ∧ ∀ 𝑟 ∈ 𝐾 ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ↔ ( ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ∀ 𝑟 ∈ 𝐾 ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ) )
108 anass ⊢ ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ∀ 𝑟 ∈ 𝐾 ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ↔ ( ( 1 · 𝑥 ) = 𝑥 ∧ ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑟 ∈ 𝐾 ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ) )
109 108 anbi2i ⊢ ( ( ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ∀ 𝑟 ∈ 𝐾 ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ) ↔ ( ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 1 · 𝑥 ) = 𝑥 ∧ ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑟 ∈ 𝐾 ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ) ) )
110 ancom ⊢ ( ( ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 1 · 𝑥 ) = 𝑥 ∧ ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑟 ∈ 𝐾 ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ) ) ↔ ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑟 ∈ 𝐾 ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) )
111 107 109 110 3bitri ⊢ ( ( ( ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ) ∧ ∀ 𝑟 ∈ 𝐾 ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ↔ ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑟 ∈ 𝐾 ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) )
112 106 111 bitrdi ⊢ ( ( 𝑉 ≠ ∅ ∧ 𝐾 ≠ ∅ ) → ( ∀ 𝑟 ∈ 𝐾 ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ↔ ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑟 ∈ 𝐾 ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ) )
113 112 ralbidv ⊢ ( ( 𝑉 ≠ ∅ ∧ 𝐾 ≠ ∅ ) → ( ∀ 𝑧 ∈ 𝑉 ∀ 𝑟 ∈ 𝐾 ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ↔ ∀ 𝑧 ∈ 𝑉 ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑟 ∈ 𝐾 ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ) )
114 r19.28zv ⊢ ( 𝑉 ≠ ∅ → ( ∀ 𝑧 ∈ 𝑉 ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑟 ∈ 𝐾 ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ↔ ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑟 ∈ 𝐾 ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ) ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ) )
115 114 adantr ⊢ ( ( 𝑉 ≠ ∅ ∧ 𝐾 ≠ ∅ ) → ( ∀ 𝑧 ∈ 𝑉 ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑟 ∈ 𝐾 ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ↔ ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑟 ∈ 𝐾 ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ) ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ) )
116 113 115 bitrd ⊢ ( ( 𝑉 ≠ ∅ ∧ 𝐾 ≠ ∅ ) → ( ∀ 𝑧 ∈ 𝑉 ∀ 𝑟 ∈ 𝐾 ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ↔ ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑟 ∈ 𝐾 ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ) ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ) )
117 anass ⊢ ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑟 ∈ 𝐾 ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ) ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ↔ ( ( 1 · 𝑥 ) = 𝑥 ∧ ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑟 ∈ 𝐾 ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ) )
118 oveq1 ⊢ ( 𝑧 = 𝑟 → ( 𝑧 + 𝑦 ) = ( 𝑟 + 𝑦 ) )
119 118 oveq1d ⊢ ( 𝑧 = 𝑟 → ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 + 𝑦 ) · 𝑥 ) )
120 oveq1 ⊢ ( 𝑧 = 𝑟 → ( 𝑧 · 𝑥 ) = ( 𝑟 · 𝑥 ) )
121 120 oveq1d ⊢ ( 𝑧 = 𝑟 → ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) )
122 119 121 eqeq12d ⊢ ( 𝑧 = 𝑟 → ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ↔ ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ) )
123 oveq1 ⊢ ( 𝑧 = 𝑟 → ( 𝑧 · 𝑦 ) = ( 𝑟 · 𝑦 ) )
124 123 oveq1d ⊢ ( 𝑧 = 𝑟 → ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑦 ) · 𝑥 ) )
125 oveq1 ⊢ ( 𝑧 = 𝑟 → ( 𝑧 · ( 𝑦 · 𝑥 ) ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) )
126 124 125 eqeq12d ⊢ ( 𝑧 = 𝑟 → ( ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ↔ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) )
127 122 126 anbi12d ⊢ ( 𝑧 = 𝑟 → ( ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) ↔ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) )
128 127 cbvralvw ⊢ ( ∀ 𝑧 ∈ 𝐾 ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) ↔ ∀ 𝑟 ∈ 𝐾 ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) )
129 128 3anbi3i ⊢ ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝐾 ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) ) ↔ ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑟 ∈ 𝐾 ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) )
130 3anan32 ⊢ ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑟 ∈ 𝐾 ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ↔ ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑟 ∈ 𝐾 ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) )
131 129 130 bitri ⊢ ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝐾 ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) ) ↔ ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑟 ∈ 𝐾 ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) )
132 131 bicomi ⊢ ( ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑟 ∈ 𝐾 ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ↔ ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝐾 ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) ) )
133 132 anbi2i ⊢ ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑟 ∈ 𝐾 ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ) ↔ ( ( 1 · 𝑥 ) = 𝑥 ∧ ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝐾 ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) ) ) )
134 117 133 bitri ⊢ ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑟 ∈ 𝐾 ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ) ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ↔ ( ( 1 · 𝑥 ) = 𝑥 ∧ ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝐾 ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) ) ) )
135 116 134 bitrdi ⊢ ( ( 𝑉 ≠ ∅ ∧ 𝐾 ≠ ∅ ) → ( ∀ 𝑧 ∈ 𝑉 ∀ 𝑟 ∈ 𝐾 ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ↔ ( ( 1 · 𝑥 ) = 𝑥 ∧ ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝐾 ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) ) ) ) )
136 135 ralbidv ⊢ ( ( 𝑉 ≠ ∅ ∧ 𝐾 ≠ ∅ ) → ( ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ∀ 𝑟 ∈ 𝐾 ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ↔ ∀ 𝑦 ∈ 𝐾 ( ( 1 · 𝑥 ) = 𝑥 ∧ ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝐾 ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) ) ) ) )
137 r19.28zv ⊢ ( 𝐾 ≠ ∅ → ( ∀ 𝑦 ∈ 𝐾 ( ( 1 · 𝑥 ) = 𝑥 ∧ ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝐾 ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) ) ) ↔ ( ( 1 · 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝐾 ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) ) ) ) )
138 137 adantl ⊢ ( ( 𝑉 ≠ ∅ ∧ 𝐾 ≠ ∅ ) → ( ∀ 𝑦 ∈ 𝐾 ( ( 1 · 𝑥 ) = 𝑥 ∧ ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝐾 ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) ) ) ↔ ( ( 1 · 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝐾 ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) ) ) ) )
139 136 138 bitrd ⊢ ( ( 𝑉 ≠ ∅ ∧ 𝐾 ≠ ∅ ) → ( ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ∀ 𝑟 ∈ 𝐾 ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ↔ ( ( 1 · 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝐾 ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) ) ) ) )
140 96 99 139 syl2anc ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → ( ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ∀ 𝑟 ∈ 𝐾 ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ↔ ( ( 1 · 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝐾 ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) ) ) ) )
141 140 ralbidv ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ∀ 𝑟 ∈ 𝐾 ( ( ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑦 · 𝑥 ) ∈ 𝑉 ) ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ) ∧ ( ( ( 𝑟 + 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑟 · 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ) ) ↔ ∀ 𝑥 ∈ 𝑉 ( ( 1 · 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝐾 ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) ) ) ) )
142 88 94 141 3bitr3d ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → ( ( 𝑆 ∈ Ring ∧ ∀ 𝑟 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ) ∧ ( ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ∧ ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ) ) ) ↔ ∀ 𝑥 ∈ 𝑉 ( ( 1 · 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝐾 ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) ) ) ) )
143 142 pm5.32i ⊢ ( ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ∧ ( 𝑆 ∈ Ring ∧ ∀ 𝑟 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ) ∧ ( ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ∧ ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ) ) ) ) ↔ ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ∧ ∀ 𝑥 ∈ 𝑉 ( ( 1 · 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝐾 ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) ) ) ) )
144 23 24 143 3bitri ⊢ ( ( ( ( 𝑊 ∈ Grp ∧ 𝑆 ∈ Ring ) ∧ ( 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ) ∧ ∀ 𝑟 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝑉 ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ( ( 𝑟 ( +g ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( ( 𝑟 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ) ∧ ( ( ( 𝑟 ( .r ‘ 𝑆 ) 𝑦 ) · 𝑥 ) = ( 𝑟 · ( 𝑦 · 𝑥 ) ) ∧ ( ( 1r ‘ 𝑆 ) · 𝑥 ) = 𝑥 ) ) ) ↔ ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ∧ ∀ 𝑥 ∈ 𝑉 ( ( 1 · 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝐾 ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) ) ) ) )
145 6 17 144 3bitri ⊢ ( 𝑊 ∈ ℂMod ↔ ( ( 𝑊 ∈ Grp ∧ 𝑆 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ∧ ∀ 𝑥 ∈ 𝑉 ( ( 1 · 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝑦 · 𝑥 ) ∈ 𝑉 ∧ ∀ 𝑧 ∈ 𝑉 ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) ∧ ∀ 𝑧 ∈ 𝐾 ( ( ( 𝑧 + 𝑦 ) · 𝑥 ) = ( ( 𝑧 · 𝑥 ) + ( 𝑦 · 𝑥 ) ) ∧ ( ( 𝑧 · 𝑦 ) · 𝑥 ) = ( 𝑧 · ( 𝑦 · 𝑥 ) ) ) ) ) ) )