Theorem 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	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑊 ) )
	isphld.a	⊢ ( 𝜑 → + = ( +g ‘ 𝑊 ) )
	isphld.s	⊢ ( 𝜑 → · = ( ·𝑠 ‘ 𝑊 ) )
	isphld.i	⊢ ( 𝜑 → 𝐼 = ( ·𝑖 ‘ 𝑊 ) )
	isphld.z	⊢ ( 𝜑 → 0 = ( 0g ‘ 𝑊 ) )
	isphld.f	⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝑊 ) )
	isphld.k	⊢ ( 𝜑 → 𝐾 = ( Base ‘ 𝐹 ) )
	isphld.p	⊢ ( 𝜑 → ⨣ = ( +g ‘ 𝐹 ) )
	isphld.t	⊢ ( 𝜑 → × = ( .r ‘ 𝐹 ) )
	isphld.c	⊢ ( 𝜑 → ∗ = ( *𝑟 ‘ 𝐹 ) )
	isphld.o	⊢ ( 𝜑 → 𝑂 = ( 0g ‘ 𝐹 ) )
	isphld.l	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	isphld.r	⊢ ( 𝜑 → 𝐹 ∈ *-Ring )
	isphld.cl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑥 𝐼 𝑦 ) ∈ 𝐾 )
	isphld.d	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐾 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( ( 𝑞 · 𝑥 ) + 𝑦 ) 𝐼 𝑧 ) = ( ( 𝑞 × ( 𝑥 𝐼 𝑧 ) ) ⨣ ( 𝑦 𝐼 𝑧 ) ) )
	isphld.ns	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ ( 𝑥 𝐼 𝑥 ) = 𝑂 ) → 𝑥 = 0 )
	isphld.cj	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( ∗ ‘ ( 𝑥 𝐼 𝑦 ) ) = ( 𝑦 𝐼 𝑥 ) )
Assertion	isphld	⊢ ( 𝜑 → 𝑊 ∈ PreHil )

Proof

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