Metamath Proof Explorer

Theorem scmatmulcl

Description: The product of two scalar matrices is a scalar matrix. (Contributed by AV, 21-Aug-2019) (Revised by AV, 19-Dec-2019)

Ref Expression
Hypotheses scmatid.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
scmatid.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
scmatid.e ⊢ 𝐸 = ( Base ‘ 𝑅 )
scmatid.0 ⊢ 0 = ( 0g ‘ 𝑅 )
scmatid.s ⊢ 𝑆 = ( 𝑁 ScMat 𝑅 )
Assertion scmatmulcl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ) → ( 𝑋 ( .r ‘ 𝐴 ) 𝑌 ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 scmatid.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 scmatid.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 scmatid.e ⊢ 𝐸 = ( Base ‘ 𝑅 )
4 scmatid.0 ⊢ 0 = ( 0g ‘ 𝑅 )
5 scmatid.s ⊢ 𝑆 = ( 𝑁 ScMat 𝑅 )
6 eqid ⊢ ( 1r ‘ 𝐴 ) = ( 1r ‘ 𝐴 )
7 eqid ⊢ ( ·𝑠 ‘ 𝐴 ) = ( ·𝑠 ‘ 𝐴 )
8 3 1 2 6 7 5 scmatel ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑋 ∈ 𝑆 ↔ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑐 ∈ 𝐸 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) ) )
9 3 1 2 6 7 5 scmatel ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑌 ∈ 𝑆 ↔ ( 𝑌 ∈ 𝐵 ∧ ∃ 𝑑 ∈ 𝐸 𝑌 = ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) ) )
10 oveq12 ⊢ ( ( 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∧ 𝑌 = ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) → ( 𝑋 ( .r ‘ 𝐴 ) 𝑌 ) = ( ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ( .r ‘ 𝐴 ) ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) )
11 10 adantll ⊢ ( ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐸 ) ∧ 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) ∧ 𝑌 = ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) → ( 𝑋 ( .r ‘ 𝐴 ) 𝑌 ) = ( ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ( .r ‘ 𝐴 ) ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) )
12 simp-4l ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐸 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
13 simplr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑋 ∈ 𝐵 ) → 𝑑 ∈ 𝐸 )
14 13 anim1ci ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐸 ) → ( 𝑐 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ) )
15 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
16 eqid ⊢ ( .r ‘ 𝐴 ) = ( .r ‘ 𝐴 )
17 1 3 4 6 7 15 16 scmatscmiddistr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑐 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ) ) → ( ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ( .r ‘ 𝐴 ) ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) = ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) )
18 12 14 17 syl2anc ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐸 ) → ( ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ( .r ‘ 𝐴 ) ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) = ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) )
19 simpl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
20 simplr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) → 𝑅 ∈ Ring )
21 simprr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) → 𝑐 ∈ 𝐸 )
22 simpl ⊢ ( ( 𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) → 𝑑 ∈ 𝐸 )
23 22 adantl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) → 𝑑 ∈ 𝐸 )
24 3 15 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑐 ∈ 𝐸 ∧ 𝑑 ∈ 𝐸 ) → ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ∈ 𝐸 )
25 20 21 23 24 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) → ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ∈ 𝐸 )
26 1 matring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
27 2 6 ringidcl ⊢ ( 𝐴 ∈ Ring → ( 1r ‘ 𝐴 ) ∈ 𝐵 )
28 26 27 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝐴 ) ∈ 𝐵 )
29 28 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) → ( 1r ‘ 𝐴 ) ∈ 𝐵 )
30 3 1 2 7 matvscl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ∈ 𝐸 ∧ ( 1r ‘ 𝐴 ) ∈ 𝐵 ) ) → ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∈ 𝐵 )
31 19 25 29 30 syl12anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) → ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∈ 𝐵 )
32 oveq1 ⊢ ( 𝑒 = ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) → ( 𝑒 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) = ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) )
33 32 eqeq2d ⊢ ( 𝑒 = ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) → ( ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) = ( 𝑒 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ↔ ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) = ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) )
34 33 adantl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) ∧ 𝑒 = ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ) → ( ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) = ( 𝑒 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ↔ ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) = ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) )
35 eqidd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) → ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) = ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) )
36 25 34 35 rspcedvd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) → ∃ 𝑒 ∈ 𝐸 ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) = ( 𝑒 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) )
37 3 1 2 6 7 5 scmatel ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∈ 𝑆 ↔ ( ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∈ 𝐵 ∧ ∃ 𝑒 ∈ 𝐸 ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) = ( 𝑒 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) ) )
38 37 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) → ( ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∈ 𝑆 ↔ ( ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∈ 𝐵 ∧ ∃ 𝑒 ∈ 𝐸 ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) = ( 𝑒 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) ) )
39 31 36 38 mpbir2and ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑑 ∈ 𝐸 ∧ 𝑐 ∈ 𝐸 ) ) → ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∈ 𝑆 )
40 39 exp32 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑑 ∈ 𝐸 → ( 𝑐 ∈ 𝐸 → ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∈ 𝑆 ) ) )
41 40 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) → ( 𝑑 ∈ 𝐸 → ( 𝑐 ∈ 𝐸 → ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∈ 𝑆 ) ) )
42 41 imp ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑑 ∈ 𝐸 ) → ( 𝑐 ∈ 𝐸 → ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∈ 𝑆 ) )
43 42 adantr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝑐 ∈ 𝐸 → ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∈ 𝑆 ) )
44 43 imp ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐸 ) → ( ( 𝑐 ( .r ‘ 𝑅 ) 𝑑 ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∈ 𝑆 )
45 18 44 eqeltrd ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐸 ) → ( ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ( .r ‘ 𝐴 ) ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) ∈ 𝑆 )
46 45 adantr ⊢ ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐸 ) ∧ 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) → ( ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ( .r ‘ 𝐴 ) ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) ∈ 𝑆 )
47 46 adantr ⊢ ( ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐸 ) ∧ 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) ∧ 𝑌 = ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) → ( ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ( .r ‘ 𝐴 ) ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) ∈ 𝑆 )
48 11 47 eqeltrd ⊢ ( ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐸 ) ∧ 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) ∧ 𝑌 = ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) → ( 𝑋 ( .r ‘ 𝐴 ) 𝑌 ) ∈ 𝑆 )
49 48 exp31 ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐸 ) → ( 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) → ( 𝑌 = ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) → ( 𝑋 ( .r ‘ 𝐴 ) 𝑌 ) ∈ 𝑆 ) ) )
50 49 rexlimdva ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑑 ∈ 𝐸 ) ∧ 𝑋 ∈ 𝐵 ) → ( ∃ 𝑐 ∈ 𝐸 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) → ( 𝑌 = ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) → ( 𝑋 ( .r ‘ 𝐴 ) 𝑌 ) ∈ 𝑆 ) ) )
51 50 expimpd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑑 ∈ 𝐸 ) → ( ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑐 ∈ 𝐸 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) → ( 𝑌 = ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) → ( 𝑋 ( .r ‘ 𝐴 ) 𝑌 ) ∈ 𝑆 ) ) )
52 51 com23 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑑 ∈ 𝐸 ) → ( 𝑌 = ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) → ( ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑐 ∈ 𝐸 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) → ( 𝑋 ( .r ‘ 𝐴 ) 𝑌 ) ∈ 𝑆 ) ) )
53 52 rexlimdva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) → ( ∃ 𝑑 ∈ 𝐸 𝑌 = ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) → ( ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑐 ∈ 𝐸 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) → ( 𝑋 ( .r ‘ 𝐴 ) 𝑌 ) ∈ 𝑆 ) ) )
54 53 expimpd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 𝑌 ∈ 𝐵 ∧ ∃ 𝑑 ∈ 𝐸 𝑌 = ( 𝑑 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) → ( ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑐 ∈ 𝐸 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) → ( 𝑋 ( .r ‘ 𝐴 ) 𝑌 ) ∈ 𝑆 ) ) )
55 9 54 sylbid ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑌 ∈ 𝑆 → ( ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑐 ∈ 𝐸 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) → ( 𝑋 ( .r ‘ 𝐴 ) 𝑌 ) ∈ 𝑆 ) ) )
56 55 com23 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑐 ∈ 𝐸 𝑋 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) → ( 𝑌 ∈ 𝑆 → ( 𝑋 ( .r ‘ 𝐴 ) 𝑌 ) ∈ 𝑆 ) ) )
57 8 56 sylbid ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑋 ∈ 𝑆 → ( 𝑌 ∈ 𝑆 → ( 𝑋 ( .r ‘ 𝐴 ) 𝑌 ) ∈ 𝑆 ) ) )
58 57 imp32 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ) → ( 𝑋 ( .r ‘ 𝐴 ) 𝑌 ) ∈ 𝑆 )