Theorem frlmphl 20988

Description: Conditions for a free module to be a pre-Hilbert space. (Contributed by Thierry Arnoux, 21-Jun-2019.) (Proof shortened by AV, 21-Jul-2019.)

Hypotheses

Ref	Expression
frlmphl.y	⊢ 𝑌 = (𝑅 freeLMod 𝐼)
frlmphl.b	⊢ 𝐵 = (Base‘𝑅)
frlmphl.t	⊢ · = (.r‘𝑅)
frlmphl.v	⊢ 𝑉 = (Base‘𝑌)
frlmphl.j	⊢ , = (·𝑖‘𝑌)
frlmphl.o	⊢ 𝑂 = (0g‘𝑌)
frlmphl.0	⊢ 0 = (0g‘𝑅)
frlmphl.s	⊢ ∗ = (*𝑟‘𝑅)
frlmphl.f	⊢ (𝜑 → 𝑅 ∈ Field)
frlmphl.m	⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ (𝑔 , 𝑔) = 0 ) → 𝑔 = 𝑂)
frlmphl.u	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( ∗ ‘𝑥) = 𝑥)
frlmphl.i	⊢ (𝜑 → 𝐼 ∈ 𝑊)

Assertion

Ref	Expression
frlmphl	⊢ (𝜑 → 𝑌 ∈ PreHil)

Distinct variable groups:   𝐵,𝑔,𝑥   𝑔,𝐼,𝑥   𝑅,𝑔,𝑥   𝑔,𝑉,𝑥   𝑔,𝑊,𝑥   · ,𝑔,𝑥   𝑔,𝑌,𝑥   0 ,𝑔,𝑥   𝜑,𝑔,𝑥   , ,𝑔,𝑥   𝑔,𝑂   𝑥, ∗

Allowed substitution hints:   ∗ (𝑔)   𝑂(𝑥)

Proof of Theorem frlmphl

Dummy variables 𝑓 𝑒 ℎ 𝑖 𝑦 𝑧 𝑘 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		frlmphl.v	. . 3 ⊢ 𝑉 = (Base‘𝑌)
2	1	a1i 11	. 2 ⊢ (𝜑 → 𝑉 = (Base‘𝑌))
3		eqidd 2739	. 2 ⊢ (𝜑 → (+g‘𝑌) = (+g‘𝑌))
4		eqidd 2739	. 2 ⊢ (𝜑 → ( ·𝑠 ‘𝑌) = ( ·𝑠 ‘𝑌))
5		frlmphl.j	. . 3 ⊢ , = (·𝑖‘𝑌)
6	5	a1i 11	. 2 ⊢ (𝜑 → , = (·𝑖‘𝑌))
7		frlmphl.o	. . 3 ⊢ 𝑂 = (0g‘𝑌)
8	7	a1i 11	. 2 ⊢ (𝜑 → 𝑂 = (0g‘𝑌))
9		frlmphl.f	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ Field)
10		isfld 20000	. . . . 5 ⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))
11	9, 10	sylib 217	. . . 4 ⊢ (𝜑 → (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))
12	11	simpld 495	. . 3 ⊢ (𝜑 → 𝑅 ∈ DivRing)
13		frlmphl.i	. . 3 ⊢ (𝜑 → 𝐼 ∈ 𝑊)
14		frlmphl.y	. . . 4 ⊢ 𝑌 = (𝑅 freeLMod 𝐼)
15	14	frlmsca 20960	. . 3 ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑊) → 𝑅 = (Scalar‘𝑌))
16	12, 13, 15	syl2anc 584	. 2 ⊢ (𝜑 → 𝑅 = (Scalar‘𝑌))
17		frlmphl.b	. . 3 ⊢ 𝐵 = (Base‘𝑅)
18	17	a1i 11	. 2 ⊢ (𝜑 → 𝐵 = (Base‘𝑅))
19		eqidd 2739	. 2 ⊢ (𝜑 → (+g‘𝑅) = (+g‘𝑅))
20		frlmphl.t	. . 3 ⊢ · = (.r‘𝑅)
21	20	a1i 11	. 2 ⊢ (𝜑 → · = (.r‘𝑅))
22		frlmphl.s	. . 3 ⊢ ∗ = (*𝑟‘𝑅)
23	22	a1i 11	. 2 ⊢ (𝜑 → ∗ = (*𝑟‘𝑅))
24		frlmphl.0	. . 3 ⊢ 0 = (0g‘𝑅)
25	24	a1i 11	. 2 ⊢ (𝜑 → 0 = (0g‘𝑅))
26		drngring 19998	. . . . 5 ⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring)
27	12, 26	syl 17	. . . 4 ⊢ (𝜑 → 𝑅 ∈ Ring)
28	14	frlmlmod 20956	. . . 4 ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊) → 𝑌 ∈ LMod)
29	27, 13, 28	syl2anc 584	. . 3 ⊢ (𝜑 → 𝑌 ∈ LMod)
30	16, 12	eqeltrrd 2840	. . 3 ⊢ (𝜑 → (Scalar‘𝑌) ∈ DivRing)
31		eqid 2738	. . . 4 ⊢ (Scalar‘𝑌) = (Scalar‘𝑌)
32	31	islvec 20366	. . 3 ⊢ (𝑌 ∈ LVec ↔ (𝑌 ∈ LMod ∧ (Scalar‘𝑌) ∈ DivRing))
33	29, 30, 32	sylanbrc 583	. 2 ⊢ (𝜑 → 𝑌 ∈ LVec)
34	11	simprd 496	. . 3 ⊢ (𝜑 → 𝑅 ∈ CRing)
35		frlmphl.u	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( ∗ ‘𝑥) = 𝑥)
36	17, 22, 34, 35	idsrngd 20122	. 2 ⊢ (𝜑 → 𝑅 ∈ *-Ring)
37	13	3ad2ant1 1132	. . . . 5 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝐼 ∈ 𝑊)
38	27	3ad2ant1 1132	. . . . 5 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝑅 ∈ Ring)
39		simp2 1136	. . . . 5 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝑔 ∈ 𝑉)
40		simp3 1137	. . . . 5 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ℎ ∈ 𝑉)
41	14, 17, 20, 1, 5	frlmipval 20986	. . . . 5 ⊢ (((𝐼 ∈ 𝑊 ∧ 𝑅 ∈ Ring) ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉)) → (𝑔 , ℎ) = (𝑅 Σg (𝑔 ∘f · ℎ)))
42	37, 38, 39, 40, 41	syl22anc 836	. . . 4 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑔 , ℎ) = (𝑅 Σg (𝑔 ∘f · ℎ)))
43	14, 17, 1	frlmbasmap 20966	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝑊 ∧ 𝑔 ∈ 𝑉) → 𝑔 ∈ (𝐵 ↑m 𝐼))
44	37, 39, 43	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝑔 ∈ (𝐵 ↑m 𝐼))
45		elmapi 8637	. . . . . . . 8 ⊢ (𝑔 ∈ (𝐵 ↑m 𝐼) → 𝑔:𝐼⟶𝐵)
46	44, 45	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝑔:𝐼⟶𝐵)
47	46	ffnd 6601	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝑔 Fn 𝐼)
48	14, 17, 1	frlmbasmap 20966	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝑊 ∧ ℎ ∈ 𝑉) → ℎ ∈ (𝐵 ↑m 𝐼))
49	37, 40, 48	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ℎ ∈ (𝐵 ↑m 𝐼))
50		elmapi 8637	. . . . . . . 8 ⊢ (ℎ ∈ (𝐵 ↑m 𝐼) → ℎ:𝐼⟶𝐵)
51	49, 50	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ℎ:𝐼⟶𝐵)
52	51	ffnd 6601	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ℎ Fn 𝐼)
53		inidm 4152	. . . . . 6 ⊢ (𝐼 ∩ 𝐼) = 𝐼
54		eqidd 2739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ 𝑥 ∈ 𝐼) → (𝑔‘𝑥) = (𝑔‘𝑥))
55		eqidd 2739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ 𝑥 ∈ 𝐼) → (ℎ‘𝑥) = (ℎ‘𝑥))
56	47, 52, 37, 37, 53, 54, 55	offval 7542	. . . . 5 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑔 ∘f · ℎ) = (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))))
57	56	oveq2d 7291	. . . 4 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑅 Σg (𝑔 ∘f · ℎ)) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥)))))
58	42, 57	eqtrd 2778	. . 3 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑔 , ℎ) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥)))))
59		ringcmn 19820	. . . . . 6 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
60	27, 59	syl 17	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ CMnd)
61	60	3ad2ant1 1132	. . . 4 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝑅 ∈ CMnd)
62	38	adantr 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ Ring)
63	46	ffvelrnda 6961	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ 𝑥 ∈ 𝐼) → (𝑔‘𝑥) ∈ 𝐵)
64	51	ffvelrnda 6961	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ 𝑥 ∈ 𝐼) → (ℎ‘𝑥) ∈ 𝐵)
65	17, 20	ringcl 19800	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ (𝑔‘𝑥) ∈ 𝐵 ∧ (ℎ‘𝑥) ∈ 𝐵) → ((𝑔‘𝑥) · (ℎ‘𝑥)) ∈ 𝐵)
66	62, 63, 64, 65	syl3anc 1370	. . . . 5 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ 𝑥 ∈ 𝐼) → ((𝑔‘𝑥) · (ℎ‘𝑥)) ∈ 𝐵)
67	66	fmpttd 6989	. . . 4 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))):𝐼⟶𝐵)
68		frlmphl.m	. . . . 5 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ (𝑔 , 𝑔) = 0 ) → 𝑔 = 𝑂)
69	14, 17, 20, 1, 5, 7, 24, 22, 9, 68, 35, 13	frlmphllem 20987	. . . 4 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))) finSupp 0 )
70	17, 24, 61, 37, 67, 69	gsumcl 19516	. . 3 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥)))) ∈ 𝐵)
71	58, 70	eqeltrd 2839	. 2 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑔 , ℎ) ∈ 𝐵)
72		eqid 2738	. . . 4 ⊢ (+g‘𝑅) = (+g‘𝑅)
73	60	3ad2ant1 1132	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑅 ∈ CMnd)
74	13	3ad2ant1 1132	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝐼 ∈ 𝑊)
75	27	3ad2ant1 1132	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑅 ∈ Ring)
76	75	adantr 481	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ Ring)
77		simp2 1136	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑘 ∈ 𝐵)
78	77	adantr 481	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → 𝑘 ∈ 𝐵)
79		simp31 1208	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑔 ∈ 𝑉)
80	74, 79, 43	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑔 ∈ (𝐵 ↑m 𝐼))
81	80, 45	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑔:𝐼⟶𝐵)
82	81	ffvelrnda 6961	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (𝑔‘𝑥) ∈ 𝐵)
83		simp33 1210	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑖 ∈ 𝑉)
84	14, 17, 1	frlmbasmap 20966	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝑊 ∧ 𝑖 ∈ 𝑉) → 𝑖 ∈ (𝐵 ↑m 𝐼))
85	74, 83, 84	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑖 ∈ (𝐵 ↑m 𝐼))
86		elmapi 8637	. . . . . . . 8 ⊢ (𝑖 ∈ (𝐵 ↑m 𝐼) → 𝑖:𝐼⟶𝐵)
87	85, 86	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑖:𝐼⟶𝐵)
88	87	ffvelrnda 6961	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (𝑖‘𝑥) ∈ 𝐵)
89	17, 20	ringcl 19800	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ (𝑔‘𝑥) ∈ 𝐵 ∧ (𝑖‘𝑥) ∈ 𝐵) → ((𝑔‘𝑥) · (𝑖‘𝑥)) ∈ 𝐵)
90	76, 82, 88, 89	syl3anc 1370	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → ((𝑔‘𝑥) · (𝑖‘𝑥)) ∈ 𝐵)
91	17, 20	ringcl 19800	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝑘 ∈ 𝐵 ∧ ((𝑔‘𝑥) · (𝑖‘𝑥)) ∈ 𝐵) → (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥))) ∈ 𝐵)
92	76, 78, 90, 91	syl3anc 1370	. . . 4 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥))) ∈ 𝐵)
93		simp32 1209	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ℎ ∈ 𝑉)
94	74, 93, 48	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ℎ ∈ (𝐵 ↑m 𝐼))
95	94, 50	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ℎ:𝐼⟶𝐵)
96	95	ffvelrnda 6961	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (ℎ‘𝑥) ∈ 𝐵)
97	17, 20	ringcl 19800	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ (ℎ‘𝑥) ∈ 𝐵 ∧ (𝑖‘𝑥) ∈ 𝐵) → ((ℎ‘𝑥) · (𝑖‘𝑥)) ∈ 𝐵)
98	76, 96, 88, 97	syl3anc 1370	. . . 4 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → ((ℎ‘𝑥) · (𝑖‘𝑥)) ∈ 𝐵)
99		eqidd 2739	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))) = (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))))
100		eqidd 2739	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥))))
101		fveq2 6774	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑔‘𝑥) = (𝑔‘𝑦))
102	101	oveq2d 7291	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑘 · (𝑔‘𝑥)) = (𝑘 · (𝑔‘𝑦)))
103	102	cbvmptv 5187	. . . . . . 7 ⊢ (𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) = (𝑦 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑦)))
104	103	oveq1i 7285	. . . . . 6 ⊢ ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘f · 𝑖) = ((𝑦 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑦))) ∘f · 𝑖)
105	17, 20	ringcl 19800	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Ring ∧ 𝑘 ∈ 𝐵 ∧ (𝑔‘𝑥) ∈ 𝐵) → (𝑘 · (𝑔‘𝑥)) ∈ 𝐵)
106	76, 78, 82, 105	syl3anc 1370	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (𝑘 · (𝑔‘𝑥)) ∈ 𝐵)
107	106	fmpttd 6989	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))):𝐼⟶𝐵)
108	107	ffnd 6601	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) Fn 𝐼)
109	103	fneq1i 6530	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) Fn 𝐼 ↔ (𝑦 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑦))) Fn 𝐼)
110	108, 109	sylib 217	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑦 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑦))) Fn 𝐼)
111	87	ffnd 6601	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑖 Fn 𝐼)
112		eqidd 2739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (𝑦 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑦))) = (𝑦 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑦))))
113		simpr 485	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥)
114	113	fveq2d 6778	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 = 𝑥) → (𝑔‘𝑦) = (𝑔‘𝑥))
115	114	oveq2d 7291	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 = 𝑥) → (𝑘 · (𝑔‘𝑦)) = (𝑘 · (𝑔‘𝑥)))
116		simpr 485	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼)
117		ovexd 7310	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (𝑘 · (𝑔‘𝑥)) ∈ V)
118	112, 115, 116, 117	fvmptd 6882	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → ((𝑦 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑦)))‘𝑥) = (𝑘 · (𝑔‘𝑥)))
119		eqidd 2739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (𝑖‘𝑥) = (𝑖‘𝑥))
120	110, 111, 74, 74, 53, 118, 119	offval 7542	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑦 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑦))) ∘f · 𝑖) = (𝑥 ∈ 𝐼 ↦ ((𝑘 · (𝑔‘𝑥)) · (𝑖‘𝑥))))
121	17, 20	ringass 19803	. . . . . . . . 9 ⊢ ((𝑅 ∈ Ring ∧ (𝑘 ∈ 𝐵 ∧ (𝑔‘𝑥) ∈ 𝐵 ∧ (𝑖‘𝑥) ∈ 𝐵)) → ((𝑘 · (𝑔‘𝑥)) · (𝑖‘𝑥)) = (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥))))
122	76, 78, 82, 88, 121	syl13anc 1371	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → ((𝑘 · (𝑔‘𝑥)) · (𝑖‘𝑥)) = (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥))))
123	122	mpteq2dva 5174	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑥 ∈ 𝐼 ↦ ((𝑘 · (𝑔‘𝑥)) · (𝑖‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))))
124	120, 123	eqtrd 2778	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑦 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑦))) ∘f · 𝑖) = (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))))
125	104, 124	eqtrid 2790	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘f · 𝑖) = (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))))
126		ovexd 7310	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘f · 𝑖) ∈ V)
127		funmpt 6472	. . . . . . 7 ⊢ Fun (𝑧 ∈ 𝐼 ↦ (((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥)))‘𝑧) · (𝑖‘𝑧)))
128		eqidd 2739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑧 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥)))‘𝑧) = ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥)))‘𝑧))
129		eqidd 2739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑧 ∈ 𝐼) → (𝑖‘𝑧) = (𝑖‘𝑧))
130	108, 111, 74, 74, 53, 128, 129	offval 7542	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘f · 𝑖) = (𝑧 ∈ 𝐼 ↦ (((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥)))‘𝑧) · (𝑖‘𝑧))))
131	130	funeqd 6456	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (Fun ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘f · 𝑖) ↔ Fun (𝑧 ∈ 𝐼 ↦ (((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥)))‘𝑧) · (𝑖‘𝑧)))))
132	127, 131	mpbiri 257	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → Fun ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘f · 𝑖))
133		simp3 1137	. . . . . . . . 9 ⊢ ((𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉) → 𝑖 ∈ 𝑉)
134	13, 133	anim12i 613	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝐼 ∈ 𝑊 ∧ 𝑖 ∈ 𝑉))
135	134	3adant2 1130	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝐼 ∈ 𝑊 ∧ 𝑖 ∈ 𝑉))
136	14, 24, 1	frlmbasfsupp 20965	. . . . . . 7 ⊢ ((𝐼 ∈ 𝑊 ∧ 𝑖 ∈ 𝑉) → 𝑖 finSupp 0 )
137	135, 136	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑖 finSupp 0 )
138	17, 24	ring0cl 19808	. . . . . . . 8 ⊢ (𝑅 ∈ Ring → 0 ∈ 𝐵)
139	75, 138	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 0 ∈ 𝐵)
140	17, 20, 24	ringrz 19827	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵) → (𝑦 · 0 ) = 0 )
141	75, 140	sylan 580	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑦 ∈ 𝐵) → (𝑦 · 0 ) = 0 )
142	74, 139, 107, 87, 141	suppofss2d 8021	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘f · 𝑖) supp 0 ) ⊆ (𝑖 supp 0 ))
143		fsuppsssupp 9144	. . . . . 6 ⊢ (((((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘f · 𝑖) ∈ V ∧ Fun ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘f · 𝑖)) ∧ (𝑖 finSupp 0 ∧ (((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘f · 𝑖) supp 0 ) ⊆ (𝑖 supp 0 ))) → ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘f · 𝑖) finSupp 0 )
144	126, 132, 137, 142, 143	syl22anc 836	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑥 ∈ 𝐼 ↦ (𝑘 · (𝑔‘𝑥))) ∘f · 𝑖) finSupp 0 )
145	125, 144	eqbrtrrd 5098	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))) finSupp 0 )
146		simp1 1135	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝜑)
147		eleq1w 2821	. . . . . . . . 9 ⊢ (𝑔 = ℎ → (𝑔 ∈ 𝑉 ↔ ℎ ∈ 𝑉))
148		id 22	. . . . . . . . . . 11 ⊢ (𝑔 = ℎ → 𝑔 = ℎ)
149	148, 148	oveq12d 7293	. . . . . . . . . 10 ⊢ (𝑔 = ℎ → (𝑔 , 𝑔) = (ℎ , ℎ))
150	149	eqeq1d 2740	. . . . . . . . 9 ⊢ (𝑔 = ℎ → ((𝑔 , 𝑔) = 0 ↔ (ℎ , ℎ) = 0 ))
151	147, 150	3anbi23d 1438	. . . . . . . 8 ⊢ (𝑔 = ℎ → ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ (𝑔 , 𝑔) = 0 ) ↔ (𝜑 ∧ ℎ ∈ 𝑉 ∧ (ℎ , ℎ) = 0 )))
152		eqeq1 2742	. . . . . . . 8 ⊢ (𝑔 = ℎ → (𝑔 = 𝑂 ↔ ℎ = 𝑂))
153	151, 152	imbi12d 345	. . . . . . 7 ⊢ (𝑔 = ℎ → (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ (𝑔 , 𝑔) = 0 ) → 𝑔 = 𝑂) ↔ ((𝜑 ∧ ℎ ∈ 𝑉 ∧ (ℎ , ℎ) = 0 ) → ℎ = 𝑂)))
154	153, 68	chvarvv 2002	. . . . . 6 ⊢ ((𝜑 ∧ ℎ ∈ 𝑉 ∧ (ℎ , ℎ) = 0 ) → ℎ = 𝑂)
155	14, 17, 20, 1, 5, 7, 24, 22, 9, 154, 35, 13	frlmphllem 20987	. . . . 5 ⊢ ((𝜑 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉) → (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥))) finSupp 0 )
156	146, 93, 83, 155	syl3anc 1370	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥))) finSupp 0 )
157	17, 24, 72, 73, 74, 92, 98, 99, 100, 145, 156	gsummptfsadd 19525	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))(+g‘𝑅)((ℎ‘𝑥) · (𝑖‘𝑥))))) = ((𝑅 Σg (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))))(+g‘𝑅)(𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥))))))
158	14, 17, 20	frlmip 20985	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝑊 ∧ 𝑅 ∈ DivRing) → (𝑔 ∈ (𝐵 ↑m 𝐼), ℎ ∈ (𝐵 ↑m 𝐼) ↦ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))))) = (·𝑖‘𝑌))
159	13, 12, 158	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → (𝑔 ∈ (𝐵 ↑m 𝐼), ℎ ∈ (𝐵 ↑m 𝐼) ↦ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))))) = (·𝑖‘𝑌))
160	5, 159	eqtr4id 2797	. . . . . . 7 ⊢ (𝜑 → , = (𝑔 ∈ (𝐵 ↑m 𝐼), ℎ ∈ (𝐵 ↑m 𝐼) ↦ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))))))
161		fveq1 6773	. . . . . . . . . . 11 ⊢ (𝑒 = 𝑔 → (𝑒‘𝑥) = (𝑔‘𝑥))
162	161	oveq1d 7290	. . . . . . . . . 10 ⊢ (𝑒 = 𝑔 → ((𝑒‘𝑥) · (𝑓‘𝑥)) = ((𝑔‘𝑥) · (𝑓‘𝑥)))
163	162	mpteq2dv 5176	. . . . . . . . 9 ⊢ (𝑒 = 𝑔 → (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑓‘𝑥))))
164	163	oveq2d 7291	. . . . . . . 8 ⊢ (𝑒 = 𝑔 → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥)))) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑓‘𝑥)))))
165		fveq1 6773	. . . . . . . . . . 11 ⊢ (𝑓 = ℎ → (𝑓‘𝑥) = (ℎ‘𝑥))
166	165	oveq2d 7291	. . . . . . . . . 10 ⊢ (𝑓 = ℎ → ((𝑔‘𝑥) · (𝑓‘𝑥)) = ((𝑔‘𝑥) · (ℎ‘𝑥)))
167	166	mpteq2dv 5176	. . . . . . . . 9 ⊢ (𝑓 = ℎ → (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑓‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))))
168	167	oveq2d 7291	. . . . . . . 8 ⊢ (𝑓 = ℎ → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑓‘𝑥)))) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥)))))
169	164, 168	cbvmpov 7370	. . . . . . 7 ⊢ (𝑒 ∈ (𝐵 ↑m 𝐼), 𝑓 ∈ (𝐵 ↑m 𝐼) ↦ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥))))) = (𝑔 ∈ (𝐵 ↑m 𝐼), ℎ ∈ (𝐵 ↑m 𝐼) ↦ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥)))))
170	160, 169	eqtr4di 2796	. . . . . 6 ⊢ (𝜑 → , = (𝑒 ∈ (𝐵 ↑m 𝐼), 𝑓 ∈ (𝐵 ↑m 𝐼) ↦ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥))))))
171	170	3ad2ant1 1132	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → , = (𝑒 ∈ (𝐵 ↑m 𝐼), 𝑓 ∈ (𝐵 ↑m 𝐼) ↦ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥))))))
172		simprl 768	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ((𝑘( ·𝑠 ‘𝑌)𝑔)(+g‘𝑌)ℎ) ∧ 𝑓 = 𝑖)) → 𝑒 = ((𝑘( ·𝑠 ‘𝑌)𝑔)(+g‘𝑌)ℎ))
173	172	fveq1d 6776	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ((𝑘( ·𝑠 ‘𝑌)𝑔)(+g‘𝑌)ℎ) ∧ 𝑓 = 𝑖)) → (𝑒‘𝑥) = (((𝑘( ·𝑠 ‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥))
174		simprr 770	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ((𝑘( ·𝑠 ‘𝑌)𝑔)(+g‘𝑌)ℎ) ∧ 𝑓 = 𝑖)) → 𝑓 = 𝑖)
175	174	fveq1d 6776	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ((𝑘( ·𝑠 ‘𝑌)𝑔)(+g‘𝑌)ℎ) ∧ 𝑓 = 𝑖)) → (𝑓‘𝑥) = (𝑖‘𝑥))
176	173, 175	oveq12d 7293	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ((𝑘( ·𝑠 ‘𝑌)𝑔)(+g‘𝑌)ℎ) ∧ 𝑓 = 𝑖)) → ((𝑒‘𝑥) · (𝑓‘𝑥)) = ((((𝑘( ·𝑠 ‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) · (𝑖‘𝑥)))
177	176	mpteq2dv 5176	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ((𝑘( ·𝑠 ‘𝑌)𝑔)(+g‘𝑌)ℎ) ∧ 𝑓 = 𝑖)) → (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((((𝑘( ·𝑠 ‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) · (𝑖‘𝑥))))
178	177	oveq2d 7291	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ((𝑘( ·𝑠 ‘𝑌)𝑔)(+g‘𝑌)ℎ) ∧ 𝑓 = 𝑖)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥)))) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((((𝑘( ·𝑠 ‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) · (𝑖‘𝑥)))))
179	29	3ad2ant1 1132	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑌 ∈ LMod)
180	16	3ad2ant1 1132	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑅 = (Scalar‘𝑌))
181	180	fveq2d 6778	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (Base‘𝑅) = (Base‘(Scalar‘𝑌)))
182	17, 181	eqtrid 2790	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝐵 = (Base‘(Scalar‘𝑌)))
183	77, 182	eleqtrd 2841	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → 𝑘 ∈ (Base‘(Scalar‘𝑌)))
184		eqid 2738	. . . . . . . . 9 ⊢ ( ·𝑠 ‘𝑌) = ( ·𝑠 ‘𝑌)
185		eqid 2738	. . . . . . . . 9 ⊢ (Base‘(Scalar‘𝑌)) = (Base‘(Scalar‘𝑌))
186	1, 31, 184, 185	lmodvscl 20140	. . . . . . . 8 ⊢ ((𝑌 ∈ LMod ∧ 𝑘 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑔 ∈ 𝑉) → (𝑘( ·𝑠 ‘𝑌)𝑔) ∈ 𝑉)
187	179, 183, 79, 186	syl3anc 1370	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑘( ·𝑠 ‘𝑌)𝑔) ∈ 𝑉)
188		eqid 2738	. . . . . . . 8 ⊢ (+g‘𝑌) = (+g‘𝑌)
189	1, 188	lmodvacl 20137	. . . . . . 7 ⊢ ((𝑌 ∈ LMod ∧ (𝑘( ·𝑠 ‘𝑌)𝑔) ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ((𝑘( ·𝑠 ‘𝑌)𝑔)(+g‘𝑌)ℎ) ∈ 𝑉)
190	179, 187, 93, 189	syl3anc 1370	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑘( ·𝑠 ‘𝑌)𝑔)(+g‘𝑌)ℎ) ∈ 𝑉)
191	14, 17, 1	frlmbasmap 20966	. . . . . 6 ⊢ ((𝐼 ∈ 𝑊 ∧ ((𝑘( ·𝑠 ‘𝑌)𝑔)(+g‘𝑌)ℎ) ∈ 𝑉) → ((𝑘( ·𝑠 ‘𝑌)𝑔)(+g‘𝑌)ℎ) ∈ (𝐵 ↑m 𝐼))
192	74, 190, 191	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑘( ·𝑠 ‘𝑌)𝑔)(+g‘𝑌)ℎ) ∈ (𝐵 ↑m 𝐼))
193		ovexd 7310	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((((𝑘( ·𝑠 ‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) · (𝑖‘𝑥)))) ∈ V)
194	171, 178, 192, 85, 193	ovmpod 7425	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (((𝑘( ·𝑠 ‘𝑌)𝑔)(+g‘𝑌)ℎ) , 𝑖) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((((𝑘( ·𝑠 ‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) · (𝑖‘𝑥)))))
195	14, 1, 75, 74, 187, 93, 72, 188	frlmplusgval 20971	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑘( ·𝑠 ‘𝑌)𝑔)(+g‘𝑌)ℎ) = ((𝑘( ·𝑠 ‘𝑌)𝑔) ∘f (+g‘𝑅)ℎ))
196	14, 17, 1	frlmbasmap 20966	. . . . . . . . . . . . 13 ⊢ ((𝐼 ∈ 𝑊 ∧ (𝑘( ·𝑠 ‘𝑌)𝑔) ∈ 𝑉) → (𝑘( ·𝑠 ‘𝑌)𝑔) ∈ (𝐵 ↑m 𝐼))
197	74, 187, 196	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑘( ·𝑠 ‘𝑌)𝑔) ∈ (𝐵 ↑m 𝐼))
198		elmapi 8637	. . . . . . . . . . . 12 ⊢ ((𝑘( ·𝑠 ‘𝑌)𝑔) ∈ (𝐵 ↑m 𝐼) → (𝑘( ·𝑠 ‘𝑌)𝑔):𝐼⟶𝐵)
199		ffn 6600	. . . . . . . . . . . 12 ⊢ ((𝑘( ·𝑠 ‘𝑌)𝑔):𝐼⟶𝐵 → (𝑘( ·𝑠 ‘𝑌)𝑔) Fn 𝐼)
200	197, 198, 199	3syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑘( ·𝑠 ‘𝑌)𝑔) Fn 𝐼)
201	95	ffnd 6601	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ℎ Fn 𝐼)
202	74	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → 𝐼 ∈ 𝑊)
203	79	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → 𝑔 ∈ 𝑉)
204	14, 1, 17, 202, 78, 203, 116, 184, 20	frlmvscaval 20975	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → ((𝑘( ·𝑠 ‘𝑌)𝑔)‘𝑥) = (𝑘 · (𝑔‘𝑥)))
205		eqidd 2739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (ℎ‘𝑥) = (ℎ‘𝑥))
206	200, 201, 74, 74, 53, 204, 205	offval 7542	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑘( ·𝑠 ‘𝑌)𝑔) ∘f (+g‘𝑅)ℎ) = (𝑥 ∈ 𝐼 ↦ ((𝑘 · (𝑔‘𝑥))(+g‘𝑅)(ℎ‘𝑥))))
207	195, 206	eqtrd 2778	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑘( ·𝑠 ‘𝑌)𝑔)(+g‘𝑌)ℎ) = (𝑥 ∈ 𝐼 ↦ ((𝑘 · (𝑔‘𝑥))(+g‘𝑅)(ℎ‘𝑥))))
208		ovexd 7310	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → ((𝑘 · (𝑔‘𝑥))(+g‘𝑅)(ℎ‘𝑥)) ∈ V)
209	207, 208	fvmpt2d 6888	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (((𝑘( ·𝑠 ‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) = ((𝑘 · (𝑔‘𝑥))(+g‘𝑅)(ℎ‘𝑥)))
210	209	oveq1d 7290	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → ((((𝑘( ·𝑠 ‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) · (𝑖‘𝑥)) = (((𝑘 · (𝑔‘𝑥))(+g‘𝑅)(ℎ‘𝑥)) · (𝑖‘𝑥)))
211	17, 72, 20	ringdir 19806	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ ((𝑘 · (𝑔‘𝑥)) ∈ 𝐵 ∧ (ℎ‘𝑥) ∈ 𝐵 ∧ (𝑖‘𝑥) ∈ 𝐵)) → (((𝑘 · (𝑔‘𝑥))(+g‘𝑅)(ℎ‘𝑥)) · (𝑖‘𝑥)) = (((𝑘 · (𝑔‘𝑥)) · (𝑖‘𝑥))(+g‘𝑅)((ℎ‘𝑥) · (𝑖‘𝑥))))
212	76, 106, 96, 88, 211	syl13anc 1371	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (((𝑘 · (𝑔‘𝑥))(+g‘𝑅)(ℎ‘𝑥)) · (𝑖‘𝑥)) = (((𝑘 · (𝑔‘𝑥)) · (𝑖‘𝑥))(+g‘𝑅)((ℎ‘𝑥) · (𝑖‘𝑥))))
213	122	oveq1d 7290	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → (((𝑘 · (𝑔‘𝑥)) · (𝑖‘𝑥))(+g‘𝑅)((ℎ‘𝑥) · (𝑖‘𝑥))) = ((𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))(+g‘𝑅)((ℎ‘𝑥) · (𝑖‘𝑥))))
214	210, 212, 213	3eqtrd 2782	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ 𝑥 ∈ 𝐼) → ((((𝑘( ·𝑠 ‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) · (𝑖‘𝑥)) = ((𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))(+g‘𝑅)((ℎ‘𝑥) · (𝑖‘𝑥))))
215	214	mpteq2dva 5174	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑥 ∈ 𝐼 ↦ ((((𝑘( ·𝑠 ‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) · (𝑖‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))(+g‘𝑅)((ℎ‘𝑥) · (𝑖‘𝑥)))))
216	215	oveq2d 7291	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((((𝑘( ·𝑠 ‘𝑌)𝑔)(+g‘𝑌)ℎ)‘𝑥) · (𝑖‘𝑥)))) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))(+g‘𝑅)((ℎ‘𝑥) · (𝑖‘𝑥))))))
217	194, 216	eqtrd 2778	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (((𝑘( ·𝑠 ‘𝑌)𝑔)(+g‘𝑌)ℎ) , 𝑖) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))(+g‘𝑅)((ℎ‘𝑥) · (𝑖‘𝑥))))))
218		simprl 768	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = 𝑔 ∧ 𝑓 = 𝑖)) → 𝑒 = 𝑔)
219	218	fveq1d 6776	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = 𝑔 ∧ 𝑓 = 𝑖)) → (𝑒‘𝑥) = (𝑔‘𝑥))
220		simprr 770	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = 𝑔 ∧ 𝑓 = 𝑖)) → 𝑓 = 𝑖)
221	220	fveq1d 6776	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = 𝑔 ∧ 𝑓 = 𝑖)) → (𝑓‘𝑥) = (𝑖‘𝑥))
222	219, 221	oveq12d 7293	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = 𝑔 ∧ 𝑓 = 𝑖)) → ((𝑒‘𝑥) · (𝑓‘𝑥)) = ((𝑔‘𝑥) · (𝑖‘𝑥)))
223	222	mpteq2dv 5176	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = 𝑔 ∧ 𝑓 = 𝑖)) → (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑖‘𝑥))))
224	223	oveq2d 7291	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = 𝑔 ∧ 𝑓 = 𝑖)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥)))) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑖‘𝑥)))))
225		ovexd 7310	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑖‘𝑥)))) ∈ V)
226	171, 224, 80, 85, 225	ovmpod 7425	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑔 , 𝑖) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑖‘𝑥)))))
227	226	oveq2d 7291	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑘 · (𝑔 , 𝑖)) = (𝑘 · (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑖‘𝑥))))))
228	14, 17, 20, 1, 5, 7, 24, 22, 9, 68, 35, 13	frlmphllem 20987	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ 𝑖 ∈ 𝑉) → (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑖‘𝑥))) finSupp 0 )
229	146, 79, 83, 228	syl3anc 1370	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑖‘𝑥))) finSupp 0 )
230	17, 24, 72, 20, 75, 74, 77, 90, 229	gsummulc2 19846	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥))))) = (𝑘 · (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (𝑖‘𝑥))))))
231	227, 230	eqtr4d 2781	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑘 · (𝑔 , 𝑖)) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥))))))
232		simprl 768	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑖)) → 𝑒 = ℎ)
233	232	fveq1d 6776	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑖)) → (𝑒‘𝑥) = (ℎ‘𝑥))
234		simprr 770	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑖)) → 𝑓 = 𝑖)
235	234	fveq1d 6776	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑖)) → (𝑓‘𝑥) = (𝑖‘𝑥))
236	233, 235	oveq12d 7293	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑖)) → ((𝑒‘𝑥) · (𝑓‘𝑥)) = ((ℎ‘𝑥) · (𝑖‘𝑥)))
237	236	mpteq2dv 5176	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑖)) → (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥))))
238	237	oveq2d 7291	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑖)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥)))) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥)))))
239		ovexd 7310	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥)))) ∈ V)
240	171, 238, 94, 85, 239	ovmpod 7425	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (ℎ , 𝑖) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥)))))
241	231, 240	oveq12d 7293	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → ((𝑘 · (𝑔 , 𝑖))(+g‘𝑅)(ℎ , 𝑖)) = ((𝑅 Σg (𝑥 ∈ 𝐼 ↦ (𝑘 · ((𝑔‘𝑥) · (𝑖‘𝑥)))))(+g‘𝑅)(𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑖‘𝑥))))))
242	157, 217, 241	3eqtr4d 2788	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵 ∧ (𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉 ∧ 𝑖 ∈ 𝑉)) → (((𝑘( ·𝑠 ‘𝑌)𝑔)(+g‘𝑌)ℎ) , 𝑖) = ((𝑘 · (𝑔 , 𝑖))(+g‘𝑅)(ℎ , 𝑖)))
243	34	3ad2ant1 1132	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → 𝑅 ∈ CRing)
244	243	adantr 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ CRing)
245	17, 20	crngcom 19801	. . . . . 6 ⊢ ((𝑅 ∈ CRing ∧ (ℎ‘𝑥) ∈ 𝐵 ∧ (𝑔‘𝑥) ∈ 𝐵) → ((ℎ‘𝑥) · (𝑔‘𝑥)) = ((𝑔‘𝑥) · (ℎ‘𝑥)))
246	244, 64, 63, 245	syl3anc 1370	. . . . 5 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ 𝑥 ∈ 𝐼) → ((ℎ‘𝑥) · (𝑔‘𝑥)) = ((𝑔‘𝑥) · (ℎ‘𝑥)))
247	246	mpteq2dva 5174	. . . 4 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥))))
248	247	oveq2d 7291	. . 3 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑔‘𝑥)))) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥)))))
249	170	3ad2ant1 1132	. . . 4 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → , = (𝑒 ∈ (𝐵 ↑m 𝐼), 𝑓 ∈ (𝐵 ↑m 𝐼) ↦ (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥))))))
250		simprl 768	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑔)) → 𝑒 = ℎ)
251	250	fveq1d 6776	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑔)) → (𝑒‘𝑥) = (ℎ‘𝑥))
252		simprr 770	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑔)) → 𝑓 = 𝑔)
253	252	fveq1d 6776	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑔)) → (𝑓‘𝑥) = (𝑔‘𝑥))
254	251, 253	oveq12d 7293	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑔)) → ((𝑒‘𝑥) · (𝑓‘𝑥)) = ((ℎ‘𝑥) · (𝑔‘𝑥)))
255	254	mpteq2dv 5176	. . . . 5 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑔)) → (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑔‘𝑥))))
256	255	oveq2d 7291	. . . 4 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) ∧ (𝑒 = ℎ ∧ 𝑓 = 𝑔)) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑒‘𝑥) · (𝑓‘𝑥)))) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑔‘𝑥)))))
257		ovexd 7310	. . . 4 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑔‘𝑥)))) ∈ V)
258	249, 256, 49, 44, 257	ovmpod 7425	. . 3 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → (ℎ , 𝑔) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((ℎ‘𝑥) · (𝑔‘𝑥)))))
259		fveq2 6774	. . . . . 6 ⊢ (𝑥 = (𝑔 , ℎ) → ( ∗ ‘𝑥) = ( ∗ ‘(𝑔 , ℎ)))
260		id 22	. . . . . 6 ⊢ (𝑥 = (𝑔 , ℎ) → 𝑥 = (𝑔 , ℎ))
261	259, 260	eqeq12d 2754	. . . . 5 ⊢ (𝑥 = (𝑔 , ℎ) → (( ∗ ‘𝑥) = 𝑥 ↔ ( ∗ ‘(𝑔 , ℎ)) = (𝑔 , ℎ)))
262	35	ralrimiva 3103	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ( ∗ ‘𝑥) = 𝑥)
263	262	3ad2ant1 1132	. . . . 5 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ∀𝑥 ∈ 𝐵 ( ∗ ‘𝑥) = 𝑥)
264	261, 263, 71	rspcdva 3562	. . . 4 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ( ∗ ‘(𝑔 , ℎ)) = (𝑔 , ℎ))
265	264, 58	eqtrd 2778	. . 3 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ( ∗ ‘(𝑔 , ℎ)) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ ((𝑔‘𝑥) · (ℎ‘𝑥)))))
266	248, 258, 265	3eqtr4rd 2789	. 2 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑉 ∧ ℎ ∈ 𝑉) → ( ∗ ‘(𝑔 , ℎ)) = (ℎ , 𝑔))
267	2, 3, 4, 6, 8, 16, 18, 19, 21, 23, 25, 33, 36, 71, 242, 68, 266	isphld 20859	1 ⊢ (𝜑 → 𝑌 ∈ PreHil)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086   = wceq 1539   ∈ wcel 2106  ∀wral 3064  Vcvv 3432   ⊆ wss 3887   class class class wbr 5074   ↦ cmpt 5157  Fun wfun 6427   Fn wfn 6428  ⟶wf 6429  ‘cfv 6433  (class class class)co 7275   ∈ cmpo 7277   ∘_f cof 7531   supp csupp 7977   ↑_m cmap 8615   finSupp cfsupp 9128  Basecbs 16912  +_gcplusg 16962  ._rcmulr 16963  *_𝑟cstv 16964  Scalarcsca 16965   ·_𝑠 cvsca 16966  ·_𝑖cip 16967  0_gc0g 17150   Σ_g cgsu 17151  CMndccmn 19386  Ringcrg 19783  CRingccrg 19784  DivRingcdr 19991  Fieldcfield 19992  LModclmod 20123  LVecclvec 20364  PreHilcphl 20829   freeLMod cfrlm 20953

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-cnex 10927  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-se 5545  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-isom 6442  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-of 7533  df-om 7713  df-1st 7831  df-2nd 7832  df-supp 7978  df-tpos 8042  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-1o 8297  df-er 8498  df-map 8617  df-ixp 8686  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-fsupp 9129  df-sup 9201  df-oi 9269  df-card 9697  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-nn 11974  df-2 12036  df-3 12037  df-4 12038  df-5 12039  df-6 12040  df-7 12041  df-8 12042  df-9 12043  df-n0 12234  df-z 12320  df-dec 12438  df-uz 12583  df-fz 13240  df-fzo 13383  df-seq 13722  df-hash 14045  df-struct 16848  df-sets 16865  df-slot 16883  df-ndx 16895  df-base 16913  df-ress 16942  df-plusg 16975  df-mulr 16976  df-sca 16978  df-vsca 16979  df-ip 16980  df-tset 16981  df-ple 16982  df-ds 16984  df-hom 16986  df-cco 16987  df-0g 17152  df-gsum 17153  df-prds 17158  df-pws 17160  df-mgm 18326  df-sgrp 18375  df-mnd 18386  df-mhm 18430  df-submnd 18431  df-grp 18580  df-minusg 18581  df-sbg 18582  df-subg 18752  df-ghm 18832  df-cntz 18923  df-cmn 19388  df-abl 19389  df-mgp 19721  df-ur 19738  df-ring 19785  df-cring 19786  df-oppr 19862  df-rnghom 19959  df-drng 19993  df-field 19994  df-subrg 20022  df-staf 20105  df-srng 20106  df-lmod 20125  df-lss 20194  df-lmhm 20284  df-lvec 20365  df-sra 20434  df-rgmod 20435  df-phl 20831  df-dsmm 20939  df-frlm 20954

This theorem is referenced by:  rrxcph  24556