isphld

Description: Properties that determine a pre-Hilbert (inner product) space. (Contributed by Mario Carneiro, 18-Nov-2013) (Revised by Mario Carneiro, 7-Oct-2015)

	Ref	Expression
Hypotheses	isphld.v	$⊢ φ \to V = {Base}_{W}$
	isphld.a	$⊢ φ \to \underset{˙}{+} = +_{W}$
	isphld.s	$⊢ φ \to \underset{˙}{\cdot} = \cdot_{W}$
	isphld.i	$⊢ φ \to I = \cdot_{𝑖} (W)$
	isphld.z	$⊢ φ \to \underset{˙}{0} = 0_{W}$
	isphld.f	$⊢ φ \to F = Scalar (W)$
	isphld.k	$⊢ φ \to K = {Base}_{F}$
	isphld.p	$⊢ φ \to \underset{˙}{⨣} = +_{F}$
	isphld.t	$⊢ φ \to \underset{˙}{\times} = \cdot_{F}$
	isphld.c	$⊢ φ \to \underset{˙}{} = _{F}$
	isphld.o	$⊢ φ \to O = 0_{F}$
	isphld.l	$⊢ φ \to W \in LVec$
	isphld.r	$⊢ φ \to F \in *-Ring$
	isphld.cl	$⊢ (φ \land x \in V \land y \in V) \to x I y \in K$
	isphld.d	$⊢ (φ \land q \in K \land (x \in V \land y \in V \land z \in V)) \to ((q \underset{˙}{\cdot} x) \underset{˙}{+} y) I z = (q \underset{˙}{\times} (x I z)) \underset{˙}{⨣} (y I z)$
	isphld.ns	$⊢ (φ \land x \in V \land x I x = O) \to x = \underset{˙}{0}$
	isphld.cj	$⊢ (φ \land x \in V \land y \in V) \to \underset{˙}{*} (x I y) = y I x$
Assertion	isphld	$⊢ φ \to W \in PreHil$

Proof

Step	Hyp	Ref	Expression
1		isphld.v	$⊢ φ \to V = {Base}_{W}$
2		isphld.a	$⊢ φ \to \underset{˙}{+} = +_{W}$
3		isphld.s	$⊢ φ \to \underset{˙}{\cdot} = \cdot_{W}$
4		isphld.i	$⊢ φ \to I = \cdot_{𝑖} (W)$
5		isphld.z	$⊢ φ \to \underset{˙}{0} = 0_{W}$
6		isphld.f	$⊢ φ \to F = Scalar (W)$
7		isphld.k	$⊢ φ \to K = {Base}_{F}$
8		isphld.p	$⊢ φ \to \underset{˙}{⨣} = +_{F}$
9		isphld.t	$⊢ φ \to \underset{˙}{\times} = \cdot_{F}$
10		isphld.c	$⊢ φ \to \underset{˙}{} = _{F}$
11		isphld.o	$⊢ φ \to O = 0_{F}$
12		isphld.l	$⊢ φ \to W \in LVec$
13		isphld.r	$⊢ φ \to F \in *-Ring$
14		isphld.cl	$⊢ (φ \land x \in V \land y \in V) \to x I y \in K$
15		isphld.d	$⊢ (φ \land q \in K \land (x \in V \land y \in V \land z \in V)) \to ((q \underset{˙}{\cdot} x) \underset{˙}{+} y) I z = (q \underset{˙}{\times} (x I z)) \underset{˙}{⨣} (y I z)$
16		isphld.ns	$⊢ (φ \land x \in V \land x I x = O) \to x = \underset{˙}{0}$
17		isphld.cj	$⊢ (φ \land x \in V \land y \in V) \to \underset{˙}{*} (x I y) = y I x$
18	6 13	eqeltrrd	$⊢ φ \to Scalar (W) \in *-Ring$
19		oveq1	$⊢ y = w \to y \cdot_{𝑖} (W) x = w \cdot_{𝑖} (W) x$
20	19	cbvmptv	$⊢ (y \in {Base}_{W} ⟼ y \cdot_{𝑖} (W) x) = (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) x)$
21	14	3expib	$⊢ φ \to ((x \in V \land y \in V) \to x I y \in K)$
22	1	eleq2d	$⊢ φ \to (x \in V \leftrightarrow x \in {Base}_{W})$
23	1	eleq2d	$⊢ φ \to (y \in V \leftrightarrow y \in {Base}_{W})$
24	22 23	anbi12d	$⊢ φ \to ((x \in V \land y \in V) \leftrightarrow (x \in {Base}_{W} \land y \in {Base}_{W}))$
25	4	oveqd	$⊢ φ \to x I y = x \cdot_{𝑖} (W) y$
26	6	fveq2d	$⊢ φ \to {Base}_{F} = {Base}_{Scalar (W)}$
27	7 26	eqtrd	$⊢ φ \to K = {Base}_{Scalar (W)}$
28	25 27	eleq12d	$⊢ φ \to (x I y \in K \leftrightarrow x \cdot_{𝑖} (W) y \in {Base}_{Scalar (W)})$
29	21 24 28	3imtr3d	$⊢ φ \to ((x \in {Base}_{W} \land y \in {Base}_{W}) \to x \cdot_{𝑖} (W) y \in {Base}_{Scalar (W)})$
30	29	impl	$⊢ ((φ \land x \in {Base}_{W}) \land y \in {Base}_{W}) \to x \cdot_{𝑖} (W) y \in {Base}_{Scalar (W)}$
31	30	an32s	$⊢ ((φ \land y \in {Base}_{W}) \land x \in {Base}_{W}) \to x \cdot_{𝑖} (W) y \in {Base}_{Scalar (W)}$
32		oveq1	$⊢ w = x \to w \cdot_{𝑖} (W) y = x \cdot_{𝑖} (W) y$
33	32	cbvmptv	$⊢ (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) y) = (x \in {Base}_{W} ⟼ x \cdot_{𝑖} (W) y)$
34	31 33	fmptd	$⊢ (φ \land y \in {Base}_{W}) \to (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) y) : {Base}_{W} ⟶ {Base}_{Scalar (W)}$
35	34	ralrimiva	$⊢ φ \to \forall y \in {Base}_{W} (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) y) : {Base}_{W} ⟶ {Base}_{Scalar (W)}$
36		oveq2	$⊢ y = z \to w \cdot_{𝑖} (W) y = w \cdot_{𝑖} (W) z$
37	36	mpteq2dv	$⊢ y = z \to (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) y) = (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) z)$
38	37	feq1d	$⊢ y = z \to ((w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) y) : {Base}_{W} ⟶ {Base}_{Scalar (W)} \leftrightarrow (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) z) : {Base}_{W} ⟶ {Base}_{Scalar (W)})$
39	38	rspccva	$⊢ (\forall y \in {Base}_{W} (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) y) : {Base}_{W} ⟶ {Base}_{Scalar (W)} \land z \in {Base}_{W}) \to (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) z) : {Base}_{W} ⟶ {Base}_{Scalar (W)}$
40	35 39	sylan	$⊢ (φ \land z \in {Base}_{W}) \to (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) z) : {Base}_{W} ⟶ {Base}_{Scalar (W)}$
41		eqidd	$⊢ (φ \land z \in {Base}_{W}) \to Scalar (W) = Scalar (W)$
42	15	3exp	$⊢ φ \to (q \in K \to ((x \in V \land y \in V \land z \in V) \to ((q \underset{˙}{\cdot} x) \underset{˙}{+} y) I z = (q \underset{˙}{\times} (x I z)) \underset{˙}{⨣} (y I z)))$
43	27	eleq2d	$⊢ φ \to (q \in K \leftrightarrow q \in {Base}_{Scalar (W)})$
44		3anrot	$⊢ (z \in V \land x \in V \land y \in V) \leftrightarrow (x \in V \land y \in V \land z \in V)$
45	1	eleq2d	$⊢ φ \to (z \in V \leftrightarrow z \in {Base}_{W})$
46	45 22 23	3anbi123d	$⊢ φ \to ((z \in V \land x \in V \land y \in V) \leftrightarrow (z \in {Base}_{W} \land x \in {Base}_{W} \land y \in {Base}_{W}))$
47	44 46	bitr3id	$⊢ φ \to ((x \in V \land y \in V \land z \in V) \leftrightarrow (z \in {Base}_{W} \land x \in {Base}_{W} \land y \in {Base}_{W}))$
48	3	oveqd	$⊢ φ \to q \underset{˙}{\cdot} x = q \cdot_{W} x$
49		eqidd	$⊢ φ \to y = y$
50	2 48 49	oveq123d	$⊢ φ \to (q \underset{˙}{\cdot} x) \underset{˙}{+} y = (q \cdot_{W} x) +_{W} y$
51		eqidd	$⊢ φ \to z = z$
52	4 50 51	oveq123d	$⊢ φ \to ((q \underset{˙}{\cdot} x) \underset{˙}{+} y) I z = ((q \cdot_{W} x) +_{W} y) \cdot_{𝑖} (W) z$
53	6	fveq2d	$⊢ φ \to +_{F} = +_{Scalar (W)}$
54	8 53	eqtrd	$⊢ φ \to \underset{˙}{⨣} = +_{Scalar (W)}$
55	6	fveq2d	$⊢ φ \to \cdot_{F} = \cdot_{Scalar (W)}$
56	9 55	eqtrd	$⊢ φ \to \underset{˙}{\times} = \cdot_{Scalar (W)}$
57		eqidd	$⊢ φ \to q = q$
58	4	oveqd	$⊢ φ \to x I z = x \cdot_{𝑖} (W) z$
59	56 57 58	oveq123d	$⊢ φ \to q \underset{˙}{\times} (x I z) = q \cdot_{Scalar (W)} (x \cdot_{𝑖} (W) z)$
60	4	oveqd	$⊢ φ \to y I z = y \cdot_{𝑖} (W) z$
61	54 59 60	oveq123d	$⊢ φ \to (q \underset{˙}{\times} (x I z)) \underset{˙}{⨣} (y I z) = (q \cdot_{Scalar (W)} (x \cdot_{𝑖} (W) z)) +_{Scalar (W)} (y \cdot_{𝑖} (W) z)$
62	52 61	eqeq12d	$⊢ φ \to (((q \underset{˙}{\cdot} x) \underset{˙}{+} y) I z = (q \underset{˙}{\times} (x I z)) \underset{˙}{⨣} (y I z) \leftrightarrow ((q \cdot_{W} x) +_{W} y) \cdot_{𝑖} (W) z = (q \cdot_{Scalar (W)} (x \cdot_{𝑖} (W) z)) +_{Scalar (W)} (y \cdot_{𝑖} (W) z))$
63	47 62	imbi12d	$⊢ φ \to (((x \in V \land y \in V \land z \in V) \to ((q \underset{˙}{\cdot} x) \underset{˙}{+} y) I z = (q \underset{˙}{\times} (x I z)) \underset{˙}{⨣} (y I z)) \leftrightarrow ((z \in {Base}_{W} \land x \in {Base}_{W} \land y \in {Base}_{W}) \to ((q \cdot_{W} x) +_{W} y) \cdot_{𝑖} (W) z = (q \cdot_{Scalar (W)} (x \cdot_{𝑖} (W) z)) +_{Scalar (W)} (y \cdot_{𝑖} (W) z)))$
64	42 43 63	3imtr3d	$⊢ φ \to (q \in {Base}_{Scalar (W)} \to ((z \in {Base}_{W} \land x \in {Base}_{W} \land y \in {Base}_{W}) \to ((q \cdot_{W} x) +_{W} y) \cdot_{𝑖} (W) z = (q \cdot_{Scalar (W)} (x \cdot_{𝑖} (W) z)) +_{Scalar (W)} (y \cdot_{𝑖} (W) z)))$
65	64	imp31	$⊢ ((φ \land q \in {Base}_{Scalar (W)}) \land (z \in {Base}_{W} \land x \in {Base}_{W} \land y \in {Base}_{W})) \to ((q \cdot_{W} x) +_{W} y) \cdot_{𝑖} (W) z = (q \cdot_{Scalar (W)} (x \cdot_{𝑖} (W) z)) +_{Scalar (W)} (y \cdot_{𝑖} (W) z)$
66	65	3exp2	$⊢ (φ \land q \in {Base}_{Scalar (W)}) \to (z \in {Base}_{W} \to (x \in {Base}_{W} \to (y \in {Base}_{W} \to ((q \cdot_{W} x) +_{W} y) \cdot_{𝑖} (W) z = (q \cdot_{Scalar (W)} (x \cdot_{𝑖} (W) z)) +_{Scalar (W)} (y \cdot_{𝑖} (W) z))))$
67	66	impancom	$⊢ (φ \land z \in {Base}_{W}) \to (q \in {Base}_{Scalar (W)} \to (x \in {Base}_{W} \to (y \in {Base}_{W} \to ((q \cdot_{W} x) +_{W} y) \cdot_{𝑖} (W) z = (q \cdot_{Scalar (W)} (x \cdot_{𝑖} (W) z)) +_{Scalar (W)} (y \cdot_{𝑖} (W) z))))$
68	67	3imp2	$⊢ ((φ \land z \in {Base}_{W}) \land (q \in {Base}_{Scalar (W)} \land x \in {Base}_{W} \land y \in {Base}_{W})) \to ((q \cdot_{W} x) +_{W} y) \cdot_{𝑖} (W) z = (q \cdot_{Scalar (W)} (x \cdot_{𝑖} (W) z)) +_{Scalar (W)} (y \cdot_{𝑖} (W) z)$
69		lveclmod	$⊢ W \in LVec \to W \in LMod$
70	12 69	syl	$⊢ φ \to W \in LMod$
71	70	adantr	$⊢ (φ \land z \in {Base}_{W}) \to W \in LMod$
72	71	adantr	$⊢ ((φ \land z \in {Base}_{W}) \land (q \in {Base}_{Scalar (W)} \land x \in {Base}_{W} \land y \in {Base}_{W})) \to W \in LMod$
73		eqid	$⊢ {Base}_{W} = {Base}_{W}$
74		eqid	$⊢ LSubSp (W) = LSubSp (W)$
75	73 74	lss1	$⊢ W \in LMod \to {Base}_{W} \in LSubSp (W)$
76	72 75	syl	$⊢ ((φ \land z \in {Base}_{W}) \land (q \in {Base}_{Scalar (W)} \land x \in {Base}_{W} \land y \in {Base}_{W})) \to {Base}_{W} \in LSubSp (W)$
77		eqid	$⊢ Scalar (W) = Scalar (W)$
78		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
79		eqid	$⊢ +_{W} = +_{W}$
80		eqid	$⊢ \cdot_{W} = \cdot_{W}$
81	77 78 79 80 74	lsscl	$⊢ ({Base}_{W} \in LSubSp (W) \land (q \in {Base}_{Scalar (W)} \land x \in {Base}_{W} \land y \in {Base}_{W})) \to (q \cdot_{W} x) +_{W} y \in {Base}_{W}$
82	76 81	sylancom	$⊢ ((φ \land z \in {Base}_{W}) \land (q \in {Base}_{Scalar (W)} \land x \in {Base}_{W} \land y \in {Base}_{W})) \to (q \cdot_{W} x) +_{W} y \in {Base}_{W}$
83		oveq1	$⊢ w = (q \cdot_{W} x) +_{W} y \to w \cdot_{𝑖} (W) z = ((q \cdot_{W} x) +_{W} y) \cdot_{𝑖} (W) z$
84		eqid	$⊢ (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) z) = (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) z)$
85		ovex	$⊢ w \cdot_{𝑖} (W) z \in V$
86	83 84 85	fvmpt3i	$⊢ (q \cdot_{W} x) +_{W} y \in {Base}_{W} \to (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) z) ((q \cdot_{W} x) +_{W} y) = ((q \cdot_{W} x) +_{W} y) \cdot_{𝑖} (W) z$
87	82 86	syl	$⊢ ((φ \land z \in {Base}_{W}) \land (q \in {Base}_{Scalar (W)} \land x \in {Base}_{W} \land y \in {Base}_{W})) \to (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) z) ((q \cdot_{W} x) +_{W} y) = ((q \cdot_{W} x) +_{W} y) \cdot_{𝑖} (W) z$
88		simpr2	$⊢ ((φ \land z \in {Base}_{W}) \land (q \in {Base}_{Scalar (W)} \land x \in {Base}_{W} \land y \in {Base}_{W})) \to x \in {Base}_{W}$
89		oveq1	$⊢ w = x \to w \cdot_{𝑖} (W) z = x \cdot_{𝑖} (W) z$
90	89 84 85	fvmpt3i	$⊢ x \in {Base}_{W} \to (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) z) (x) = x \cdot_{𝑖} (W) z$
91	88 90	syl	$⊢ ((φ \land z \in {Base}_{W}) \land (q \in {Base}_{Scalar (W)} \land x \in {Base}_{W} \land y \in {Base}_{W})) \to (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) z) (x) = x \cdot_{𝑖} (W) z$
92	91	oveq2d	$⊢ ((φ \land z \in {Base}_{W}) \land (q \in {Base}_{Scalar (W)} \land x \in {Base}_{W} \land y \in {Base}_{W})) \to q \cdot_{Scalar (W)} (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) z) (x) = q \cdot_{Scalar (W)} (x \cdot_{𝑖} (W) z)$
93		simpr3	$⊢ ((φ \land z \in {Base}_{W}) \land (q \in {Base}_{Scalar (W)} \land x \in {Base}_{W} \land y \in {Base}_{W})) \to y \in {Base}_{W}$
94		oveq1	$⊢ w = y \to w \cdot_{𝑖} (W) z = y \cdot_{𝑖} (W) z$
95	94 84 85	fvmpt3i	$⊢ y \in {Base}_{W} \to (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) z) (y) = y \cdot_{𝑖} (W) z$
96	93 95	syl	$⊢ ((φ \land z \in {Base}_{W}) \land (q \in {Base}_{Scalar (W)} \land x \in {Base}_{W} \land y \in {Base}_{W})) \to (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) z) (y) = y \cdot_{𝑖} (W) z$
97	92 96	oveq12d	$⊢ ((φ \land z \in {Base}_{W}) \land (q \in {Base}_{Scalar (W)} \land x \in {Base}_{W} \land y \in {Base}_{W})) \to (q \cdot_{Scalar (W)} (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) z) (x)) +_{Scalar (W)} (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) z) (y) = (q \cdot_{Scalar (W)} (x \cdot_{𝑖} (W) z)) +_{Scalar (W)} (y \cdot_{𝑖} (W) z)$
98	68 87 97	3eqtr4d	$⊢ ((φ \land z \in {Base}_{W}) \land (q \in {Base}_{Scalar (W)} \land x \in {Base}_{W} \land y \in {Base}_{W})) \to (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) z) ((q \cdot_{W} x) +_{W} y) = (q \cdot_{Scalar (W)} (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) z) (x)) +_{Scalar (W)} (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) z) (y)$
99	98	ralrimivvva	$⊢ (φ \land z \in {Base}_{W}) \to \forall q \in {Base}_{Scalar (W)} \forall x \in {Base}_{W} \forall y \in {Base}_{W} (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) z) ((q \cdot_{W} x) +_{W} y) = (q \cdot_{Scalar (W)} (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) z) (x)) +_{Scalar (W)} (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) z) (y)$
100	77	lmodring	$⊢ W \in LMod \to Scalar (W) \in Ring$
101		rlmlmod	$⊢ Scalar (W) \in Ring \to ringLMod (Scalar (W)) \in LMod$
102	70 100 101	3syl	$⊢ φ \to ringLMod (Scalar (W)) \in LMod$
103	102	adantr	$⊢ (φ \land z \in {Base}_{W}) \to ringLMod (Scalar (W)) \in LMod$
104		rlmbas	$⊢ {Base}_{Scalar (W)} = {Base}_{ringLMod (Scalar (W))}$
105		fvex	$⊢ Scalar (W) \in V$
106		rlmsca	$⊢ Scalar (W) \in V \to Scalar (W) = Scalar (ringLMod (Scalar (W)))$
107	105 106	ax-mp	$⊢ Scalar (W) = Scalar (ringLMod (Scalar (W)))$
108		rlmplusg	$⊢ +_{Scalar (W)} = +_{ringLMod (Scalar (W))}$
109		rlmvsca	$⊢ \cdot_{Scalar (W)} = \cdot_{ringLMod (Scalar (W))}$
110	73 104 77 107 78 79 108 80 109	islmhm2	$⊢ (W \in LMod \land ringLMod (Scalar (W)) \in LMod) \to ((w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) z) \in (W LMHom ringLMod (Scalar (W))) \leftrightarrow ((w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) z) : {Base}_{W} ⟶ {Base}_{Scalar (W)} \land Scalar (W) = Scalar (W) \land \forall q \in {Base}_{Scalar (W)} \forall x \in {Base}_{W} \forall y \in {Base}_{W} (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) z) ((q \cdot_{W} x) +_{W} y) = (q \cdot_{Scalar (W)} (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) z) (x)) +_{Scalar (W)} (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) z) (y)))$
111	71 103 110	syl2anc	$⊢ (φ \land z \in {Base}_{W}) \to ((w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) z) \in (W LMHom ringLMod (Scalar (W))) \leftrightarrow ((w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) z) : {Base}_{W} ⟶ {Base}_{Scalar (W)} \land Scalar (W) = Scalar (W) \land \forall q \in {Base}_{Scalar (W)} \forall x \in {Base}_{W} \forall y \in {Base}_{W} (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) z) ((q \cdot_{W} x) +_{W} y) = (q \cdot_{Scalar (W)} (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) z) (x)) +_{Scalar (W)} (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) z) (y)))$
112	40 41 99 111	mpbir3and	$⊢ (φ \land z \in {Base}_{W}) \to (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) z) \in (W LMHom ringLMod (Scalar (W)))$
113	112	ralrimiva	$⊢ φ \to \forall z \in {Base}_{W} (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) z) \in (W LMHom ringLMod (Scalar (W)))$
114		oveq2	$⊢ z = x \to w \cdot_{𝑖} (W) z = w \cdot_{𝑖} (W) x$
115	114	mpteq2dv	$⊢ z = x \to (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) z) = (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) x)$
116	115	eleq1d	$⊢ z = x \to ((w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) z) \in (W LMHom ringLMod (Scalar (W))) \leftrightarrow (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) x) \in (W LMHom ringLMod (Scalar (W))))$
117	116	rspccva	$⊢ (\forall z \in {Base}_{W} (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) z) \in (W LMHom ringLMod (Scalar (W))) \land x \in {Base}_{W}) \to (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) x) \in (W LMHom ringLMod (Scalar (W)))$
118	113 117	sylan	$⊢ (φ \land x \in {Base}_{W}) \to (w \in {Base}_{W} ⟼ w \cdot_{𝑖} (W) x) \in (W LMHom ringLMod (Scalar (W)))$
119	20 118	eqeltrid	$⊢ (φ \land x \in {Base}_{W}) \to (y \in {Base}_{W} ⟼ y \cdot_{𝑖} (W) x) \in (W LMHom ringLMod (Scalar (W)))$
120	16	3exp	$⊢ φ \to (x \in V \to (x I x = O \to x = \underset{˙}{0}))$
121	4	oveqd	$⊢ φ \to x I x = x \cdot_{𝑖} (W) x$
122	6	fveq2d	$⊢ φ \to 0_{F} = 0_{Scalar (W)}$
123	11 122	eqtrd	$⊢ φ \to O = 0_{Scalar (W)}$
124	121 123	eqeq12d	$⊢ φ \to (x I x = O \leftrightarrow x \cdot_{𝑖} (W) x = 0_{Scalar (W)})$
125	5	eqeq2d	$⊢ φ \to (x = \underset{˙}{0} \leftrightarrow x = 0_{W})$
126	124 125	imbi12d	$⊢ φ \to ((x I x = O \to x = \underset{˙}{0}) \leftrightarrow (x \cdot_{𝑖} (W) x = 0_{Scalar (W)} \to x = 0_{W}))$
127	120 22 126	3imtr3d	$⊢ φ \to (x \in {Base}_{W} \to (x \cdot_{𝑖} (W) x = 0_{Scalar (W)} \to x = 0_{W}))$
128	127	imp	$⊢ (φ \land x \in {Base}_{W}) \to (x \cdot_{𝑖} (W) x = 0_{Scalar (W)} \to x = 0_{W})$
129	17	3expib	$⊢ φ \to ((x \in V \land y \in V) \to \underset{˙}{*} (x I y) = y I x)$
130	6	fveq2d	$⊢ φ \to _{F} = _{Scalar (W)}$
131	10 130	eqtrd	$⊢ φ \to \underset{˙}{} = _{Scalar (W)}$
132	131 25	fveq12d	$⊢ φ \to \underset{˙}{} (x I y) = {(x \cdot_{𝑖} (W) y)}^{_{Scalar (W)}}$
133	4	oveqd	$⊢ φ \to y I x = y \cdot_{𝑖} (W) x$
134	132 133	eqeq12d	$⊢ φ \to (\underset{˙}{} (x I y) = y I x \leftrightarrow {(x \cdot_{𝑖} (W) y)}^{_{Scalar (W)}} = y \cdot_{𝑖} (W) x)$
135	129 24 134	3imtr3d	$⊢ φ \to ((x \in {Base}_{W} \land y \in {Base}_{W}) \to {(x \cdot_{𝑖} (W) y)}^{*_{Scalar (W)}} = y \cdot_{𝑖} (W) x)$
136	135	expdimp	$⊢ (φ \land x \in {Base}_{W}) \to (y \in {Base}_{W} \to {(x \cdot_{𝑖} (W) y)}^{*_{Scalar (W)}} = y \cdot_{𝑖} (W) x)$
137	136	ralrimiv	$⊢ (φ \land x \in {Base}_{W}) \to \forall y \in {Base}_{W} {(x \cdot_{𝑖} (W) y)}^{*_{Scalar (W)}} = y \cdot_{𝑖} (W) x$
138	119 128 137	3jca	$⊢ (φ \land x \in {Base}_{W}) \to ((y \in {Base}_{W} ⟼ y \cdot_{𝑖} (W) x) \in (W LMHom ringLMod (Scalar (W))) \land (x \cdot_{𝑖} (W) x = 0_{Scalar (W)} \to x = 0_{W}) \land \forall y \in {Base}_{W} {(x \cdot_{𝑖} (W) y)}^{*_{Scalar (W)}} = y \cdot_{𝑖} (W) x)$
139	138	ralrimiva	$⊢ φ \to \forall x \in {Base}_{W} ((y \in {Base}_{W} ⟼ y \cdot_{𝑖} (W) x) \in (W LMHom ringLMod (Scalar (W))) \land (x \cdot_{𝑖} (W) x = 0_{Scalar (W)} \to x = 0_{W}) \land \forall y \in {Base}_{W} {(x \cdot_{𝑖} (W) y)}^{*_{Scalar (W)}} = y \cdot_{𝑖} (W) x)$
140		eqid	$⊢ \cdot_{𝑖} (W) = \cdot_{𝑖} (W)$
141		eqid	$⊢ 0_{W} = 0_{W}$
142		eqid	$⊢ _{Scalar (W)} = _{Scalar (W)}$
143		eqid	$⊢ 0_{Scalar (W)} = 0_{Scalar (W)}$
144	73 77 140 141 142 143	isphl	$⊢ W \in PreHil \leftrightarrow (W \in LVec \land Scalar (W) \in -Ring \land \forall x \in {Base}_{W} ((y \in {Base}_{W} ⟼ y \cdot_{𝑖} (W) x) \in (W LMHom ringLMod (Scalar (W))) \land (x \cdot_{𝑖} (W) x = 0_{Scalar (W)} \to x = 0_{W}) \land \forall y \in {Base}_{W} {(x \cdot_{𝑖} (W) y)}^{_{Scalar (W)}} = y \cdot_{𝑖} (W) x))$
145	12 18 139 144	syl3anbrc	$⊢ φ \to W \in PreHil$

Metamath Proof Explorer

Theorem isphld

Proof