lflvscl

Description: Closure of a scalar product with a functional. Note that this is the scalar product for a right vector space with the scalar after the vector; reversing these fails closure. (Contributed by NM, 9-Oct-2014) (Revised by Mario Carneiro, 22-Apr-2015)

	Ref	Expression
Hypotheses	lflsccl.v	$⊢ V = {Base}_{W}$
	lflsccl.d	$⊢ D = Scalar (W)$
	lflsccl.k	$⊢ K = {Base}_{D}$
	lflsccl.t	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
	lflsccl.f	$⊢ F = LFnl (W)$
	lflsccl.w	$⊢ φ \to W \in LMod$
	lflsccl.g	$⊢ φ \to G \in F$
	lflsccl.r	$⊢ φ \to R \in K$
Assertion	lflvscl	$⊢ φ \to G {\underset{˙}{\cdot}}_{f} (V \times \{R\}) \in F$

Proof

Step	Hyp	Ref	Expression
1		lflsccl.v	$⊢ V = {Base}_{W}$
2		lflsccl.d	$⊢ D = Scalar (W)$
3		lflsccl.k	$⊢ K = {Base}_{D}$
4		lflsccl.t	$⊢ \underset{˙}{\cdot} = \cdot_{D}$
5		lflsccl.f	$⊢ F = LFnl (W)$
6		lflsccl.w	$⊢ φ \to W \in LMod$
7		lflsccl.g	$⊢ φ \to G \in F$
8		lflsccl.r	$⊢ φ \to R \in K$
9	1	a1i	$⊢ φ \to V = {Base}_{W}$
10		eqidd	$⊢ φ \to +_{W} = +_{W}$
11	2	a1i	$⊢ φ \to D = Scalar (W)$
12		eqidd	$⊢ φ \to \cdot_{W} = \cdot_{W}$
13	3	a1i	$⊢ φ \to K = {Base}_{D}$
14		eqidd	$⊢ φ \to +_{D} = +_{D}$
15	4	a1i	$⊢ φ \to \underset{˙}{\cdot} = \cdot_{D}$
16	5	a1i	$⊢ φ \to F = LFnl (W)$
17	2	lmodring	$⊢ W \in LMod \to D \in Ring$
18	6 17	syl	$⊢ φ \to D \in Ring$
19	3 4	ringcl	$⊢ (D \in Ring \land x \in K \land y \in K) \to x \underset{˙}{\cdot} y \in K$
20	19	3expb	$⊢ (D \in Ring \land (x \in K \land y \in K)) \to x \underset{˙}{\cdot} y \in K$
21	18 20	sylan	$⊢ (φ \land (x \in K \land y \in K)) \to x \underset{˙}{\cdot} y \in K$
22	2 3 1 5	lflf	$⊢ (W \in LMod \land G \in F) \to G : V ⟶ K$
23	6 7 22	syl2anc	$⊢ φ \to G : V ⟶ K$
24		fconst6g	$⊢ R \in K \to (V \times \{R\}) : V ⟶ K$
25	8 24	syl	$⊢ φ \to (V \times \{R\}) : V ⟶ K$
26	1	fvexi	$⊢ V \in V$
27	26	a1i	$⊢ φ \to V \in V$
28		inidm	$⊢ V \cap V = V$
29	21 23 25 27 27 28	off	$⊢ φ \to (G {\underset{˙}{\cdot}}_{f} (V \times \{R\})) : V ⟶ K$
30	6	adantr	$⊢ (φ \land (r \in K \land x \in V \land y \in V)) \to W \in LMod$
31	7	adantr	$⊢ (φ \land (r \in K \land x \in V \land y \in V)) \to G \in F$
32		simpr1	$⊢ (φ \land (r \in K \land x \in V \land y \in V)) \to r \in K$
33		simpr2	$⊢ (φ \land (r \in K \land x \in V \land y \in V)) \to x \in V$
34		simpr3	$⊢ (φ \land (r \in K \land x \in V \land y \in V)) \to y \in V$
35		eqid	$⊢ +_{W} = +_{W}$
36		eqid	$⊢ \cdot_{W} = \cdot_{W}$
37		eqid	$⊢ +_{D} = +_{D}$
38	1 35 2 36 3 37 4 5	lfli	$⊢ (W \in LMod \land G \in F \land (r \in K \land x \in V \land y \in V)) \to G ((r \cdot_{W} x) +_{W} y) = (r \underset{˙}{\cdot} G (x)) +_{D} G (y)$
39	30 31 32 33 34 38	syl113anc	$⊢ (φ \land (r \in K \land x \in V \land y \in V)) \to G ((r \cdot_{W} x) +_{W} y) = (r \underset{˙}{\cdot} G (x)) +_{D} G (y)$
40	39	oveq1d	$⊢ (φ \land (r \in K \land x \in V \land y \in V)) \to G ((r \cdot_{W} x) +_{W} y) \underset{˙}{\cdot} R = ((r \underset{˙}{\cdot} G (x)) +_{D} G (y)) \underset{˙}{\cdot} R$
41	18	adantr	$⊢ (φ \land (r \in K \land x \in V \land y \in V)) \to D \in Ring$
42	2 3 1 5	lflcl	$⊢ (W \in LMod \land G \in F \land x \in V) \to G (x) \in K$
43	30 31 33 42	syl3anc	$⊢ (φ \land (r \in K \land x \in V \land y \in V)) \to G (x) \in K$
44	3 4	ringcl	$⊢ (D \in Ring \land r \in K \land G (x) \in K) \to r \underset{˙}{\cdot} G (x) \in K$
45	41 32 43 44	syl3anc	$⊢ (φ \land (r \in K \land x \in V \land y \in V)) \to r \underset{˙}{\cdot} G (x) \in K$
46	2 3 1 5	lflcl	$⊢ (W \in LMod \land G \in F \land y \in V) \to G (y) \in K$
47	30 31 34 46	syl3anc	$⊢ (φ \land (r \in K \land x \in V \land y \in V)) \to G (y) \in K$
48	8	adantr	$⊢ (φ \land (r \in K \land x \in V \land y \in V)) \to R \in K$
49	3 37 4	ringdir	$⊢ (D \in Ring \land (r \underset{˙}{\cdot} G (x) \in K \land G (y) \in K \land R \in K)) \to ((r \underset{˙}{\cdot} G (x)) +_{D} G (y)) \underset{˙}{\cdot} R = ((r \underset{˙}{\cdot} G (x)) \underset{˙}{\cdot} R) +_{D} (G (y) \underset{˙}{\cdot} R)$
50	41 45 47 48 49	syl13anc	$⊢ (φ \land (r \in K \land x \in V \land y \in V)) \to ((r \underset{˙}{\cdot} G (x)) +_{D} G (y)) \underset{˙}{\cdot} R = ((r \underset{˙}{\cdot} G (x)) \underset{˙}{\cdot} R) +_{D} (G (y) \underset{˙}{\cdot} R)$
51	3 4	ringass	$⊢ (D \in Ring \land (r \in K \land G (x) \in K \land R \in K)) \to (r \underset{˙}{\cdot} G (x)) \underset{˙}{\cdot} R = r \underset{˙}{\cdot} (G (x) \underset{˙}{\cdot} R)$
52	41 32 43 48 51	syl13anc	$⊢ (φ \land (r \in K \land x \in V \land y \in V)) \to (r \underset{˙}{\cdot} G (x)) \underset{˙}{\cdot} R = r \underset{˙}{\cdot} (G (x) \underset{˙}{\cdot} R)$
53	52	oveq1d	$⊢ (φ \land (r \in K \land x \in V \land y \in V)) \to ((r \underset{˙}{\cdot} G (x)) \underset{˙}{\cdot} R) +_{D} (G (y) \underset{˙}{\cdot} R) = (r \underset{˙}{\cdot} (G (x) \underset{˙}{\cdot} R)) +_{D} (G (y) \underset{˙}{\cdot} R)$
54	40 50 53	3eqtrd	$⊢ (φ \land (r \in K \land x \in V \land y \in V)) \to G ((r \cdot_{W} x) +_{W} y) \underset{˙}{\cdot} R = (r \underset{˙}{\cdot} (G (x) \underset{˙}{\cdot} R)) +_{D} (G (y) \underset{˙}{\cdot} R)$
55	1 2 36 3	lmodvscl	$⊢ (W \in LMod \land r \in K \land x \in V) \to r \cdot_{W} x \in V$
56	30 32 33 55	syl3anc	$⊢ (φ \land (r \in K \land x \in V \land y \in V)) \to r \cdot_{W} x \in V$
57	1 35	lmodvacl	$⊢ (W \in LMod \land r \cdot_{W} x \in V \land y \in V) \to (r \cdot_{W} x) +_{W} y \in V$
58	30 56 34 57	syl3anc	$⊢ (φ \land (r \in K \land x \in V \land y \in V)) \to (r \cdot_{W} x) +_{W} y \in V$
59	23	ffnd	$⊢ φ \to G Fn V$
60		eqidd	$⊢ (φ \land (r \cdot_{W} x) +_{W} y \in V) \to G ((r \cdot_{W} x) +_{W} y) = G ((r \cdot_{W} x) +_{W} y)$
61	27 8 59 60	ofc2	$⊢ (φ \land (r \cdot_{W} x) +_{W} y \in V) \to (G {\underset{˙}{\cdot}}_{f} (V \times \{R\})) ((r \cdot_{W} x) +_{W} y) = G ((r \cdot_{W} x) +_{W} y) \underset{˙}{\cdot} R$
62	58 61	syldan	$⊢ (φ \land (r \in K \land x \in V \land y \in V)) \to (G {\underset{˙}{\cdot}}_{f} (V \times \{R\})) ((r \cdot_{W} x) +_{W} y) = G ((r \cdot_{W} x) +_{W} y) \underset{˙}{\cdot} R$
63		eqidd	$⊢ (φ \land x \in V) \to G (x) = G (x)$
64	27 8 59 63	ofc2	$⊢ (φ \land x \in V) \to (G {\underset{˙}{\cdot}}_{f} (V \times \{R\})) (x) = G (x) \underset{˙}{\cdot} R$
65	33 64	syldan	$⊢ (φ \land (r \in K \land x \in V \land y \in V)) \to (G {\underset{˙}{\cdot}}_{f} (V \times \{R\})) (x) = G (x) \underset{˙}{\cdot} R$
66	65	oveq2d	$⊢ (φ \land (r \in K \land x \in V \land y \in V)) \to r \underset{˙}{\cdot} (G {\underset{˙}{\cdot}}_{f} (V \times \{R\})) (x) = r \underset{˙}{\cdot} (G (x) \underset{˙}{\cdot} R)$
67		eqidd	$⊢ (φ \land y \in V) \to G (y) = G (y)$
68	27 8 59 67	ofc2	$⊢ (φ \land y \in V) \to (G {\underset{˙}{\cdot}}_{f} (V \times \{R\})) (y) = G (y) \underset{˙}{\cdot} R$
69	34 68	syldan	$⊢ (φ \land (r \in K \land x \in V \land y \in V)) \to (G {\underset{˙}{\cdot}}_{f} (V \times \{R\})) (y) = G (y) \underset{˙}{\cdot} R$
70	66 69	oveq12d	$⊢ (φ \land (r \in K \land x \in V \land y \in V)) \to (r \underset{˙}{\cdot} (G {\underset{˙}{\cdot}}_{f} (V \times \{R\})) (x)) +_{D} (G {\underset{˙}{\cdot}}_{f} (V \times \{R\})) (y) = (r \underset{˙}{\cdot} (G (x) \underset{˙}{\cdot} R)) +_{D} (G (y) \underset{˙}{\cdot} R)$
71	54 62 70	3eqtr4d	$⊢ (φ \land (r \in K \land x \in V \land y \in V)) \to (G {\underset{˙}{\cdot}}_{f} (V \times \{R\})) ((r \cdot_{W} x) +_{W} y) = (r \underset{˙}{\cdot} (G {\underset{˙}{\cdot}}_{f} (V \times \{R\})) (x)) +_{D} (G {\underset{˙}{\cdot}}_{f} (V \times \{R\})) (y)$
72	9 10 11 12 13 14 15 16 29 71 6	islfld	$⊢ φ \to G {\underset{˙}{\cdot}}_{f} (V \times \{R\}) \in F$

Metamath Proof Explorer

Theorem lflvscl

Proof