frlmphl

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)

	Ref	Expression
Hypotheses	frlmphl.y	$⊢ Y = R freeLMod I$
	frlmphl.b	$⊢ B = {Base}_{R}$
	frlmphl.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	frlmphl.v	$⊢ V = {Base}_{Y}$
	frlmphl.j	$⊢ \underset{˙}{,} = \cdot_{𝑖} (Y)$
	frlmphl.o	$⊢ O = 0_{Y}$
	frlmphl.0	$⊢ \underset{˙}{0} = 0_{R}$
	frlmphl.s	$⊢ \underset{˙}{} = _{R}$
	frlmphl.f	$⊢ φ \to R \in Field$
	frlmphl.m	$⊢ (φ \land g \in V \land g \underset{˙}{,} g = \underset{˙}{0}) \to g = O$
	frlmphl.u	$⊢ (φ \land x \in B) \to \underset{˙}{*} (x) = x$
	frlmphl.i	$⊢ φ \to I \in W$
Assertion	frlmphl	$⊢ φ \to Y \in PreHil$

Proof

Step	Hyp	Ref	Expression
1		frlmphl.y	$⊢ Y = R freeLMod I$
2		frlmphl.b	$⊢ B = {Base}_{R}$
3		frlmphl.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		frlmphl.v	$⊢ V = {Base}_{Y}$
5		frlmphl.j	$⊢ \underset{˙}{,} = \cdot_{𝑖} (Y)$
6		frlmphl.o	$⊢ O = 0_{Y}$
7		frlmphl.0	$⊢ \underset{˙}{0} = 0_{R}$
8		frlmphl.s	$⊢ \underset{˙}{} = _{R}$
9		frlmphl.f	$⊢ φ \to R \in Field$
10		frlmphl.m	$⊢ (φ \land g \in V \land g \underset{˙}{,} g = \underset{˙}{0}) \to g = O$
11		frlmphl.u	$⊢ (φ \land x \in B) \to \underset{˙}{*} (x) = x$
12		frlmphl.i	$⊢ φ \to I \in W$
13	4	a1i	$⊢ φ \to V = {Base}_{Y}$
14		eqidd	$⊢ φ \to +_{Y} = +_{Y}$
15		eqidd	$⊢ φ \to \cdot_{Y} = \cdot_{Y}$
16	5	a1i	$⊢ φ \to \underset{˙}{,} = \cdot_{𝑖} (Y)$
17	6	a1i	$⊢ φ \to O = 0_{Y}$
18		isfld	$⊢ R \in Field \leftrightarrow (R \in DivRing \land R \in CRing)$
19	9 18	sylib	$⊢ φ \to (R \in DivRing \land R \in CRing)$
20	19	simpld	$⊢ φ \to R \in DivRing$
21	1	frlmsca	$⊢ (R \in DivRing \land I \in W) \to R = Scalar (Y)$
22	20 12 21	syl2anc	$⊢ φ \to R = Scalar (Y)$
23	2	a1i	$⊢ φ \to B = {Base}_{R}$
24		eqidd	$⊢ φ \to +_{R} = +_{R}$
25	3	a1i	$⊢ φ \to \underset{˙}{\cdot} = \cdot_{R}$
26	8	a1i	$⊢ φ \to \underset{˙}{} = _{R}$
27	7	a1i	$⊢ φ \to \underset{˙}{0} = 0_{R}$
28		drngring	$⊢ R \in DivRing \to R \in Ring$
29	20 28	syl	$⊢ φ \to R \in Ring$
30	1	frlmlmod	$⊢ (R \in Ring \land I \in W) \to Y \in LMod$
31	29 12 30	syl2anc	$⊢ φ \to Y \in LMod$
32	22 20	eqeltrrd	$⊢ φ \to Scalar (Y) \in DivRing$
33		eqid	$⊢ Scalar (Y) = Scalar (Y)$
34	33	islvec	$⊢ Y \in LVec \leftrightarrow (Y \in LMod \land Scalar (Y) \in DivRing)$
35	31 32 34	sylanbrc	$⊢ φ \to Y \in LVec$
36	19	simprd	$⊢ φ \to R \in CRing$
37	2 8 36 11	idsrngd	$⊢ φ \to R \in *-Ring$
38	12	3ad2ant1	$⊢ (φ \land g \in V \land h \in V) \to I \in W$
39	29	3ad2ant1	$⊢ (φ \land g \in V \land h \in V) \to R \in Ring$
40		simp2	$⊢ (φ \land g \in V \land h \in V) \to g \in V$
41		simp3	$⊢ (φ \land g \in V \land h \in V) \to h \in V$
42	1 2 3 4 5	frlmipval	$⊢ ((I \in W \land R \in Ring) \land (g \in V \land h \in V)) \to g \underset{˙}{,} h = \sum_{R} (g {\underset{˙}{\cdot}}_{f} h)$
43	38 39 40 41 42	syl22anc	$⊢ (φ \land g \in V \land h \in V) \to g \underset{˙}{,} h = \sum_{R} (g {\underset{˙}{\cdot}}_{f} h)$
44	1 2 4	frlmbasmap	$⊢ (I \in W \land g \in V) \to g \in (B^{I})$
45	38 40 44	syl2anc	$⊢ (φ \land g \in V \land h \in V) \to g \in (B^{I})$
46		elmapi	$⊢ g \in (B^{I}) \to g : I ⟶ B$
47	45 46	syl	$⊢ (φ \land g \in V \land h \in V) \to g : I ⟶ B$
48	47	ffnd	$⊢ (φ \land g \in V \land h \in V) \to g Fn I$
49	1 2 4	frlmbasmap	$⊢ (I \in W \land h \in V) \to h \in (B^{I})$
50	38 41 49	syl2anc	$⊢ (φ \land g \in V \land h \in V) \to h \in (B^{I})$
51		elmapi	$⊢ h \in (B^{I}) \to h : I ⟶ B$
52	50 51	syl	$⊢ (φ \land g \in V \land h \in V) \to h : I ⟶ B$
53	52	ffnd	$⊢ (φ \land g \in V \land h \in V) \to h Fn I$
54		inidm	$⊢ I \cap I = I$
55		eqidd	$⊢ ((φ \land g \in V \land h \in V) \land x \in I) \to g (x) = g (x)$
56		eqidd	$⊢ ((φ \land g \in V \land h \in V) \land x \in I) \to h (x) = h (x)$
57	48 53 38 38 54 55 56	offval	$⊢ (φ \land g \in V \land h \in V) \to g {\underset{˙}{\cdot}}_{f} h = (x \in I ⟼ g (x) \underset{˙}{\cdot} h (x))$
58	57	oveq2d	$⊢ (φ \land g \in V \land h \in V) \to \sum_{R} (g {\underset{˙}{\cdot}}_{f} h) = \underset{x \in I}{\sum_{R}} (g (x) \underset{˙}{\cdot} h (x))$
59	43 58	eqtrd	$⊢ (φ \land g \in V \land h \in V) \to g \underset{˙}{,} h = \underset{x \in I}{\sum_{R}} (g (x) \underset{˙}{\cdot} h (x))$
60		ringcmn	$⊢ R \in Ring \to R \in CMnd$
61	29 60	syl	$⊢ φ \to R \in CMnd$
62	61	3ad2ant1	$⊢ (φ \land g \in V \land h \in V) \to R \in CMnd$
63	39	adantr	$⊢ ((φ \land g \in V \land h \in V) \land x \in I) \to R \in Ring$
64	47	ffvelrnda	$⊢ ((φ \land g \in V \land h \in V) \land x \in I) \to g (x) \in B$
65	52	ffvelrnda	$⊢ ((φ \land g \in V \land h \in V) \land x \in I) \to h (x) \in B$
66	2 3	ringcl	$⊢ (R \in Ring \land g (x) \in B \land h (x) \in B) \to g (x) \underset{˙}{\cdot} h (x) \in B$
67	63 64 65 66	syl3anc	$⊢ ((φ \land g \in V \land h \in V) \land x \in I) \to g (x) \underset{˙}{\cdot} h (x) \in B$
68	67	fmpttd	$⊢ (φ \land g \in V \land h \in V) \to (x \in I ⟼ g (x) \underset{˙}{\cdot} h (x)) : I ⟶ B$
69	1 2 3 4 5 6 7 8 9 10 11 12	frlmphllem	$⊢ (φ \land g \in V \land h \in V) \to {finSupp}_{\underset{˙}{0}} ((x \in I ⟼ g (x) \underset{˙}{\cdot} h (x)))$
70	2 7 62 38 68 69	gsumcl	$⊢ (φ \land g \in V \land h \in V) \to \underset{x \in I}{\sum_{R}} (g (x) \underset{˙}{\cdot} h (x)) \in B$
71	59 70	eqeltrd	$⊢ (φ \land g \in V \land h \in V) \to g \underset{˙}{,} h \in B$
72		eqid	$⊢ +_{R} = +_{R}$
73	61	3ad2ant1	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to R \in CMnd$
74	12	3ad2ant1	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to I \in W$
75	29	3ad2ant1	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to R \in Ring$
76	75	adantr	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land x \in I) \to R \in Ring$
77		simp2	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to k \in B$
78	77	adantr	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land x \in I) \to k \in B$
79		simp31	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to g \in V$
80	74 79 44	syl2anc	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to g \in (B^{I})$
81	80 46	syl	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to g : I ⟶ B$
82	81	ffvelrnda	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land x \in I) \to g (x) \in B$
83		simp33	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to i \in V$
84	1 2 4	frlmbasmap	$⊢ (I \in W \land i \in V) \to i \in (B^{I})$
85	74 83 84	syl2anc	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to i \in (B^{I})$
86		elmapi	$⊢ i \in (B^{I}) \to i : I ⟶ B$
87	85 86	syl	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to i : I ⟶ B$
88	87	ffvelrnda	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land x \in I) \to i (x) \in B$
89	2 3	ringcl	$⊢ (R \in Ring \land g (x) \in B \land i (x) \in B) \to g (x) \underset{˙}{\cdot} i (x) \in B$
90	76 82 88 89	syl3anc	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land x \in I) \to g (x) \underset{˙}{\cdot} i (x) \in B$
91	2 3	ringcl	$⊢ (R \in Ring \land k \in B \land g (x) \underset{˙}{\cdot} i (x) \in B) \to k \underset{˙}{\cdot} (g (x) \underset{˙}{\cdot} i (x)) \in B$
92	76 78 90 91	syl3anc	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land x \in I) \to k \underset{˙}{\cdot} (g (x) \underset{˙}{\cdot} i (x)) \in B$
93		simp32	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to h \in V$
94	74 93 49	syl2anc	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to h \in (B^{I})$
95	94 51	syl	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to h : I ⟶ B$
96	95	ffvelrnda	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land x \in I) \to h (x) \in B$
97	2 3	ringcl	$⊢ (R \in Ring \land h (x) \in B \land i (x) \in B) \to h (x) \underset{˙}{\cdot} i (x) \in B$
98	76 96 88 97	syl3anc	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land x \in I) \to h (x) \underset{˙}{\cdot} i (x) \in B$
99		eqidd	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to (x \in I ⟼ k \underset{˙}{\cdot} (g (x) \underset{˙}{\cdot} i (x))) = (x \in I ⟼ k \underset{˙}{\cdot} (g (x) \underset{˙}{\cdot} i (x)))$
100		eqidd	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to (x \in I ⟼ h (x) \underset{˙}{\cdot} i (x)) = (x \in I ⟼ h (x) \underset{˙}{\cdot} i (x))$
101		fveq2	$⊢ x = y \to g (x) = g (y)$
102	101	oveq2d	$⊢ x = y \to k \underset{˙}{\cdot} g (x) = k \underset{˙}{\cdot} g (y)$
103	102	cbvmptv	$⊢ (x \in I ⟼ k \underset{˙}{\cdot} g (x)) = (y \in I ⟼ k \underset{˙}{\cdot} g (y))$
104	103	oveq1i	$⊢ (x \in I ⟼ k \underset{˙}{\cdot} g (x)) {\underset{˙}{\cdot}}_{f} i = (y \in I ⟼ k \underset{˙}{\cdot} g (y)) {\underset{˙}{\cdot}}_{f} i$
105	2 3	ringcl	$⊢ (R \in Ring \land k \in B \land g (x) \in B) \to k \underset{˙}{\cdot} g (x) \in B$
106	76 78 82 105	syl3anc	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land x \in I) \to k \underset{˙}{\cdot} g (x) \in B$
107	106	fmpttd	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to (x \in I ⟼ k \underset{˙}{\cdot} g (x)) : I ⟶ B$
108	107	ffnd	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to (x \in I ⟼ k \underset{˙}{\cdot} g (x)) Fn I$
109	103	fneq1i	$⊢ (x \in I ⟼ k \underset{˙}{\cdot} g (x)) Fn I \leftrightarrow (y \in I ⟼ k \underset{˙}{\cdot} g (y)) Fn I$
110	108 109	sylib	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to (y \in I ⟼ k \underset{˙}{\cdot} g (y)) Fn I$
111	87	ffnd	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to i Fn I$
112		eqidd	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land x \in I) \to (y \in I ⟼ k \underset{˙}{\cdot} g (y)) = (y \in I ⟼ k \underset{˙}{\cdot} g (y))$
113		simpr	$⊢ (((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land x \in I) \land y = x) \to y = x$
114	113	fveq2d	$⊢ (((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land x \in I) \land y = x) \to g (y) = g (x)$
115	114	oveq2d	$⊢ (((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land x \in I) \land y = x) \to k \underset{˙}{\cdot} g (y) = k \underset{˙}{\cdot} g (x)$
116		simpr	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land x \in I) \to x \in I$
117		ovexd	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land x \in I) \to k \underset{˙}{\cdot} g (x) \in V$
118	112 115 116 117	fvmptd	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land x \in I) \to (y \in I ⟼ k \underset{˙}{\cdot} g (y)) (x) = k \underset{˙}{\cdot} g (x)$
119		eqidd	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land x \in I) \to i (x) = i (x)$
120	110 111 74 74 54 118 119	offval	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to (y \in I ⟼ k \underset{˙}{\cdot} g (y)) {\underset{˙}{\cdot}}_{f} i = (x \in I ⟼ (k \underset{˙}{\cdot} g (x)) \underset{˙}{\cdot} i (x))$
121	2 3	ringass	$⊢ (R \in Ring \land (k \in B \land g (x) \in B \land i (x) \in B)) \to (k \underset{˙}{\cdot} g (x)) \underset{˙}{\cdot} i (x) = k \underset{˙}{\cdot} (g (x) \underset{˙}{\cdot} i (x))$
122	76 78 82 88 121	syl13anc	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land x \in I) \to (k \underset{˙}{\cdot} g (x)) \underset{˙}{\cdot} i (x) = k \underset{˙}{\cdot} (g (x) \underset{˙}{\cdot} i (x))$
123	122	mpteq2dva	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to (x \in I ⟼ (k \underset{˙}{\cdot} g (x)) \underset{˙}{\cdot} i (x)) = (x \in I ⟼ k \underset{˙}{\cdot} (g (x) \underset{˙}{\cdot} i (x)))$
124	120 123	eqtrd	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to (y \in I ⟼ k \underset{˙}{\cdot} g (y)) {\underset{˙}{\cdot}}_{f} i = (x \in I ⟼ k \underset{˙}{\cdot} (g (x) \underset{˙}{\cdot} i (x)))$
125	104 124	syl5eq	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to (x \in I ⟼ k \underset{˙}{\cdot} g (x)) {\underset{˙}{\cdot}}_{f} i = (x \in I ⟼ k \underset{˙}{\cdot} (g (x) \underset{˙}{\cdot} i (x)))$
126		ovexd	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to (x \in I ⟼ k \underset{˙}{\cdot} g (x)) {\underset{˙}{\cdot}}_{f} i \in V$
127		funmpt	$⊢ Fun (z \in I ⟼ (x \in I ⟼ k \underset{˙}{\cdot} g (x)) (z) \underset{˙}{\cdot} i (z))$
128		eqidd	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land z \in I) \to (x \in I ⟼ k \underset{˙}{\cdot} g (x)) (z) = (x \in I ⟼ k \underset{˙}{\cdot} g (x)) (z)$
129		eqidd	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land z \in I) \to i (z) = i (z)$
130	108 111 74 74 54 128 129	offval	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to (x \in I ⟼ k \underset{˙}{\cdot} g (x)) {\underset{˙}{\cdot}}_{f} i = (z \in I ⟼ (x \in I ⟼ k \underset{˙}{\cdot} g (x)) (z) \underset{˙}{\cdot} i (z))$
131	130	funeqd	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to (Fun ((x \in I ⟼ k \underset{˙}{\cdot} g (x)) {\underset{˙}{\cdot}}_{f} i) \leftrightarrow Fun (z \in I ⟼ (x \in I ⟼ k \underset{˙}{\cdot} g (x)) (z) \underset{˙}{\cdot} i (z)))$
132	127 131	mpbiri	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to Fun ((x \in I ⟼ k \underset{˙}{\cdot} g (x)) {\underset{˙}{\cdot}}_{f} i)$
133		simp3	$⊢ (g \in V \land h \in V \land i \in V) \to i \in V$
134	12 133	anim12i	$⊢ (φ \land (g \in V \land h \in V \land i \in V)) \to (I \in W \land i \in V)$
135	134	3adant2	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to (I \in W \land i \in V)$
136	1 7 4	frlmbasfsupp	$⊢ (I \in W \land i \in V) \to {finSupp}_{\underset{˙}{0}} (i)$
137	135 136	syl	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to {finSupp}_{\underset{˙}{0}} (i)$
138	2 7	ring0cl	$⊢ R \in Ring \to \underset{˙}{0} \in B$
139	75 138	syl	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to \underset{˙}{0} \in B$
140	2 3 7	ringrz	$⊢ (R \in Ring \land y \in B) \to y \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
141	75 140	sylan	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land y \in B) \to y \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
142	74 139 107 87 141	suppofss2d	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to ((x \in I ⟼ k \underset{˙}{\cdot} g (x)) {\underset{˙}{\cdot}}_{f} i) supp \underset{˙}{0} \subseteq i supp \underset{˙}{0}$
143		fsuppsssupp	$⊢ (((x \in I ⟼ k \underset{˙}{\cdot} g (x)) {\underset{˙}{\cdot}}_{f} i \in V \land Fun ((x \in I ⟼ k \underset{˙}{\cdot} g (x)) {\underset{˙}{\cdot}}_{f} i)) \land ({finSupp}_{\underset{˙}{0}} (i) \land ((x \in I ⟼ k \underset{˙}{\cdot} g (x)) {\underset{˙}{\cdot}}_{f} i) supp \underset{˙}{0} \subseteq i supp \underset{˙}{0})) \to {finSupp}_{\underset{˙}{0}} (((x \in I ⟼ k \underset{˙}{\cdot} g (x)) {\underset{˙}{\cdot}}_{f} i))$
144	126 132 137 142 143	syl22anc	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to {finSupp}_{\underset{˙}{0}} (((x \in I ⟼ k \underset{˙}{\cdot} g (x)) {\underset{˙}{\cdot}}_{f} i))$
145	125 144	eqbrtrrd	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to {finSupp}_{\underset{˙}{0}} ((x \in I ⟼ k \underset{˙}{\cdot} (g (x) \underset{˙}{\cdot} i (x))))$
146		simp1	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to φ$
147		eleq1w	$⊢ g = h \to (g \in V \leftrightarrow h \in V)$
148		id	$⊢ g = h \to g = h$
149	148 148	oveq12d	$⊢ g = h \to g \underset{˙}{,} g = h \underset{˙}{,} h$
150	149	eqeq1d	$⊢ g = h \to (g \underset{˙}{,} g = \underset{˙}{0} \leftrightarrow h \underset{˙}{,} h = \underset{˙}{0})$
151	147 150	3anbi23d	$⊢ g = h \to ((φ \land g \in V \land g \underset{˙}{,} g = \underset{˙}{0}) \leftrightarrow (φ \land h \in V \land h \underset{˙}{,} h = \underset{˙}{0}))$
152		eqeq1	$⊢ g = h \to (g = O \leftrightarrow h = O)$
153	151 152	imbi12d	$⊢ g = h \to (((φ \land g \in V \land g \underset{˙}{,} g = \underset{˙}{0}) \to g = O) \leftrightarrow ((φ \land h \in V \land h \underset{˙}{,} h = \underset{˙}{0}) \to h = O))$
154	153 10	chvarvv	$⊢ (φ \land h \in V \land h \underset{˙}{,} h = \underset{˙}{0}) \to h = O$
155	1 2 3 4 5 6 7 8 9 154 11 12	frlmphllem	$⊢ (φ \land h \in V \land i \in V) \to {finSupp}_{\underset{˙}{0}} ((x \in I ⟼ h (x) \underset{˙}{\cdot} i (x)))$
156	146 93 83 155	syl3anc	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to {finSupp}_{\underset{˙}{0}} ((x \in I ⟼ h (x) \underset{˙}{\cdot} i (x)))$
157	2 7 72 73 74 92 98 99 100 145 156	gsummptfsadd	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to \underset{x \in I}{\sum_{R}} ((k \underset{˙}{\cdot} (g (x) \underset{˙}{\cdot} i (x))) +_{R} (h (x) \underset{˙}{\cdot} i (x))) = (\underset{x \in I}{\sum_{R}}, (k \underset{˙}{\cdot} (g (x) \underset{˙}{\cdot} i (x)))) +_{R} (\underset{x \in I}{\sum_{R}}, (h (x) \underset{˙}{\cdot} i (x)))$
158	1 2 3	frlmip	$⊢ (I \in W \land R \in DivRing) \to (g \in (B^{I}), h \in (B^{I}) ⟼ \underset{x \in I}{\sum_{R}} (g (x) \underset{˙}{\cdot} h (x))) = \cdot_{𝑖} (Y)$
159	12 20 158	syl2anc	$⊢ φ \to (g \in (B^{I}), h \in (B^{I}) ⟼ \underset{x \in I}{\sum_{R}} (g (x) \underset{˙}{\cdot} h (x))) = \cdot_{𝑖} (Y)$
160	5 159	eqtr4id	$⊢ φ \to \underset{˙}{,} = (g \in (B^{I}), h \in (B^{I}) ⟼ \underset{x \in I}{\sum_{R}} (g (x) \underset{˙}{\cdot} h (x)))$
161		fveq1	$⊢ e = g \to e (x) = g (x)$
162	161	oveq1d	$⊢ e = g \to e (x) \underset{˙}{\cdot} f (x) = g (x) \underset{˙}{\cdot} f (x)$
163	162	mpteq2dv	$⊢ e = g \to (x \in I ⟼ e (x) \underset{˙}{\cdot} f (x)) = (x \in I ⟼ g (x) \underset{˙}{\cdot} f (x))$
164	163	oveq2d	$⊢ e = g \to \underset{x \in I}{\sum_{R}} (e (x) \underset{˙}{\cdot} f (x)) = \underset{x \in I}{\sum_{R}} (g (x) \underset{˙}{\cdot} f (x))$
165		fveq1	$⊢ f = h \to f (x) = h (x)$
166	165	oveq2d	$⊢ f = h \to g (x) \underset{˙}{\cdot} f (x) = g (x) \underset{˙}{\cdot} h (x)$
167	166	mpteq2dv	$⊢ f = h \to (x \in I ⟼ g (x) \underset{˙}{\cdot} f (x)) = (x \in I ⟼ g (x) \underset{˙}{\cdot} h (x))$
168	167	oveq2d	$⊢ f = h \to \underset{x \in I}{\sum_{R}} (g (x) \underset{˙}{\cdot} f (x)) = \underset{x \in I}{\sum_{R}} (g (x) \underset{˙}{\cdot} h (x))$
169	164 168	cbvmpov	$⊢ (e \in (B^{I}), f \in (B^{I}) ⟼ \underset{x \in I}{\sum_{R}} (e (x) \underset{˙}{\cdot} f (x))) = (g \in (B^{I}), h \in (B^{I}) ⟼ \underset{x \in I}{\sum_{R}} (g (x) \underset{˙}{\cdot} h (x)))$
170	160 169	eqtr4di	$⊢ φ \to \underset{˙}{,} = (e \in (B^{I}), f \in (B^{I}) ⟼ \underset{x \in I}{\sum_{R}} (e (x) \underset{˙}{\cdot} f (x)))$
171	170	3ad2ant1	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to \underset{˙}{,} = (e \in (B^{I}), f \in (B^{I}) ⟼ \underset{x \in I}{\sum_{R}} (e (x) \underset{˙}{\cdot} f (x)))$
172		simprl	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land (e = (k \cdot_{Y} g) +_{Y} h \land f = i)) \to e = (k \cdot_{Y} g) +_{Y} h$
173	172	fveq1d	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land (e = (k \cdot_{Y} g) +_{Y} h \land f = i)) \to e (x) = ((k \cdot_{Y} g) +_{Y} h) (x)$
174		simprr	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land (e = (k \cdot_{Y} g) +_{Y} h \land f = i)) \to f = i$
175	174	fveq1d	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land (e = (k \cdot_{Y} g) +_{Y} h \land f = i)) \to f (x) = i (x)$
176	173 175	oveq12d	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land (e = (k \cdot_{Y} g) +_{Y} h \land f = i)) \to e (x) \underset{˙}{\cdot} f (x) = ((k \cdot_{Y} g) +_{Y} h) (x) \underset{˙}{\cdot} i (x)$
177	176	mpteq2dv	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land (e = (k \cdot_{Y} g) +_{Y} h \land f = i)) \to (x \in I ⟼ e (x) \underset{˙}{\cdot} f (x)) = (x \in I ⟼ ((k \cdot_{Y} g) +_{Y} h) (x) \underset{˙}{\cdot} i (x))$
178	177	oveq2d	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land (e = (k \cdot_{Y} g) +_{Y} h \land f = i)) \to \underset{x \in I}{\sum_{R}} (e (x) \underset{˙}{\cdot} f (x)) = \underset{x \in I}{\sum_{R}} (((k \cdot_{Y} g) +_{Y} h) (x) \underset{˙}{\cdot} i (x))$
179	31	3ad2ant1	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to Y \in LMod$
180	22	3ad2ant1	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to R = Scalar (Y)$
181	180	fveq2d	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to {Base}_{R} = {Base}_{Scalar (Y)}$
182	2 181	syl5eq	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to B = {Base}_{Scalar (Y)}$
183	77 182	eleqtrd	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to k \in {Base}_{Scalar (Y)}$
184		eqid	$⊢ \cdot_{Y} = \cdot_{Y}$
185		eqid	$⊢ {Base}_{Scalar (Y)} = {Base}_{Scalar (Y)}$
186	4 33 184 185	lmodvscl	$⊢ (Y \in LMod \land k \in {Base}_{Scalar (Y)} \land g \in V) \to k \cdot_{Y} g \in V$
187	179 183 79 186	syl3anc	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to k \cdot_{Y} g \in V$
188		eqid	$⊢ +_{Y} = +_{Y}$
189	4 188	lmodvacl	$⊢ (Y \in LMod \land k \cdot_{Y} g \in V \land h \in V) \to (k \cdot_{Y} g) +_{Y} h \in V$
190	179 187 93 189	syl3anc	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to (k \cdot_{Y} g) +_{Y} h \in V$
191	1 2 4	frlmbasmap	$⊢ (I \in W \land (k \cdot_{Y} g) +_{Y} h \in V) \to (k \cdot_{Y} g) +_{Y} h \in (B^{I})$
192	74 190 191	syl2anc	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to (k \cdot_{Y} g) +_{Y} h \in (B^{I})$
193		ovexd	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to \underset{x \in I}{\sum_{R}} (((k \cdot_{Y} g) +_{Y} h) (x) \underset{˙}{\cdot} i (x)) \in V$
194	171 178 192 85 193	ovmpod	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to ((k \cdot_{Y} g) +_{Y} h) \underset{˙}{,} i = \underset{x \in I}{\sum_{R}} (((k \cdot_{Y} g) +_{Y} h) (x) \underset{˙}{\cdot} i (x))$
195	1 4 75 74 187 93 72 188	frlmplusgval	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to (k \cdot_{Y} g) +_{Y} h = (k \cdot_{Y} g) {+_{R}}_{f} h$
196	1 2 4	frlmbasmap	$⊢ (I \in W \land k \cdot_{Y} g \in V) \to k \cdot_{Y} g \in (B^{I})$
197	74 187 196	syl2anc	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to k \cdot_{Y} g \in (B^{I})$
198		elmapi	$⊢ k \cdot_{Y} g \in (B^{I}) \to (k \cdot_{Y} g) : I ⟶ B$
199		ffn	$⊢ (k \cdot_{Y} g) : I ⟶ B \to (k \cdot_{Y} g) Fn I$
200	197 198 199	3syl	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to (k \cdot_{Y} g) Fn I$
201	95	ffnd	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to h Fn I$
202	74	adantr	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land x \in I) \to I \in W$
203	79	adantr	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land x \in I) \to g \in V$
204	1 4 2 202 78 203 116 184 3	frlmvscaval	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land x \in I) \to (k \cdot_{Y} g) (x) = k \underset{˙}{\cdot} g (x)$
205		eqidd	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land x \in I) \to h (x) = h (x)$
206	200 201 74 74 54 204 205	offval	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to (k \cdot_{Y} g) {+_{R}}_{f} h = (x \in I ⟼ (k \underset{˙}{\cdot} g (x)) +_{R} h (x))$
207	195 206	eqtrd	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to (k \cdot_{Y} g) +_{Y} h = (x \in I ⟼ (k \underset{˙}{\cdot} g (x)) +_{R} h (x))$
208		ovexd	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land x \in I) \to (k \underset{˙}{\cdot} g (x)) +_{R} h (x) \in V$
209	207 208	fvmpt2d	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land x \in I) \to ((k \cdot_{Y} g) +_{Y} h) (x) = (k \underset{˙}{\cdot} g (x)) +_{R} h (x)$
210	209	oveq1d	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land x \in I) \to ((k \cdot_{Y} g) +_{Y} h) (x) \underset{˙}{\cdot} i (x) = ((k \underset{˙}{\cdot} g (x)) +_{R} h (x)) \underset{˙}{\cdot} i (x)$
211	2 72 3	ringdir	$⊢ (R \in Ring \land (k \underset{˙}{\cdot} g (x) \in B \land h (x) \in B \land i (x) \in B)) \to ((k \underset{˙}{\cdot} g (x)) +_{R} h (x)) \underset{˙}{\cdot} i (x) = ((k \underset{˙}{\cdot} g (x)) \underset{˙}{\cdot} i (x)) +_{R} (h (x) \underset{˙}{\cdot} i (x))$
212	76 106 96 88 211	syl13anc	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land x \in I) \to ((k \underset{˙}{\cdot} g (x)) +_{R} h (x)) \underset{˙}{\cdot} i (x) = ((k \underset{˙}{\cdot} g (x)) \underset{˙}{\cdot} i (x)) +_{R} (h (x) \underset{˙}{\cdot} i (x))$
213	122	oveq1d	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land x \in I) \to ((k \underset{˙}{\cdot} g (x)) \underset{˙}{\cdot} i (x)) +_{R} (h (x) \underset{˙}{\cdot} i (x)) = (k \underset{˙}{\cdot} (g (x) \underset{˙}{\cdot} i (x))) +_{R} (h (x) \underset{˙}{\cdot} i (x))$
214	210 212 213	3eqtrd	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land x \in I) \to ((k \cdot_{Y} g) +_{Y} h) (x) \underset{˙}{\cdot} i (x) = (k \underset{˙}{\cdot} (g (x) \underset{˙}{\cdot} i (x))) +_{R} (h (x) \underset{˙}{\cdot} i (x))$
215	214	mpteq2dva	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to (x \in I ⟼ ((k \cdot_{Y} g) +_{Y} h) (x) \underset{˙}{\cdot} i (x)) = (x \in I ⟼ (k \underset{˙}{\cdot} (g (x) \underset{˙}{\cdot} i (x))) +_{R} (h (x) \underset{˙}{\cdot} i (x)))$
216	215	oveq2d	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to \underset{x \in I}{\sum_{R}} (((k \cdot_{Y} g) +_{Y} h) (x) \underset{˙}{\cdot} i (x)) = \underset{x \in I}{\sum_{R}} ((k \underset{˙}{\cdot} (g (x) \underset{˙}{\cdot} i (x))) +_{R} (h (x) \underset{˙}{\cdot} i (x)))$
217	194 216	eqtrd	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to ((k \cdot_{Y} g) +_{Y} h) \underset{˙}{,} i = \underset{x \in I}{\sum_{R}} ((k \underset{˙}{\cdot} (g (x) \underset{˙}{\cdot} i (x))) +_{R} (h (x) \underset{˙}{\cdot} i (x)))$
218		simprl	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land (e = g \land f = i)) \to e = g$
219	218	fveq1d	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land (e = g \land f = i)) \to e (x) = g (x)$
220		simprr	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land (e = g \land f = i)) \to f = i$
221	220	fveq1d	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land (e = g \land f = i)) \to f (x) = i (x)$
222	219 221	oveq12d	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land (e = g \land f = i)) \to e (x) \underset{˙}{\cdot} f (x) = g (x) \underset{˙}{\cdot} i (x)$
223	222	mpteq2dv	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land (e = g \land f = i)) \to (x \in I ⟼ e (x) \underset{˙}{\cdot} f (x)) = (x \in I ⟼ g (x) \underset{˙}{\cdot} i (x))$
224	223	oveq2d	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land (e = g \land f = i)) \to \underset{x \in I}{\sum_{R}} (e (x) \underset{˙}{\cdot} f (x)) = \underset{x \in I}{\sum_{R}} (g (x) \underset{˙}{\cdot} i (x))$
225		ovexd	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to \underset{x \in I}{\sum_{R}} (g (x) \underset{˙}{\cdot} i (x)) \in V$
226	171 224 80 85 225	ovmpod	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to g \underset{˙}{,} i = \underset{x \in I}{\sum_{R}} (g (x) \underset{˙}{\cdot} i (x))$
227	226	oveq2d	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to k \underset{˙}{\cdot} (g \underset{˙}{,} i) = k \underset{˙}{\cdot} (\underset{x \in I}{\sum_{R}}, (g (x) \underset{˙}{\cdot} i (x)))$
228	1 2 3 4 5 6 7 8 9 10 11 12	frlmphllem	$⊢ (φ \land g \in V \land i \in V) \to {finSupp}_{\underset{˙}{0}} ((x \in I ⟼ g (x) \underset{˙}{\cdot} i (x)))$
229	146 79 83 228	syl3anc	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to {finSupp}_{\underset{˙}{0}} ((x \in I ⟼ g (x) \underset{˙}{\cdot} i (x)))$
230	2 7 72 3 75 74 77 90 229	gsummulc2	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to \underset{x \in I}{\sum_{R}} (k \underset{˙}{\cdot} (g (x) \underset{˙}{\cdot} i (x))) = k \underset{˙}{\cdot} (\underset{x \in I}{\sum_{R}}, (g (x) \underset{˙}{\cdot} i (x)))$
231	227 230	eqtr4d	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to k \underset{˙}{\cdot} (g \underset{˙}{,} i) = \underset{x \in I}{\sum_{R}} (k \underset{˙}{\cdot} (g (x) \underset{˙}{\cdot} i (x)))$
232		simprl	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land (e = h \land f = i)) \to e = h$
233	232	fveq1d	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land (e = h \land f = i)) \to e (x) = h (x)$
234		simprr	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land (e = h \land f = i)) \to f = i$
235	234	fveq1d	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land (e = h \land f = i)) \to f (x) = i (x)$
236	233 235	oveq12d	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land (e = h \land f = i)) \to e (x) \underset{˙}{\cdot} f (x) = h (x) \underset{˙}{\cdot} i (x)$
237	236	mpteq2dv	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land (e = h \land f = i)) \to (x \in I ⟼ e (x) \underset{˙}{\cdot} f (x)) = (x \in I ⟼ h (x) \underset{˙}{\cdot} i (x))$
238	237	oveq2d	$⊢ ((φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \land (e = h \land f = i)) \to \underset{x \in I}{\sum_{R}} (e (x) \underset{˙}{\cdot} f (x)) = \underset{x \in I}{\sum_{R}} (h (x) \underset{˙}{\cdot} i (x))$
239		ovexd	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to \underset{x \in I}{\sum_{R}} (h (x) \underset{˙}{\cdot} i (x)) \in V$
240	171 238 94 85 239	ovmpod	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to h \underset{˙}{,} i = \underset{x \in I}{\sum_{R}} (h (x) \underset{˙}{\cdot} i (x))$
241	231 240	oveq12d	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to (k \underset{˙}{\cdot} (g \underset{˙}{,} i)) +_{R} (h \underset{˙}{,} i) = (\underset{x \in I}{\sum_{R}}, (k \underset{˙}{\cdot} (g (x) \underset{˙}{\cdot} i (x)))) +_{R} (\underset{x \in I}{\sum_{R}}, (h (x) \underset{˙}{\cdot} i (x)))$
242	157 217 241	3eqtr4d	$⊢ (φ \land k \in B \land (g \in V \land h \in V \land i \in V)) \to ((k \cdot_{Y} g) +_{Y} h) \underset{˙}{,} i = (k \underset{˙}{\cdot} (g \underset{˙}{,} i)) +_{R} (h \underset{˙}{,} i)$
243	36	3ad2ant1	$⊢ (φ \land g \in V \land h \in V) \to R \in CRing$
244	243	adantr	$⊢ ((φ \land g \in V \land h \in V) \land x \in I) \to R \in CRing$
245	2 3	crngcom	$⊢ (R \in CRing \land h (x) \in B \land g (x) \in B) \to h (x) \underset{˙}{\cdot} g (x) = g (x) \underset{˙}{\cdot} h (x)$
246	244 65 64 245	syl3anc	$⊢ ((φ \land g \in V \land h \in V) \land x \in I) \to h (x) \underset{˙}{\cdot} g (x) = g (x) \underset{˙}{\cdot} h (x)$
247	246	mpteq2dva	$⊢ (φ \land g \in V \land h \in V) \to (x \in I ⟼ h (x) \underset{˙}{\cdot} g (x)) = (x \in I ⟼ g (x) \underset{˙}{\cdot} h (x))$
248	247	oveq2d	$⊢ (φ \land g \in V \land h \in V) \to \underset{x \in I}{\sum_{R}} (h (x) \underset{˙}{\cdot} g (x)) = \underset{x \in I}{\sum_{R}} (g (x) \underset{˙}{\cdot} h (x))$
249	170	3ad2ant1	$⊢ (φ \land g \in V \land h \in V) \to \underset{˙}{,} = (e \in (B^{I}), f \in (B^{I}) ⟼ \underset{x \in I}{\sum_{R}} (e (x) \underset{˙}{\cdot} f (x)))$
250		simprl	$⊢ ((φ \land g \in V \land h \in V) \land (e = h \land f = g)) \to e = h$
251	250	fveq1d	$⊢ ((φ \land g \in V \land h \in V) \land (e = h \land f = g)) \to e (x) = h (x)$
252		simprr	$⊢ ((φ \land g \in V \land h \in V) \land (e = h \land f = g)) \to f = g$
253	252	fveq1d	$⊢ ((φ \land g \in V \land h \in V) \land (e = h \land f = g)) \to f (x) = g (x)$
254	251 253	oveq12d	$⊢ ((φ \land g \in V \land h \in V) \land (e = h \land f = g)) \to e (x) \underset{˙}{\cdot} f (x) = h (x) \underset{˙}{\cdot} g (x)$
255	254	mpteq2dv	$⊢ ((φ \land g \in V \land h \in V) \land (e = h \land f = g)) \to (x \in I ⟼ e (x) \underset{˙}{\cdot} f (x)) = (x \in I ⟼ h (x) \underset{˙}{\cdot} g (x))$
256	255	oveq2d	$⊢ ((φ \land g \in V \land h \in V) \land (e = h \land f = g)) \to \underset{x \in I}{\sum_{R}} (e (x) \underset{˙}{\cdot} f (x)) = \underset{x \in I}{\sum_{R}} (h (x) \underset{˙}{\cdot} g (x))$
257		ovexd	$⊢ (φ \land g \in V \land h \in V) \to \underset{x \in I}{\sum_{R}} (h (x) \underset{˙}{\cdot} g (x)) \in V$
258	249 256 50 45 257	ovmpod	$⊢ (φ \land g \in V \land h \in V) \to h \underset{˙}{,} g = \underset{x \in I}{\sum_{R}} (h (x) \underset{˙}{\cdot} g (x))$
259		fveq2	$⊢ x = g \underset{˙}{,} h \to \underset{˙}{} (x) = \underset{˙}{} (g \underset{˙}{,} h)$
260		id	$⊢ x = g \underset{˙}{,} h \to x = g \underset{˙}{,} h$
261	259 260	eqeq12d	$⊢ x = g \underset{˙}{,} h \to (\underset{˙}{} (x) = x \leftrightarrow \underset{˙}{} (g \underset{˙}{,} h) = g \underset{˙}{,} h)$
262	11	ralrimiva	$⊢ φ \to \forall x \in B \underset{˙}{*} (x) = x$
263	262	3ad2ant1	$⊢ (φ \land g \in V \land h \in V) \to \forall x \in B \underset{˙}{*} (x) = x$
264	261 263 71	rspcdva	$⊢ (φ \land g \in V \land h \in V) \to \underset{˙}{*} (g \underset{˙}{,} h) = g \underset{˙}{,} h$
265	264 59	eqtrd	$⊢ (φ \land g \in V \land h \in V) \to \underset{˙}{*} (g \underset{˙}{,} h) = \underset{x \in I}{\sum_{R}} (g (x) \underset{˙}{\cdot} h (x))$
266	248 258 265	3eqtr4rd	$⊢ (φ \land g \in V \land h \in V) \to \underset{˙}{*} (g \underset{˙}{,} h) = h \underset{˙}{,} g$
267	13 14 15 16 17 22 23 24 25 26 27 35 37 71 242 10 266	isphld	$⊢ φ \to Y \in PreHil$

Metamath Proof Explorer

Theorem frlmphl

Proof