Theorem prdslmodd 19743

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

Hypotheses

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

Assertion

Ref	Expression
prdslmodd	⊢ (𝜑 → 𝑌 ∈ LMod)

Distinct variable groups:   𝑦,𝐼   𝜑,𝑦   𝑦,𝑅   𝑦,𝑆   𝑦,𝑌

Allowed substitution hint:   𝑉(𝑦)

Proof of Theorem prdslmodd

Dummy variables 𝑎 𝑏 𝑐 are mutually distinct and distinct from all other variables.

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114  Vcvv 3496   ⊆ wss 3938   ↦ cmpt 5148   Fn wfn 6352  ⟶wf 6353  ‘cfv 6357  (class class class)co 7158  Basecbs 16485  +_gcplusg 16567  ._rcmulr 16568  Scalarcsca 16570   ·_𝑠 cvsca 16571  X_scprds 16721  Grpcgrp 18105  1_rcur 19253  Ringcrg 19299  LModclmod 19636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-rep 5192  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-cnex 10595  ax-resscn 10596  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-addrcl 10600  ax-mulcl 10601  ax-mulrcl 10602  ax-mulcom 10603  ax-addass 10604  ax-mulass 10605  ax-distr 10606  ax-i2m1 10607  ax-1ne0 10608  ax-1rid 10609  ax-rnegex 10610  ax-rrecex 10611  ax-cnre 10612  ax-pre-lttri 10613  ax-pre-lttrn 10614  ax-pre-ltadd 10615  ax-pre-mulgt0 10616

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-nel 3126  df-ral 3145  df-rex 3146  df-reu 3147  df-rmo 3148  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-int 4879  df-iun 4923  df-br 5069  df-opab 5131  df-mpt 5149  df-tr 5175  df-id 5462  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-we 5518  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-pred 6150  df-ord 6196  df-on 6197  df-lim 6198  df-suc 6199  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-riota 7116  df-ov 7161  df-oprab 7162  df-mpo 7163  df-om 7583  df-1st 7691  df-2nd 7692  df-wrecs 7949  df-recs 8010  df-rdg 8048  df-1o 8104  df-oadd 8108  df-er 8291  df-map 8410  df-ixp 8464  df-en 8512  df-dom 8513  df-sdom 8514  df-fin 8515  df-sup 8908  df-pnf 10679  df-mnf 10680  df-xr 10681  df-ltxr 10682  df-le 10683  df-sub 10874  df-neg 10875  df-nn 11641  df-2 11703  df-3 11704  df-4 11705  df-5 11706  df-6 11707  df-7 11708  df-8 11709  df-9 11710  df-n0 11901  df-z 11985  df-dec 12102  df-uz 12247  df-fz 12896  df-struct 16487  df-ndx 16488  df-slot 16489  df-base 16491  df-sets 16492  df-plusg 16580  df-mulr 16581  df-sca 16583  df-vsca 16584  df-ip 16585  df-tset 16586  df-ple 16587  df-ds 16589  df-hom 16591  df-cco 16592  df-0g 16717  df-prds 16723  df-mgm 17854  df-sgrp 17903  df-mnd 17914  df-grp 18108  df-minusg 18109  df-mgp 19242  df-ur 19254  df-ring 19301  df-lmod 19638

This theorem is referenced by:  pwslmod  19744  dsmmlss  20890  dsmmlmod  20891