Theorem psrlmod

Description: The ring of power series is a left module. (Contributed by Mario Carneiro, 29-Dec-2014)

	Ref	Expression
Hypotheses	psrring.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
	psrring.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	psrring.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
Assertion	psrlmod	⊢ ( 𝜑 → 𝑆 ∈ LMod )

Proof

Step	Hyp	Ref	Expression
1		psrring.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2		psrring.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
3		psrring.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
4		eqidd	⊢ ( 𝜑 → ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 ) )
5		eqidd	⊢ ( 𝜑 → ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 ) )
6	1 2 3	psrsca	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑆 ) )
7		eqidd	⊢ ( 𝜑 → ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ 𝑆 ) )
8		eqidd	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) )
9		eqidd	⊢ ( 𝜑 → ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 ) )
10		eqidd	⊢ ( 𝜑 → ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 ) )
11		eqidd	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 ) )
12		ringgrp	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
13	3 12	syl	⊢ ( 𝜑 → 𝑅 ∈ Grp )
14	1 2 13	psrgrp	⊢ ( 𝜑 → 𝑆 ∈ Grp )
15		eqid	⊢ ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ 𝑆 )
16		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
17		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
18	3	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → 𝑅 ∈ Ring )
19		simp2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
20		simp3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → 𝑦 ∈ ( Base ‘ 𝑆 ) )
21	1 15 16 17 18 19 20	psrvscacl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ∈ ( Base ‘ 𝑆 ) )
22		ovex	⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
23	22	rabex	⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∈ V
24	23	a1i	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∈ V )
25		simpr1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
26		fconst6g	⊢ ( 𝑥 ∈ ( Base ‘ 𝑅 ) → ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
27	25 26	syl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
28		eqid	⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
29		simpr2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑆 ) )
30	1 16 28 17 29	psrelbas	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑦 : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
31		simpr3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑧 ∈ ( Base ‘ 𝑆 ) )
32	1 16 28 17 31	psrelbas	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑧 : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
33	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑅 ∈ Ring )
34		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
35		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
36	16 34 35	ringdi	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑟 ∈ ( Base ‘ 𝑅 ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ∧ 𝑡 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑟 ( .r ‘ 𝑅 ) ( 𝑠 ( +g ‘ 𝑅 ) 𝑡 ) ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑠 ) ( +g ‘ 𝑅 ) ( 𝑟 ( .r ‘ 𝑅 ) 𝑡 ) ) )
37	33 36	sylan	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ 𝑅 ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ∧ 𝑡 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑟 ( .r ‘ 𝑅 ) ( 𝑠 ( +g ‘ 𝑅 ) 𝑡 ) ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑠 ) ( +g ‘ 𝑅 ) ( 𝑟 ( .r ‘ 𝑅 ) 𝑡 ) ) )
38	24 27 30 32 37	caofdi	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) ( 𝑦 ∘f ( +g ‘ 𝑅 ) 𝑧 ) ) = ( ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑦 ) ∘f ( +g ‘ 𝑅 ) ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) ) )
39		eqid	⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
40	1 17 34 39 29 31	psradd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑦 ( +g ‘ 𝑆 ) 𝑧 ) = ( 𝑦 ∘f ( +g ‘ 𝑅 ) 𝑧 ) )
41	40	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) ( 𝑦 ( +g ‘ 𝑆 ) 𝑧 ) ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) ( 𝑦 ∘f ( +g ‘ 𝑅 ) 𝑧 ) ) )
42	1 15 16 17 35 28 25 29	psrvsca	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑦 ) )
43	1 15 16 17 35 28 25 31	psrvsca	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) )
44	42 43	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ∘f ( +g ‘ 𝑅 ) ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ) = ( ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑦 ) ∘f ( +g ‘ 𝑅 ) ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) ) )
45	38 41 44	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) ( 𝑦 ( +g ‘ 𝑆 ) 𝑧 ) ) = ( ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ∘f ( +g ‘ 𝑅 ) ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ) )
46	13	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑅 ∈ Grp )
47	1 17 39 46 29 31	psraddcl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑦 ( +g ‘ 𝑆 ) 𝑧 ) ∈ ( Base ‘ 𝑆 ) )
48	1 15 16 17 35 28 25 47	psrvsca	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑆 ) ( 𝑦 ( +g ‘ 𝑆 ) 𝑧 ) ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) ( 𝑦 ( +g ‘ 𝑆 ) 𝑧 ) ) )
49	21	3adant3r3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ∈ ( Base ‘ 𝑆 ) )
50	1 15 16 17 33 25 31	psrvscacl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ∈ ( Base ‘ 𝑆 ) )
51	1 17 34 39 49 50	psradd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ( +g ‘ 𝑆 ) ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ) = ( ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ∘f ( +g ‘ 𝑅 ) ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ) )
52	45 48 51	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑆 ) ( 𝑦 ( +g ‘ 𝑆 ) 𝑧 ) ) = ( ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) ( +g ‘ 𝑆 ) ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ) )
53		simpr1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
54		simpr3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑧 ∈ ( Base ‘ 𝑆 ) )
55	1 15 16 17 35 28 53 54	psrvsca	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) )
56		simpr2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
57	1 15 16 17 35 28 56 54	psrvsca	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑦 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑦 } ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) )
58	55 57	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ∘f ( +g ‘ 𝑅 ) ( 𝑦 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ) = ( ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) ∘f ( +g ‘ 𝑅 ) ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑦 } ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) ) )
59	23	a1i	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∈ V )
60	1 16 28 17 54	psrelbas	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑧 : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
61	53 26	syl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
62		fconst6g	⊢ ( 𝑦 ∈ ( Base ‘ 𝑅 ) → ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑦 } ) : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
63	56 62	syl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑦 } ) : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
64	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑅 ∈ Ring )
65	16 34 35	ringdir	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑟 ∈ ( Base ‘ 𝑅 ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ∧ 𝑡 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑟 ( +g ‘ 𝑅 ) 𝑠 ) ( .r ‘ 𝑅 ) 𝑡 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑡 ) ( +g ‘ 𝑅 ) ( 𝑠 ( .r ‘ 𝑅 ) 𝑡 ) ) )
66	64 65	sylan	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ 𝑅 ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ∧ 𝑡 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑟 ( +g ‘ 𝑅 ) 𝑠 ) ( .r ‘ 𝑅 ) 𝑡 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑡 ) ( +g ‘ 𝑅 ) ( 𝑠 ( .r ‘ 𝑅 ) 𝑡 ) ) )
67	59 60 61 63 66	caofdir	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( +g ‘ 𝑅 ) ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑦 } ) ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) = ( ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) ∘f ( +g ‘ 𝑅 ) ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑦 } ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) ) )
68	59 53 56	ofc12	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( +g ‘ 𝑅 ) ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑦 } ) ) = ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) } ) )
69	68	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( +g ‘ 𝑅 ) ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑦 } ) ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) } ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) )
70	58 67 69	3eqtr2rd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) } ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) = ( ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ∘f ( +g ‘ 𝑅 ) ( 𝑦 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ) )
71	16 34	ringacl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
72	64 53 56 71	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
73	1 15 16 17 35 28 72 54	psrvsca	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ( ·𝑠 ‘ 𝑆 ) 𝑧 ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) } ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) )
74	1 15 16 17 64 53 54	psrvscacl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ∈ ( Base ‘ 𝑆 ) )
75	1 15 16 17 64 56 54	psrvscacl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑦 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ∈ ( Base ‘ 𝑆 ) )
76	1 17 34 39 74 75	psradd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ( +g ‘ 𝑆 ) ( 𝑦 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ) = ( ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ∘f ( +g ‘ 𝑅 ) ( 𝑦 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ) )
77	70 73 76	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ( ·𝑠 ‘ 𝑆 ) 𝑧 ) = ( ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ( +g ‘ 𝑆 ) ( 𝑦 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ) )
78	57	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) ( 𝑦 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑦 } ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) ) )
79	16 35	ringass	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑟 ∈ ( Base ‘ 𝑅 ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ∧ 𝑡 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑠 ) ( .r ‘ 𝑅 ) 𝑡 ) = ( 𝑟 ( .r ‘ 𝑅 ) ( 𝑠 ( .r ‘ 𝑅 ) 𝑡 ) ) )
80	64 79	sylan	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ 𝑅 ) ∧ 𝑠 ∈ ( Base ‘ 𝑅 ) ∧ 𝑡 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑠 ) ( .r ‘ 𝑅 ) 𝑡 ) = ( 𝑟 ( .r ‘ 𝑅 ) ( 𝑠 ( .r ‘ 𝑅 ) 𝑡 ) ) )
81	59 61 63 60 80	caofass	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑦 } ) ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑦 } ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) ) )
82	59 53 56	ofc12	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑦 } ) ) = ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) } ) )
83	82	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑦 } ) ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) } ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) )
84	78 81 83	3eqtr2rd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) } ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) ( 𝑦 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ) )
85	16 35	ringcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
86	64 53 56 85	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
87	1 15 16 17 35 28 86 54	psrvsca	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( ·𝑠 ‘ 𝑆 ) 𝑧 ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) } ) ∘f ( .r ‘ 𝑅 ) 𝑧 ) )
88	1 15 16 17 35 28 53 75	psrvsca	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑆 ) ( 𝑦 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r ‘ 𝑅 ) ( 𝑦 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ) )
89	84 87 88	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( ·𝑠 ‘ 𝑆 ) 𝑧 ) = ( 𝑥 ( ·𝑠 ‘ 𝑆 ) ( 𝑦 ( ·𝑠 ‘ 𝑆 ) 𝑧 ) ) )
90	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → 𝑅 ∈ Ring )
91		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
92	16 91	ringidcl	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
93	90 92	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
94		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → 𝑥 ∈ ( Base ‘ 𝑆 ) )
95	1 15 16 17 35 28 93 94	psrvsca	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑆 ) 𝑥 ) = ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { ( 1r ‘ 𝑅 ) } ) ∘f ( .r ‘ 𝑅 ) 𝑥 ) )
96	23	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∈ V )
97	1 16 28 17 94	psrelbas	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → 𝑥 : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
98	16 35 91	ringlidm	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑟 ) = 𝑟 )
99	90 98	sylan	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑟 ) = 𝑟 )
100	96 97 93 99	caofid0l	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → ( ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } × { ( 1r ‘ 𝑅 ) } ) ∘f ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 )
101	95 100	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑆 ) 𝑥 ) = 𝑥 )
102	4 5 6 7 8 9 10 11 3 14 21 52 77 89 101	islmodd	⊢ ( 𝜑 → 𝑆 ∈ LMod )