hlhilphllem

	Ref	Expression
Hypotheses	hlhilphl.h	$⊢ H = LHyp (K)$
	hlhilphllem.u	$⊢ U = HLHil (K) (W)$
	hlhilphl.k	$⊢ φ \to (K \in HL \land W \in H)$
	hlhilphllem.f	$⊢ F = Scalar (U)$
	hlhilphllem.l	$⊢ L = DVecH (K) (W)$
	hlhilphllem.v	$⊢ V = {Base}_{L}$
	hlhilphllem.a	$⊢ \underset{˙}{+} = +_{L}$
	hlhilphllem.s	$⊢ \underset{˙}{\cdot} = \cdot_{L}$
	hlhilphllem.r	$⊢ R = Scalar (L)$
	hlhilphllem.b	$⊢ B = {Base}_{R}$
	hlhilphllem.p	$⊢ \underset{˙}{⨣} = +_{R}$
	hlhilphllem.t	$⊢ \underset{˙}{\times} = \cdot_{R}$
	hlhilphllem.q	$⊢ Q = 0_{R}$
	hlhilphllem.z	$⊢ \underset{˙}{0} = 0_{L}$
	hlhilphllem.i	$⊢ \underset{˙}{,} = \cdot_{𝑖} (U)$
	hlhilphllem.j	$⊢ J = HDMap (K) (W)$
	hlhilphllem.g	$⊢ G = HGMap (K) (W)$
	hlhilphllem.e	$⊢ E = (x \in V, y \in V ⟼ J (y) (x))$
Assertion	hlhilphllem	$⊢ φ \to U \in PreHil$

Proof

Step	Hyp	Ref	Expression
1		hlhilphl.h	$⊢ H = LHyp (K)$
2		hlhilphllem.u	$⊢ U = HLHil (K) (W)$
3		hlhilphl.k	$⊢ φ \to (K \in HL \land W \in H)$
4		hlhilphllem.f	$⊢ F = Scalar (U)$
5		hlhilphllem.l	$⊢ L = DVecH (K) (W)$
6		hlhilphllem.v	$⊢ V = {Base}_{L}$
7		hlhilphllem.a	$⊢ \underset{˙}{+} = +_{L}$
8		hlhilphllem.s	$⊢ \underset{˙}{\cdot} = \cdot_{L}$
9		hlhilphllem.r	$⊢ R = Scalar (L)$
10		hlhilphllem.b	$⊢ B = {Base}_{R}$
11		hlhilphllem.p	$⊢ \underset{˙}{⨣} = +_{R}$
12		hlhilphllem.t	$⊢ \underset{˙}{\times} = \cdot_{R}$
13		hlhilphllem.q	$⊢ Q = 0_{R}$
14		hlhilphllem.z	$⊢ \underset{˙}{0} = 0_{L}$
15		hlhilphllem.i	$⊢ \underset{˙}{,} = \cdot_{𝑖} (U)$
16		hlhilphllem.j	$⊢ J = HDMap (K) (W)$
17		hlhilphllem.g	$⊢ G = HGMap (K) (W)$
18		hlhilphllem.e	$⊢ E = (x \in V, y \in V ⟼ J (y) (x))$
19	1 2 3 5 6	hlhilbase	$⊢ φ \to V = {Base}_{U}$
20	1 2 3 5 7	hlhilplus	$⊢ φ \to \underset{˙}{+} = +_{U}$
21	1 5 8 2 3	hlhilvsca	$⊢ φ \to \underset{˙}{\cdot} = \cdot_{U}$
22	15	a1i	$⊢ φ \to \underset{˙}{,} = \cdot_{𝑖} (U)$
23	1 5 2 3 14	hlhil0	$⊢ φ \to \underset{˙}{0} = 0_{U}$
24	4	a1i	$⊢ φ \to F = Scalar (U)$
25	1 5 9 2 4 3 10	hlhilsbase2	$⊢ φ \to B = {Base}_{F}$
26	1 5 9 2 4 3 11	hlhilsplus2	$⊢ φ \to \underset{˙}{⨣} = +_{F}$
27	1 5 9 2 4 3 12	hlhilsmul2	$⊢ φ \to \underset{˙}{\times} = \cdot_{F}$
28	1 2 4 17 3	hlhilnvl	$⊢ φ \to G = *_{F}$
29	1 5 9 2 4 3 13	hlhils0	$⊢ φ \to Q = 0_{F}$
30	1 2 3	hlhillvec	$⊢ φ \to U \in LVec$
31	1 2 3 4	hlhilsrng	$⊢ φ \to F \in *-Ring$
32	3	3ad2ant1	$⊢ (φ \land a \in V \land b \in V) \to (K \in HL \land W \in H)$
33		simp2	$⊢ (φ \land a \in V \land b \in V) \to a \in V$
34		simp3	$⊢ (φ \land a \in V \land b \in V) \to b \in V$
35	1 5 6 16 2 32 15 33 34	hlhilipval	$⊢ (φ \land a \in V \land b \in V) \to a \underset{˙}{,} b = J (b) (a)$
36	1 5 6 9 10 16 32 33 34	hdmapipcl	$⊢ (φ \land a \in V \land b \in V) \to J (b) (a) \in B$
37	35 36	eqeltrd	$⊢ (φ \land a \in V \land b \in V) \to a \underset{˙}{,} b \in B$
38	3	3ad2ant1	$⊢ (φ \land d \in B \land (a \in V \land b \in V \land c \in V)) \to (K \in HL \land W \in H)$
39		simp31	$⊢ (φ \land d \in B \land (a \in V \land b \in V \land c \in V)) \to a \in V$
40		simp32	$⊢ (φ \land d \in B \land (a \in V \land b \in V \land c \in V)) \to b \in V$
41		simp33	$⊢ (φ \land d \in B \land (a \in V \land b \in V \land c \in V)) \to c \in V$
42		simp2	$⊢ (φ \land d \in B \land (a \in V \land b \in V \land c \in V)) \to d \in B$
43	1 5 6 7 8 9 10 11 12 16 38 39 40 41 42	hdmapln1	$⊢ (φ \land d \in B \land (a \in V \land b \in V \land c \in V)) \to J (c) ((d \underset{˙}{\cdot} a) \underset{˙}{+} b) = (d \underset{˙}{\times} J (c) (a)) \underset{˙}{⨣} J (c) (b)$
44	1 5 3	dvhlmod	$⊢ φ \to L \in LMod$
45	44	3ad2ant1	$⊢ (φ \land d \in B \land (a \in V \land b \in V \land c \in V)) \to L \in LMod$
46	6 9 8 10	lmodvscl	$⊢ (L \in LMod \land d \in B \land a \in V) \to d \underset{˙}{\cdot} a \in V$
47	45 42 39 46	syl3anc	$⊢ (φ \land d \in B \land (a \in V \land b \in V \land c \in V)) \to d \underset{˙}{\cdot} a \in V$
48	6 7	lmodvacl	$⊢ (L \in LMod \land d \underset{˙}{\cdot} a \in V \land b \in V) \to (d \underset{˙}{\cdot} a) \underset{˙}{+} b \in V$
49	45 47 40 48	syl3anc	$⊢ (φ \land d \in B \land (a \in V \land b \in V \land c \in V)) \to (d \underset{˙}{\cdot} a) \underset{˙}{+} b \in V$
50	1 5 6 16 2 38 15 49 41	hlhilipval	$⊢ (φ \land d \in B \land (a \in V \land b \in V \land c \in V)) \to ((d \underset{˙}{\cdot} a) \underset{˙}{+} b) \underset{˙}{,} c = J (c) ((d \underset{˙}{\cdot} a) \underset{˙}{+} b)$
51	1 5 6 16 2 38 15 39 41	hlhilipval	$⊢ (φ \land d \in B \land (a \in V \land b \in V \land c \in V)) \to a \underset{˙}{,} c = J (c) (a)$
52	51	oveq2d	$⊢ (φ \land d \in B \land (a \in V \land b \in V \land c \in V)) \to d \underset{˙}{\times} (a \underset{˙}{,} c) = d \underset{˙}{\times} J (c) (a)$
53	1 5 6 16 2 38 15 40 41	hlhilipval	$⊢ (φ \land d \in B \land (a \in V \land b \in V \land c \in V)) \to b \underset{˙}{,} c = J (c) (b)$
54	52 53	oveq12d	$⊢ (φ \land d \in B \land (a \in V \land b \in V \land c \in V)) \to (d \underset{˙}{\times} (a \underset{˙}{,} c)) \underset{˙}{⨣} (b \underset{˙}{,} c) = (d \underset{˙}{\times} J (c) (a)) \underset{˙}{⨣} J (c) (b)$
55	43 50 54	3eqtr4d	$⊢ (φ \land d \in B \land (a \in V \land b \in V \land c \in V)) \to ((d \underset{˙}{\cdot} a) \underset{˙}{+} b) \underset{˙}{,} c = (d \underset{˙}{\times} (a \underset{˙}{,} c)) \underset{˙}{⨣} (b \underset{˙}{,} c)$
56	3	adantr	$⊢ (φ \land a \in V) \to (K \in HL \land W \in H)$
57		simpr	$⊢ (φ \land a \in V) \to a \in V$
58	1 5 6 16 2 56 15 57 57	hlhilipval	$⊢ (φ \land a \in V) \to a \underset{˙}{,} a = J (a) (a)$
59	58	eqeq1d	$⊢ (φ \land a \in V) \to (a \underset{˙}{,} a = Q \leftrightarrow J (a) (a) = Q)$
60	1 5 6 14 9 13 16 56 57	hdmapip0	$⊢ (φ \land a \in V) \to (J (a) (a) = Q \leftrightarrow a = \underset{˙}{0})$
61	59 60	bitrd	$⊢ (φ \land a \in V) \to (a \underset{˙}{,} a = Q \leftrightarrow a = \underset{˙}{0})$
62	61	biimp3a	$⊢ (φ \land a \in V \land a \underset{˙}{,} a = Q) \to a = \underset{˙}{0}$
63	1 5 6 16 17 32 33 34	hdmapg	$⊢ (φ \land a \in V \land b \in V) \to G (J (b) (a)) = J (a) (b)$
64	35	fveq2d	$⊢ (φ \land a \in V \land b \in V) \to G (a \underset{˙}{,} b) = G (J (b) (a))$
65	1 5 6 16 2 32 15 34 33	hlhilipval	$⊢ (φ \land a \in V \land b \in V) \to b \underset{˙}{,} a = J (a) (b)$
66	63 64 65	3eqtr4d	$⊢ (φ \land a \in V \land b \in V) \to G (a \underset{˙}{,} b) = b \underset{˙}{,} a$
67	19 20 21 22 23 24 25 26 27 28 29 30 31 37 55 62 66	isphld	$⊢ φ \to U \in PreHil$

Metamath Proof Explorer

Theorem hlhilphllem

Proof