Theorem prdslmodd

Description: The product of a family of left modules is a left module. (Contributed by Stefan O'Rear, 10-Jan-2015)

	Ref	Expression
Hypotheses	prdslmodd.y	⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
	prdslmodd.s	⊢ ( 𝜑 → 𝑆 ∈ Ring )
	prdslmodd.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	prdslmodd.rm	⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ LMod )
	prdslmodd.rs	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) = 𝑆 )
Assertion	prdslmodd	⊢ ( 𝜑 → 𝑌 ∈ LMod )

Proof

Step	Hyp	Ref	Expression
1		prdslmodd.y	⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
2		prdslmodd.s	⊢ ( 𝜑 → 𝑆 ∈ Ring )
3		prdslmodd.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
4		prdslmodd.rm	⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ LMod )
5		prdslmodd.rs	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) = 𝑆 )
6		eqidd	⊢ ( 𝜑 → ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 ) )
7		eqidd	⊢ ( 𝜑 → ( +g ‘ 𝑌 ) = ( +g ‘ 𝑌 ) )
8	4 3	fexd	⊢ ( 𝜑 → 𝑅 ∈ V )
9	1 2 8	prdssca	⊢ ( 𝜑 → 𝑆 = ( Scalar ‘ 𝑌 ) )
10		eqidd	⊢ ( 𝜑 → ( ·𝑠 ‘ 𝑌 ) = ( ·𝑠 ‘ 𝑌 ) )
11		eqidd	⊢ ( 𝜑 → ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 ) )
12		eqidd	⊢ ( 𝜑 → ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 ) )
13		eqidd	⊢ ( 𝜑 → ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 ) )
14		eqidd	⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 ) )
15		lmodgrp	⊢ ( 𝑎 ∈ LMod → 𝑎 ∈ Grp )
16	15	ssriv	⊢ LMod ⊆ Grp
17		fss	⊢ ( ( 𝑅 : 𝐼 ⟶ LMod ∧ LMod ⊆ Grp ) → 𝑅 : 𝐼 ⟶ Grp )
18	4 16 17	sylancl	⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Grp )
19	1 3 2 18	prdsgrpd	⊢ ( 𝜑 → 𝑌 ∈ Grp )
20		eqid	⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
21		eqid	⊢ ( ·𝑠 ‘ 𝑌 ) = ( ·𝑠 ‘ 𝑌 )
22		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
23	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑆 ∈ Ring )
24	3	elexd	⊢ ( 𝜑 → 𝐼 ∈ V )
25	24	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) ) → 𝐼 ∈ V )
26	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑅 : 𝐼 ⟶ LMod )
27		simprl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑎 ∈ ( Base ‘ 𝑆 ) )
28		simprr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑏 ∈ ( Base ‘ 𝑌 ) )
29	5	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) = 𝑆 )
30	1 20 21 22 23 25 26 27 28 29	prdsvscacl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑏 ) ∈ ( Base ‘ 𝑌 ) )
31	30	3impb	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑏 ) ∈ ( Base ‘ 𝑌 ) )
32	4	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑦 ) ∈ LMod )
33	32	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑦 ) ∈ LMod )
34		simplr1	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑎 ∈ ( Base ‘ 𝑆 ) )
35	5	fveq2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) = ( Base ‘ 𝑆 ) )
36	35	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) = ( Base ‘ 𝑆 ) )
37	34 36	eleqtrrd	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑎 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) )
38	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑆 ∈ Ring )
39	24	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝐼 ∈ V )
40	4	ffnd	⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
41	40	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑅 Fn 𝐼 )
42		simplr2	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑏 ∈ ( Base ‘ 𝑌 ) )
43		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑦 ∈ 𝐼 )
44	1 20 38 39 41 42 43	prdsbasprj	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑏 ‘ 𝑦 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) )
45		simplr3	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑐 ∈ ( Base ‘ 𝑌 ) )
46	1 20 38 39 41 45 43	prdsbasprj	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑐 ‘ 𝑦 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) )
47		eqid	⊢ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) = ( Base ‘ ( 𝑅 ‘ 𝑦 ) )
48		eqid	⊢ ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) = ( +g ‘ ( 𝑅 ‘ 𝑦 ) )
49		eqid	⊢ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) = ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) )
50		eqid	⊢ ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) = ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) )
51		eqid	⊢ ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) = ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) )
52	47 48 49 50 51	lmodvsdi	⊢ ( ( ( 𝑅 ‘ 𝑦 ) ∈ LMod ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) ∧ ( 𝑏 ‘ 𝑦 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ∧ ( 𝑐 ‘ 𝑦 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) → ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑏 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ) = ( ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑏 ‘ 𝑦 ) ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ) )
53	33 37 44 46 52	syl13anc	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑏 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ) = ( ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑏 ‘ 𝑦 ) ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ) )
54		eqid	⊢ ( +g ‘ 𝑌 ) = ( +g ‘ 𝑌 )
55	1 20 38 39 41 42 45 54 43	prdsplusgfval	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑏 ( +g ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) = ( ( 𝑏 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) )
56	55	oveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑏 ( +g ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ) = ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑏 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ) )
57	1 20 21 22 38 39 41 34 42 43	prdsvscafval	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑏 ) ‘ 𝑦 ) = ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑏 ‘ 𝑦 ) ) )
58	1 20 21 22 38 39 41 34 45 43	prdsvscafval	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) = ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) )
59	57 58	oveq12d	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑏 ) ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ) = ( ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑏 ‘ 𝑦 ) ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ) )
60	53 56 59	3eqtr4d	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑏 ( +g ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ) = ( ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑏 ) ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ) )
61	60	mpteq2dva	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑦 ∈ 𝐼 ↦ ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑏 ( +g ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝐼 ↦ ( ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑏 ) ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ) ) )
62	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑆 ∈ Ring )
63	24	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝐼 ∈ V )
64	40	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑅 Fn 𝐼 )
65		simpr1	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑎 ∈ ( Base ‘ 𝑆 ) )
66	19	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑌 ∈ Grp )
67		simpr2	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑏 ∈ ( Base ‘ 𝑌 ) )
68		simpr3	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑐 ∈ ( Base ‘ 𝑌 ) )
69	20 54	grpcl	⊢ ( ( 𝑌 ∈ Grp ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) → ( 𝑏 ( +g ‘ 𝑌 ) 𝑐 ) ∈ ( Base ‘ 𝑌 ) )
70	66 67 68 69	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑏 ( +g ‘ 𝑌 ) 𝑐 ) ∈ ( Base ‘ 𝑌 ) )
71	1 20 21 22 62 63 64 65 70	prdsvscaval	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑌 ) ( 𝑏 ( +g ‘ 𝑌 ) 𝑐 ) ) = ( 𝑦 ∈ 𝐼 ↦ ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑏 ( +g ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ) ) )
72	30	3adantr3	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑏 ) ∈ ( Base ‘ 𝑌 ) )
73	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑆 ∈ Ring )
74	24	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝐼 ∈ V )
75	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑅 : 𝐼 ⟶ LMod )
76		simprl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑎 ∈ ( Base ‘ 𝑆 ) )
77		simprr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑐 ∈ ( Base ‘ 𝑌 ) )
78	5	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) = 𝑆 )
79	1 20 21 22 73 74 75 76 77 78	prdsvscacl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ∈ ( Base ‘ 𝑌 ) )
80	79	3adantr2	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ∈ ( Base ‘ 𝑌 ) )
81	1 20 62 63 64 72 80 54	prdsplusgval	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑏 ) ( +g ‘ 𝑌 ) ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ) = ( 𝑦 ∈ 𝐼 ↦ ( ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑏 ) ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ) ) )
82	61 71 81	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑌 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑌 ) ( 𝑏 ( +g ‘ 𝑌 ) 𝑐 ) ) = ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑏 ) ( +g ‘ 𝑌 ) ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ) )
83	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑆 ∈ Ring )
84	24	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝐼 ∈ V )
85	40	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑅 Fn 𝐼 )
86		simplr1	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑎 ∈ ( Base ‘ 𝑆 ) )
87		simplr3	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑐 ∈ ( Base ‘ 𝑌 ) )
88		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑦 ∈ 𝐼 )
89	1 20 21 22 83 84 85 86 87 88	prdsvscafval	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) = ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) )
90		simplr2	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑏 ∈ ( Base ‘ 𝑆 ) )
91	1 20 21 22 83 84 85 90 87 88	prdsvscafval	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑏 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) = ( 𝑏 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) )
92	89 91	oveq12d	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑏 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ) = ( ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑏 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ) )
93	32	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑦 ) ∈ LMod )
94	35	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) = ( Base ‘ 𝑆 ) )
95	86 94	eleqtrrd	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑎 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) )
96	90 94	eleqtrrd	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑏 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) )
97	1 20 83 84 85 87 88	prdsbasprj	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑐 ‘ 𝑦 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) )
98		eqid	⊢ ( +g ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) = ( +g ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) )
99	47 48 49 50 51 98	lmodvsdir	⊢ ( ( ( 𝑅 ‘ 𝑦 ) ∈ LMod ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) ∧ 𝑏 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) ∧ ( 𝑐 ‘ 𝑦 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) → ( ( 𝑎 ( +g ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) 𝑏 ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) = ( ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑏 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ) )
100	93 95 96 97 99	syl13anc	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑎 ( +g ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) 𝑏 ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) = ( ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑏 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ) )
101	5	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) = 𝑆 )
102	101	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( +g ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) = ( +g ‘ 𝑆 ) )
103	102	oveqd	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑎 ( +g ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) 𝑏 ) = ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) )
104	103	oveq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑎 ( +g ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) 𝑏 ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) = ( ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) )
105	92 100 104	3eqtr2rd	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) = ( ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑏 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ) )
106	105	mpteq2dva	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝐼 ↦ ( ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑏 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ) ) )
107	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑆 ∈ Ring )
108	24	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝐼 ∈ V )
109	40	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑅 Fn 𝐼 )
110		simpr1	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑎 ∈ ( Base ‘ 𝑆 ) )
111		simpr2	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑏 ∈ ( Base ‘ 𝑆 ) )
112		eqid	⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
113	22 112	ringacl	⊢ ( ( 𝑆 ∈ Ring ∧ 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) ∈ ( Base ‘ 𝑆 ) )
114	107 110 111 113	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) ∈ ( Base ‘ 𝑆 ) )
115		simpr3	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑐 ∈ ( Base ‘ 𝑌 ) )
116	1 20 21 22 107 108 109 114 115	prdsvscaval	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) ( ·𝑠 ‘ 𝑌 ) 𝑐 ) = ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ) )
117	79	3adantr2	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ∈ ( Base ‘ 𝑌 ) )
118	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → 𝑅 : 𝐼 ⟶ LMod )
119	1 20 21 22 107 108 118 111 115 101	prdsvscacl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑏 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ∈ ( Base ‘ 𝑌 ) )
120	1 20 107 108 109 117 119 54	prdsplusgval	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ( +g ‘ 𝑌 ) ( 𝑏 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ) = ( 𝑦 ∈ 𝐼 ↦ ( ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ( +g ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑏 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ) ) )
121	106 116 120	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) ( ·𝑠 ‘ 𝑌 ) 𝑐 ) = ( ( 𝑎 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ( +g ‘ 𝑌 ) ( 𝑏 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ) )
122	91	oveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑏 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ) = ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑏 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ) )
123		eqid	⊢ ( .r ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) = ( .r ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) )
124	47 49 50 51 123	lmodvsass	⊢ ( ( ( 𝑅 ‘ 𝑦 ) ∈ LMod ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) ∧ 𝑏 ∈ ( Base ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) ∧ ( 𝑐 ‘ 𝑦 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) ) → ( ( 𝑎 ( .r ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) 𝑏 ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) = ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑏 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ) )
125	93 95 96 97 124	syl13anc	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑎 ( .r ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) 𝑏 ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) = ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑏 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ) )
126	101	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( .r ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) = ( .r ‘ 𝑆 ) )
127	126	oveqd	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑎 ( .r ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) 𝑏 ) = ( 𝑎 ( .r ‘ 𝑆 ) 𝑏 ) )
128	127	oveq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑎 ( .r ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) 𝑏 ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) = ( ( 𝑎 ( .r ‘ 𝑆 ) 𝑏 ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) )
129	122 125 128	3eqtr2rd	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑎 ( .r ‘ 𝑆 ) 𝑏 ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) = ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑏 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ) )
130	129	mpteq2dva	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑎 ( .r ‘ 𝑆 ) 𝑏 ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝐼 ↦ ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑏 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ) ) )
131		eqid	⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
132	22 131	ringcl	⊢ ( ( 𝑆 ∈ Ring ∧ 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑎 ( .r ‘ 𝑆 ) 𝑏 ) ∈ ( Base ‘ 𝑆 ) )
133	107 110 111 132	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑎 ( .r ‘ 𝑆 ) 𝑏 ) ∈ ( Base ‘ 𝑆 ) )
134	1 20 21 22 107 108 109 133 115	prdsvscaval	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( ( 𝑎 ( .r ‘ 𝑆 ) 𝑏 ) ( ·𝑠 ‘ 𝑌 ) 𝑐 ) = ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑎 ( .r ‘ 𝑆 ) 𝑏 ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑐 ‘ 𝑦 ) ) ) )
135	1 20 21 22 107 108 109 110 119	prdsvscaval	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑌 ) ( 𝑏 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ) = ( 𝑦 ∈ 𝐼 ↦ ( 𝑎 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( ( 𝑏 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ‘ 𝑦 ) ) ) )
136	130 134 135	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑌 ) ) ) → ( ( 𝑎 ( .r ‘ 𝑆 ) 𝑏 ) ( ·𝑠 ‘ 𝑌 ) 𝑐 ) = ( 𝑎 ( ·𝑠 ‘ 𝑌 ) ( 𝑏 ( ·𝑠 ‘ 𝑌 ) 𝑐 ) ) )
137	5	fveq2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ( 1r ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) = ( 1r ‘ 𝑆 ) )
138	137	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 1r ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) = ( 1r ‘ 𝑆 ) )
139	138	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 1r ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑦 ) ) = ( ( 1r ‘ 𝑆 ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑦 ) ) )
140	32	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑦 ) ∈ LMod )
141	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑆 ∈ Ring )
142	24	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝐼 ∈ V )
143	40	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑅 Fn 𝐼 )
144		simplr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑎 ∈ ( Base ‘ 𝑌 ) )
145		simpr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑦 ∈ 𝐼 )
146	1 20 141 142 143 144 145	prdsbasprj	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑎 ‘ 𝑦 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) )
147		eqid	⊢ ( 1r ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) = ( 1r ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) )
148	47 49 50 147	lmodvs1	⊢ ( ( ( 𝑅 ‘ 𝑦 ) ∈ LMod ∧ ( 𝑎 ‘ 𝑦 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) → ( ( 1r ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑦 ) ) = ( 𝑎 ‘ 𝑦 ) )
149	140 146 148	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 1r ‘ ( Scalar ‘ ( 𝑅 ‘ 𝑦 ) ) ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑦 ) ) = ( 𝑎 ‘ 𝑦 ) )
150	139 149	eqtr3d	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 1r ‘ 𝑆 ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑦 ) ) = ( 𝑎 ‘ 𝑦 ) )
151	150	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) → ( 𝑦 ∈ 𝐼 ↦ ( ( 1r ‘ 𝑆 ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝐼 ↦ ( 𝑎 ‘ 𝑦 ) ) )
152	2	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) → 𝑆 ∈ Ring )
153	24	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) → 𝐼 ∈ V )
154	40	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) → 𝑅 Fn 𝐼 )
155		eqid	⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
156	22 155	ringidcl	⊢ ( 𝑆 ∈ Ring → ( 1r ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) )
157	2 156	syl	⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) )
158	157	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) → ( 1r ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) )
159		simpr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) → 𝑎 ∈ ( Base ‘ 𝑌 ) )
160	1 20 21 22 152 153 154 158 159	prdsvscaval	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) → ( ( 1r ‘ 𝑆 ) ( ·𝑠 ‘ 𝑌 ) 𝑎 ) = ( 𝑦 ∈ 𝐼 ↦ ( ( 1r ‘ 𝑆 ) ( ·𝑠 ‘ ( 𝑅 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑦 ) ) ) )
161	1 20 152 153 154 159	prdsbasfn	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) → 𝑎 Fn 𝐼 )
162		dffn5	⊢ ( 𝑎 Fn 𝐼 ↔ 𝑎 = ( 𝑦 ∈ 𝐼 ↦ ( 𝑎 ‘ 𝑦 ) ) )
163	161 162	sylib	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) → 𝑎 = ( 𝑦 ∈ 𝐼 ↦ ( 𝑎 ‘ 𝑦 ) ) )
164	151 160 163	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ 𝑌 ) ) → ( ( 1r ‘ 𝑆 ) ( ·𝑠 ‘ 𝑌 ) 𝑎 ) = 𝑎 )
165	6 7 9 10 11 12 13 14 2 19 31 82 121 136 164	islmodd	⊢ ( 𝜑 → 𝑌 ∈ LMod )