Metamath Proof Explorer

Theorem smatvscl

Description: Closure of the scalar multiplication in the ring of scalar matrices. ( matvscl analog.) (Contributed by AV, 24-Dec-2019)

Ref Expression
Hypotheses smatvscl.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
smatvscl.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
smatvscl.s ⊢ 𝑆 = ( 𝑁 ScMat 𝑅 )
smatvscl.t ⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
Assertion smatvscl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑆 ) ) → ( 𝐶 ∗ 𝑋 ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 smatvscl.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
2 smatvscl.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
3 smatvscl.s ⊢ 𝑆 = ( 𝑁 ScMat 𝑅 )
4 smatvscl.t ⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
5 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6 eqid ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
7 eqid ⊢ ( 1r ‘ 𝐴 ) = ( 1r ‘ 𝐴 )
8 5 2 6 7 4 3 scmatel ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑋 ∈ 𝑆 ↔ ( 𝑋 ∈ ( Base ‘ 𝐴 ) ∧ ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) 𝑋 = ( 𝑐 ∗ ( 1r ‘ 𝐴 ) ) ) ) )
9 oveq2 ⊢ ( 𝑋 = ( 𝑐 ∗ ( 1r ‘ 𝐴 ) ) → ( 𝐶 ∗ 𝑋 ) = ( 𝐶 ∗ ( 𝑐 ∗ ( 1r ‘ 𝐴 ) ) ) )
10 9 adantl ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑋 = ( 𝑐 ∗ ( 1r ‘ 𝐴 ) ) ) → ( 𝐶 ∗ 𝑋 ) = ( 𝐶 ∗ ( 𝑐 ∗ ( 1r ‘ 𝐴 ) ) ) )
11 2 matlmod ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ LMod )
12 11 ad3antrrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → 𝐴 ∈ LMod )
13 2 matsca2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑅 = ( Scalar ‘ 𝐴 ) )
14 13 fveq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
15 1 14 syl5eq ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐾 = ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
16 15 eleq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝐶 ∈ 𝐾 ↔ 𝐶 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ) )
17 16 biimpa ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) → 𝐶 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
18 17 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → 𝐶 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
19 13 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐴 ) ) → 𝑅 = ( Scalar ‘ 𝐴 ) )
20 19 fveq2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐴 ) ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
21 20 eleq2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑐 ∈ ( Base ‘ 𝑅 ) ↔ 𝑐 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ) )
22 21 biimpa ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → 𝑐 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
23 2 matring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
24 6 7 ringidcl ⊢ ( 𝐴 ∈ Ring → ( 1r ‘ 𝐴 ) ∈ ( Base ‘ 𝐴 ) )
25 23 24 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝐴 ) ∈ ( Base ‘ 𝐴 ) )
26 25 ad3antrrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → ( 1r ‘ 𝐴 ) ∈ ( Base ‘ 𝐴 ) )
27 eqid ⊢ ( Scalar ‘ 𝐴 ) = ( Scalar ‘ 𝐴 )
28 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝐴 ) ) = ( Base ‘ ( Scalar ‘ 𝐴 ) )
29 eqid ⊢ ( .r ‘ ( Scalar ‘ 𝐴 ) ) = ( .r ‘ ( Scalar ‘ 𝐴 ) )
30 6 27 4 28 29 lmodvsass ⊢ ( ( 𝐴 ∈ LMod ∧ ( 𝐶 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑐 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ ( 1r ‘ 𝐴 ) ∈ ( Base ‘ 𝐴 ) ) ) → ( ( 𝐶 ( .r ‘ ( Scalar ‘ 𝐴 ) ) 𝑐 ) ∗ ( 1r ‘ 𝐴 ) ) = ( 𝐶 ∗ ( 𝑐 ∗ ( 1r ‘ 𝐴 ) ) ) )
31 12 18 22 26 30 syl13anc ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐶 ( .r ‘ ( Scalar ‘ 𝐴 ) ) 𝑐 ) ∗ ( 1r ‘ 𝐴 ) ) = ( 𝐶 ∗ ( 𝑐 ∗ ( 1r ‘ 𝐴 ) ) ) )
32 31 eqcomd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐶 ∗ ( 𝑐 ∗ ( 1r ‘ 𝐴 ) ) ) = ( ( 𝐶 ( .r ‘ ( Scalar ‘ 𝐴 ) ) 𝑐 ) ∗ ( 1r ‘ 𝐴 ) ) )
33 simplll ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
34 13 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) → 𝑅 = ( Scalar ‘ 𝐴 ) )
35 34 eqcomd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) → ( Scalar ‘ 𝐴 ) = 𝑅 )
36 35 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → ( Scalar ‘ 𝐴 ) = 𝑅 )
37 36 fveq2d ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → ( .r ‘ ( Scalar ‘ 𝐴 ) ) = ( .r ‘ 𝑅 ) )
38 37 oveqd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐶 ( .r ‘ ( Scalar ‘ 𝐴 ) ) 𝑐 ) = ( 𝐶 ( .r ‘ 𝑅 ) 𝑐 ) )
39 simp-4r ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
40 simpllr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → 𝐶 ∈ 𝐾 )
41 1 eqcomi ⊢ ( Base ‘ 𝑅 ) = 𝐾
42 41 eleq2i ⊢ ( 𝑐 ∈ ( Base ‘ 𝑅 ) ↔ 𝑐 ∈ 𝐾 )
43 42 biimpi ⊢ ( 𝑐 ∈ ( Base ‘ 𝑅 ) → 𝑐 ∈ 𝐾 )
44 43 adantl ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → 𝑐 ∈ 𝐾 )
45 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
46 1 45 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ∧ 𝑐 ∈ 𝐾 ) → ( 𝐶 ( .r ‘ 𝑅 ) 𝑐 ) ∈ 𝐾 )
47 39 40 44 46 syl3anc ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐶 ( .r ‘ 𝑅 ) 𝑐 ) ∈ 𝐾 )
48 38 47 eqeltrd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐶 ( .r ‘ ( Scalar ‘ 𝐴 ) ) 𝑐 ) ∈ 𝐾 )
49 1 2 6 4 matvscl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( ( 𝐶 ( .r ‘ ( Scalar ‘ 𝐴 ) ) 𝑐 ) ∈ 𝐾 ∧ ( 1r ‘ 𝐴 ) ∈ ( Base ‘ 𝐴 ) ) ) → ( ( 𝐶 ( .r ‘ ( Scalar ‘ 𝐴 ) ) 𝑐 ) ∗ ( 1r ‘ 𝐴 ) ) ∈ ( Base ‘ 𝐴 ) )
50 33 48 26 49 syl12anc ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐶 ( .r ‘ ( Scalar ‘ 𝐴 ) ) 𝑐 ) ∗ ( 1r ‘ 𝐴 ) ) ∈ ( Base ‘ 𝐴 ) )
51 oveq1 ⊢ ( ( 𝐶 ( .r ‘ ( Scalar ‘ 𝐴 ) ) 𝑐 ) = 𝑒 → ( ( 𝐶 ( .r ‘ ( Scalar ‘ 𝐴 ) ) 𝑐 ) ∗ ( 1r ‘ 𝐴 ) ) = ( 𝑒 ∗ ( 1r ‘ 𝐴 ) ) )
52 51 eqcoms ⊢ ( 𝑒 = ( 𝐶 ( .r ‘ ( Scalar ‘ 𝐴 ) ) 𝑐 ) → ( ( 𝐶 ( .r ‘ ( Scalar ‘ 𝐴 ) ) 𝑐 ) ∗ ( 1r ‘ 𝐴 ) ) = ( 𝑒 ∗ ( 1r ‘ 𝐴 ) ) )
53 52 adantl ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑒 = ( 𝐶 ( .r ‘ ( Scalar ‘ 𝐴 ) ) 𝑐 ) ) → ( ( 𝐶 ( .r ‘ ( Scalar ‘ 𝐴 ) ) 𝑐 ) ∗ ( 1r ‘ 𝐴 ) ) = ( 𝑒 ∗ ( 1r ‘ 𝐴 ) ) )
54 48 53 rspcedeq2vd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → ∃ 𝑒 ∈ 𝐾 ( ( 𝐶 ( .r ‘ ( Scalar ‘ 𝐴 ) ) 𝑐 ) ∗ ( 1r ‘ 𝐴 ) ) = ( 𝑒 ∗ ( 1r ‘ 𝐴 ) ) )
55 1 2 6 7 4 3 scmatel ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( ( 𝐶 ( .r ‘ ( Scalar ‘ 𝐴 ) ) 𝑐 ) ∗ ( 1r ‘ 𝐴 ) ) ∈ 𝑆 ↔ ( ( ( 𝐶 ( .r ‘ ( Scalar ‘ 𝐴 ) ) 𝑐 ) ∗ ( 1r ‘ 𝐴 ) ) ∈ ( Base ‘ 𝐴 ) ∧ ∃ 𝑒 ∈ 𝐾 ( ( 𝐶 ( .r ‘ ( Scalar ‘ 𝐴 ) ) 𝑐 ) ∗ ( 1r ‘ 𝐴 ) ) = ( 𝑒 ∗ ( 1r ‘ 𝐴 ) ) ) ) )
56 55 ad3antrrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → ( ( ( 𝐶 ( .r ‘ ( Scalar ‘ 𝐴 ) ) 𝑐 ) ∗ ( 1r ‘ 𝐴 ) ) ∈ 𝑆 ↔ ( ( ( 𝐶 ( .r ‘ ( Scalar ‘ 𝐴 ) ) 𝑐 ) ∗ ( 1r ‘ 𝐴 ) ) ∈ ( Base ‘ 𝐴 ) ∧ ∃ 𝑒 ∈ 𝐾 ( ( 𝐶 ( .r ‘ ( Scalar ‘ 𝐴 ) ) 𝑐 ) ∗ ( 1r ‘ 𝐴 ) ) = ( 𝑒 ∗ ( 1r ‘ 𝐴 ) ) ) ) )
57 50 54 56 mpbir2and ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐶 ( .r ‘ ( Scalar ‘ 𝐴 ) ) 𝑐 ) ∗ ( 1r ‘ 𝐴 ) ) ∈ 𝑆 )
58 32 57 eqeltrd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐶 ∗ ( 𝑐 ∗ ( 1r ‘ 𝐴 ) ) ) ∈ 𝑆 )
59 58 adantr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑋 = ( 𝑐 ∗ ( 1r ‘ 𝐴 ) ) ) → ( 𝐶 ∗ ( 𝑐 ∗ ( 1r ‘ 𝐴 ) ) ) ∈ 𝑆 )
60 10 59 eqeltrd ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑋 = ( 𝑐 ∗ ( 1r ‘ 𝐴 ) ) ) → ( 𝐶 ∗ 𝑋 ) ∈ 𝑆 )
61 60 rexlimdva2 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐴 ) ) → ( ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) 𝑋 = ( 𝑐 ∗ ( 1r ‘ 𝐴 ) ) → ( 𝐶 ∗ 𝑋 ) ∈ 𝑆 ) )
62 61 expimpd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) → ( ( 𝑋 ∈ ( Base ‘ 𝐴 ) ∧ ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) 𝑋 = ( 𝑐 ∗ ( 1r ‘ 𝐴 ) ) ) → ( 𝐶 ∗ 𝑋 ) ∈ 𝑆 ) )
63 62 ex ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝐶 ∈ 𝐾 → ( ( 𝑋 ∈ ( Base ‘ 𝐴 ) ∧ ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) 𝑋 = ( 𝑐 ∗ ( 1r ‘ 𝐴 ) ) ) → ( 𝐶 ∗ 𝑋 ) ∈ 𝑆 ) ) )
64 63 com23 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 𝑋 ∈ ( Base ‘ 𝐴 ) ∧ ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) 𝑋 = ( 𝑐 ∗ ( 1r ‘ 𝐴 ) ) ) → ( 𝐶 ∈ 𝐾 → ( 𝐶 ∗ 𝑋 ) ∈ 𝑆 ) ) )
65 8 64 sylbid ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑋 ∈ 𝑆 → ( 𝐶 ∈ 𝐾 → ( 𝐶 ∗ 𝑋 ) ∈ 𝑆 ) ) )
66 65 com23 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝐶 ∈ 𝐾 → ( 𝑋 ∈ 𝑆 → ( 𝐶 ∗ 𝑋 ) ∈ 𝑆 ) ) )
67 66 imp32 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑆 ) ) → ( 𝐶 ∗ 𝑋 ) ∈ 𝑆 )