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

Metamath Proof Explorer

Theorem frlmphl

Proof