lmhmvsca

Description: The pointwise scalar product of a linear function and a constant is linear, over a commutative ring. (Contributed by Mario Carneiro, 22-Sep-2015)

	Ref	Expression
Hypotheses	lmhmvsca.v	$⊢ V = {Base}_{M}$
	lmhmvsca.s	$⊢ \underset{˙}{\cdot} = \cdot_{N}$
	lmhmvsca.j	$⊢ J = Scalar (N)$
	lmhmvsca.k	$⊢ K = {Base}_{J}$
Assertion	lmhmvsca	$⊢ (J \in CRing \land A \in K \land F \in (M LMHom N)) \to (V \times \{A\}) {\underset{˙}{\cdot}}_{f} F \in (M LMHom N)$

Proof

Step	Hyp	Ref	Expression
1		lmhmvsca.v	$⊢ V = {Base}_{M}$
2		lmhmvsca.s	$⊢ \underset{˙}{\cdot} = \cdot_{N}$
3		lmhmvsca.j	$⊢ J = Scalar (N)$
4		lmhmvsca.k	$⊢ K = {Base}_{J}$
5		eqid	$⊢ \cdot_{M} = \cdot_{M}$
6		eqid	$⊢ Scalar (M) = Scalar (M)$
7		eqid	$⊢ {Base}_{Scalar (M)} = {Base}_{Scalar (M)}$
8		lmhmlmod1	$⊢ F \in (M LMHom N) \to M \in LMod$
9	8	3ad2ant3	$⊢ (J \in CRing \land A \in K \land F \in (M LMHom N)) \to M \in LMod$
10		lmhmlmod2	$⊢ F \in (M LMHom N) \to N \in LMod$
11	10	3ad2ant3	$⊢ (J \in CRing \land A \in K \land F \in (M LMHom N)) \to N \in LMod$
12	6 3	lmhmsca	$⊢ F \in (M LMHom N) \to J = Scalar (M)$
13	12	3ad2ant3	$⊢ (J \in CRing \land A \in K \land F \in (M LMHom N)) \to J = Scalar (M)$
14	1	fvexi	$⊢ V \in V$
15	14	a1i	$⊢ (J \in CRing \land A \in K \land F \in (M LMHom N)) \to V \in V$
16		simpl2	$⊢ ((J \in CRing \land A \in K \land F \in (M LMHom N)) \land v \in V) \to A \in K$
17		eqid	$⊢ {Base}_{N} = {Base}_{N}$
18	1 17	lmhmf	$⊢ F \in (M LMHom N) \to F : V ⟶ {Base}_{N}$
19	18	3ad2ant3	$⊢ (J \in CRing \land A \in K \land F \in (M LMHom N)) \to F : V ⟶ {Base}_{N}$
20	19	ffvelrnda	$⊢ ((J \in CRing \land A \in K \land F \in (M LMHom N)) \land v \in V) \to F (v) \in {Base}_{N}$
21		fconstmpt	$⊢ V \times \{A\} = (v \in V ⟼ A)$
22	21	a1i	$⊢ (J \in CRing \land A \in K \land F \in (M LMHom N)) \to V \times \{A\} = (v \in V ⟼ A)$
23	19	feqmptd	$⊢ (J \in CRing \land A \in K \land F \in (M LMHom N)) \to F = (v \in V ⟼ F (v))$
24	15 16 20 22 23	offval2	$⊢ (J \in CRing \land A \in K \land F \in (M LMHom N)) \to (V \times \{A\}) {\underset{˙}{\cdot}}_{f} F = (v \in V ⟼ A \underset{˙}{\cdot} F (v))$
25		eqidd	$⊢ (J \in CRing \land A \in K \land F \in (M LMHom N)) \to (u \in {Base}_{N} ⟼ A \underset{˙}{\cdot} u) = (u \in {Base}_{N} ⟼ A \underset{˙}{\cdot} u)$
26		oveq2	$⊢ u = F (v) \to A \underset{˙}{\cdot} u = A \underset{˙}{\cdot} F (v)$
27	20 23 25 26	fmptco	$⊢ (J \in CRing \land A \in K \land F \in (M LMHom N)) \to (u \in {Base}_{N} ⟼ A \underset{˙}{\cdot} u) \circ F = (v \in V ⟼ A \underset{˙}{\cdot} F (v))$
28	24 27	eqtr4d	$⊢ (J \in CRing \land A \in K \land F \in (M LMHom N)) \to (V \times \{A\}) {\underset{˙}{\cdot}}_{f} F = (u \in {Base}_{N} ⟼ A \underset{˙}{\cdot} u) \circ F$
29		simp2	$⊢ (J \in CRing \land A \in K \land F \in (M LMHom N)) \to A \in K$
30	17 3 2 4	lmodvsghm	$⊢ (N \in LMod \land A \in K) \to (u \in {Base}_{N} ⟼ A \underset{˙}{\cdot} u) \in (N GrpHom N)$
31	11 29 30	syl2anc	$⊢ (J \in CRing \land A \in K \land F \in (M LMHom N)) \to (u \in {Base}_{N} ⟼ A \underset{˙}{\cdot} u) \in (N GrpHom N)$
32		lmghm	$⊢ F \in (M LMHom N) \to F \in (M GrpHom N)$
33	32	3ad2ant3	$⊢ (J \in CRing \land A \in K \land F \in (M LMHom N)) \to F \in (M GrpHom N)$
34		ghmco	$⊢ ((u \in {Base}_{N} ⟼ A \underset{˙}{\cdot} u) \in (N GrpHom N) \land F \in (M GrpHom N)) \to (u \in {Base}_{N} ⟼ A \underset{˙}{\cdot} u) \circ F \in (M GrpHom N)$
35	31 33 34	syl2anc	$⊢ (J \in CRing \land A \in K \land F \in (M LMHom N)) \to (u \in {Base}_{N} ⟼ A \underset{˙}{\cdot} u) \circ F \in (M GrpHom N)$
36	28 35	eqeltrd	$⊢ (J \in CRing \land A \in K \land F \in (M LMHom N)) \to (V \times \{A\}) {\underset{˙}{\cdot}}_{f} F \in (M GrpHom N)$
37		simpl1	$⊢ ((J \in CRing \land A \in K \land F \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in V)) \to J \in CRing$
38		simpl2	$⊢ ((J \in CRing \land A \in K \land F \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in V)) \to A \in K$
39		simprl	$⊢ ((J \in CRing \land A \in K \land F \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in V)) \to x \in {Base}_{Scalar (M)}$
40	13	fveq2d	$⊢ (J \in CRing \land A \in K \land F \in (M LMHom N)) \to {Base}_{J} = {Base}_{Scalar (M)}$
41	4 40	syl5eq	$⊢ (J \in CRing \land A \in K \land F \in (M LMHom N)) \to K = {Base}_{Scalar (M)}$
42	41	adantr	$⊢ ((J \in CRing \land A \in K \land F \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in V)) \to K = {Base}_{Scalar (M)}$
43	39 42	eleqtrrd	$⊢ ((J \in CRing \land A \in K \land F \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in V)) \to x \in K$
44		eqid	$⊢ \cdot_{J} = \cdot_{J}$
45	4 44	crngcom	$⊢ (J \in CRing \land A \in K \land x \in K) \to A \cdot_{J} x = x \cdot_{J} A$
46	37 38 43 45	syl3anc	$⊢ ((J \in CRing \land A \in K \land F \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in V)) \to A \cdot_{J} x = x \cdot_{J} A$
47	46	oveq1d	$⊢ ((J \in CRing \land A \in K \land F \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in V)) \to (A \cdot_{J} x) \underset{˙}{\cdot} F (y) = (x \cdot_{J} A) \underset{˙}{\cdot} F (y)$
48	11	adantr	$⊢ ((J \in CRing \land A \in K \land F \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in V)) \to N \in LMod$
49	19	adantr	$⊢ ((J \in CRing \land A \in K \land F \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in V)) \to F : V ⟶ {Base}_{N}$
50		simprr	$⊢ ((J \in CRing \land A \in K \land F \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in V)) \to y \in V$
51	49 50	ffvelrnd	$⊢ ((J \in CRing \land A \in K \land F \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in V)) \to F (y) \in {Base}_{N}$
52	17 3 2 4 44	lmodvsass	$⊢ (N \in LMod \land (A \in K \land x \in K \land F (y) \in {Base}_{N})) \to (A \cdot_{J} x) \underset{˙}{\cdot} F (y) = A \underset{˙}{\cdot} (x \underset{˙}{\cdot} F (y))$
53	48 38 43 51 52	syl13anc	$⊢ ((J \in CRing \land A \in K \land F \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in V)) \to (A \cdot_{J} x) \underset{˙}{\cdot} F (y) = A \underset{˙}{\cdot} (x \underset{˙}{\cdot} F (y))$
54	17 3 2 4 44	lmodvsass	$⊢ (N \in LMod \land (x \in K \land A \in K \land F (y) \in {Base}_{N})) \to (x \cdot_{J} A) \underset{˙}{\cdot} F (y) = x \underset{˙}{\cdot} (A \underset{˙}{\cdot} F (y))$
55	48 43 38 51 54	syl13anc	$⊢ ((J \in CRing \land A \in K \land F \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in V)) \to (x \cdot_{J} A) \underset{˙}{\cdot} F (y) = x \underset{˙}{\cdot} (A \underset{˙}{\cdot} F (y))$
56	47 53 55	3eqtr3d	$⊢ ((J \in CRing \land A \in K \land F \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in V)) \to A \underset{˙}{\cdot} (x \underset{˙}{\cdot} F (y)) = x \underset{˙}{\cdot} (A \underset{˙}{\cdot} F (y))$
57	1 6 5 7	lmodvscl	$⊢ (M \in LMod \land x \in {Base}_{Scalar (M)} \land y \in V) \to x \cdot_{M} y \in V$
58	57	3expb	$⊢ (M \in LMod \land (x \in {Base}_{Scalar (M)} \land y \in V)) \to x \cdot_{M} y \in V$
59	9 58	sylan	$⊢ ((J \in CRing \land A \in K \land F \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in V)) \to x \cdot_{M} y \in V$
60	14	a1i	$⊢ ((J \in CRing \land A \in K \land F \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in V)) \to V \in V$
61	19	ffnd	$⊢ (J \in CRing \land A \in K \land F \in (M LMHom N)) \to F Fn V$
62	61	adantr	$⊢ ((J \in CRing \land A \in K \land F \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in V)) \to F Fn V$
63	6 7 1 5 2	lmhmlin	$⊢ (F \in (M LMHom N) \land x \in {Base}_{Scalar (M)} \land y \in V) \to F (x \cdot_{M} y) = x \underset{˙}{\cdot} F (y)$
64	63	3expb	$⊢ (F \in (M LMHom N) \land (x \in {Base}_{Scalar (M)} \land y \in V)) \to F (x \cdot_{M} y) = x \underset{˙}{\cdot} F (y)$
65	64	3ad2antl3	$⊢ ((J \in CRing \land A \in K \land F \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in V)) \to F (x \cdot_{M} y) = x \underset{˙}{\cdot} F (y)$
66	65	adantr	$⊢ (((J \in CRing \land A \in K \land F \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in V)) \land x \cdot_{M} y \in V) \to F (x \cdot_{M} y) = x \underset{˙}{\cdot} F (y)$
67	60 38 62 66	ofc1	$⊢ (((J \in CRing \land A \in K \land F \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in V)) \land x \cdot_{M} y \in V) \to ((V \times \{A\}) {\underset{˙}{\cdot}}_{f} F) (x \cdot_{M} y) = A \underset{˙}{\cdot} (x \underset{˙}{\cdot} F (y))$
68	59 67	mpdan	$⊢ ((J \in CRing \land A \in K \land F \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in V)) \to ((V \times \{A\}) {\underset{˙}{\cdot}}_{f} F) (x \cdot_{M} y) = A \underset{˙}{\cdot} (x \underset{˙}{\cdot} F (y))$
69		eqidd	$⊢ (((J \in CRing \land A \in K \land F \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in V)) \land y \in V) \to F (y) = F (y)$
70	60 38 62 69	ofc1	$⊢ (((J \in CRing \land A \in K \land F \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in V)) \land y \in V) \to ((V \times \{A\}) {\underset{˙}{\cdot}}_{f} F) (y) = A \underset{˙}{\cdot} F (y)$
71	50 70	mpdan	$⊢ ((J \in CRing \land A \in K \land F \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in V)) \to ((V \times \{A\}) {\underset{˙}{\cdot}}_{f} F) (y) = A \underset{˙}{\cdot} F (y)$
72	71	oveq2d	$⊢ ((J \in CRing \land A \in K \land F \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in V)) \to x \underset{˙}{\cdot} ((V \times \{A\}) {\underset{˙}{\cdot}}_{f} F) (y) = x \underset{˙}{\cdot} (A \underset{˙}{\cdot} F (y))$
73	56 68 72	3eqtr4d	$⊢ ((J \in CRing \land A \in K \land F \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in V)) \to ((V \times \{A\}) {\underset{˙}{\cdot}}_{f} F) (x \cdot_{M} y) = x \underset{˙}{\cdot} ((V \times \{A\}) {\underset{˙}{\cdot}}_{f} F) (y)$
74	1 5 2 6 3 7 9 11 13 36 73	islmhmd	$⊢ (J \in CRing \land A \in K \land F \in (M LMHom N)) \to (V \times \{A\}) {\underset{˙}{\cdot}}_{f} F \in (M LMHom N)$

Metamath Proof Explorer

Theorem lmhmvsca

Proof