lmhmco

Description: The composition of two module-linear functions is module-linear. (Contributed by Stefan O'Rear, 4-Sep-2015)

		Ref	Expression
	Assertion	lmhmco	$⊢ (F \in (N LMHom O) \land G \in (M LMHom N)) \to F \circ G \in (M LMHom O)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{M} = {Base}_{M}$
2		eqid	$⊢ \cdot_{M} = \cdot_{M}$
3		eqid	$⊢ \cdot_{O} = \cdot_{O}$
4		eqid	$⊢ Scalar (M) = Scalar (M)$
5		eqid	$⊢ Scalar (O) = Scalar (O)$
6		eqid	$⊢ {Base}_{Scalar (M)} = {Base}_{Scalar (M)}$
7		lmhmlmod1	$⊢ G \in (M LMHom N) \to M \in LMod$
8	7	adantl	$⊢ (F \in (N LMHom O) \land G \in (M LMHom N)) \to M \in LMod$
9		lmhmlmod2	$⊢ F \in (N LMHom O) \to O \in LMod$
10	9	adantr	$⊢ (F \in (N LMHom O) \land G \in (M LMHom N)) \to O \in LMod$
11		eqid	$⊢ Scalar (N) = Scalar (N)$
12	11 5	lmhmsca	$⊢ F \in (N LMHom O) \to Scalar (O) = Scalar (N)$
13	4 11	lmhmsca	$⊢ G \in (M LMHom N) \to Scalar (N) = Scalar (M)$
14	12 13	sylan9eq	$⊢ (F \in (N LMHom O) \land G \in (M LMHom N)) \to Scalar (O) = Scalar (M)$
15		lmghm	$⊢ F \in (N LMHom O) \to F \in (N GrpHom O)$
16		lmghm	$⊢ G \in (M LMHom N) \to G \in (M GrpHom N)$
17		ghmco	$⊢ (F \in (N GrpHom O) \land G \in (M GrpHom N)) \to F \circ G \in (M GrpHom O)$
18	15 16 17	syl2an	$⊢ (F \in (N LMHom O) \land G \in (M LMHom N)) \to F \circ G \in (M GrpHom O)$
19		simplr	$⊢ ((F \in (N LMHom O) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to G \in (M LMHom N)$
20		simprl	$⊢ ((F \in (N LMHom O) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to x \in {Base}_{Scalar (M)}$
21		simprr	$⊢ ((F \in (N LMHom O) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to y \in {Base}_{M}$
22		eqid	$⊢ \cdot_{N} = \cdot_{N}$
23	4 6 1 2 22	lmhmlin	$⊢ (G \in (M LMHom N) \land x \in {Base}_{Scalar (M)} \land y \in {Base}_{M}) \to G (x \cdot_{M} y) = x \cdot_{N} G (y)$
24	19 20 21 23	syl3anc	$⊢ ((F \in (N LMHom O) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to G (x \cdot_{M} y) = x \cdot_{N} G (y)$
25	24	fveq2d	$⊢ ((F \in (N LMHom O) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to F (G (x \cdot_{M} y)) = F (x \cdot_{N} G (y))$
26		simpll	$⊢ ((F \in (N LMHom O) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to F \in (N LMHom O)$
27	13	fveq2d	$⊢ G \in (M LMHom N) \to {Base}_{Scalar (N)} = {Base}_{Scalar (M)}$
28	27	ad2antlr	$⊢ ((F \in (N LMHom O) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to {Base}_{Scalar (N)} = {Base}_{Scalar (M)}$
29	20 28	eleqtrrd	$⊢ ((F \in (N LMHom O) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to x \in {Base}_{Scalar (N)}$
30		eqid	$⊢ {Base}_{N} = {Base}_{N}$
31	1 30	lmhmf	$⊢ G \in (M LMHom N) \to G : {Base}_{M} ⟶ {Base}_{N}$
32	31	adantl	$⊢ (F \in (N LMHom O) \land G \in (M LMHom N)) \to G : {Base}_{M} ⟶ {Base}_{N}$
33	32	ffvelrnda	$⊢ ((F \in (N LMHom O) \land G \in (M LMHom N)) \land y \in {Base}_{M}) \to G (y) \in {Base}_{N}$
34	33	adantrl	$⊢ ((F \in (N LMHom O) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to G (y) \in {Base}_{N}$
35		eqid	$⊢ {Base}_{Scalar (N)} = {Base}_{Scalar (N)}$
36	11 35 30 22 3	lmhmlin	$⊢ (F \in (N LMHom O) \land x \in {Base}_{Scalar (N)} \land G (y) \in {Base}_{N}) \to F (x \cdot_{N} G (y)) = x \cdot_{O} F (G (y))$
37	26 29 34 36	syl3anc	$⊢ ((F \in (N LMHom O) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to F (x \cdot_{N} G (y)) = x \cdot_{O} F (G (y))$
38	25 37	eqtrd	$⊢ ((F \in (N LMHom O) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to F (G (x \cdot_{M} y)) = x \cdot_{O} F (G (y))$
39	32	ffnd	$⊢ (F \in (N LMHom O) \land G \in (M LMHom N)) \to G Fn {Base}_{M}$
40	7	ad2antlr	$⊢ ((F \in (N LMHom O) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to M \in LMod$
41	1 4 2 6	lmodvscl	$⊢ (M \in LMod \land x \in {Base}_{Scalar (M)} \land y \in {Base}_{M}) \to x \cdot_{M} y \in {Base}_{M}$
42	40 20 21 41	syl3anc	$⊢ ((F \in (N LMHom O) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to x \cdot_{M} y \in {Base}_{M}$
43		fvco2	$⊢ (G Fn {Base}_{M} \land x \cdot_{M} y \in {Base}_{M}) \to (F \circ G) (x \cdot_{M} y) = F (G (x \cdot_{M} y))$
44	39 42 43	syl2an2r	$⊢ ((F \in (N LMHom O) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to (F \circ G) (x \cdot_{M} y) = F (G (x \cdot_{M} y))$
45		fvco2	$⊢ (G Fn {Base}_{M} \land y \in {Base}_{M}) \to (F \circ G) (y) = F (G (y))$
46	39 21 45	syl2an2r	$⊢ ((F \in (N LMHom O) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to (F \circ G) (y) = F (G (y))$
47	46	oveq2d	$⊢ ((F \in (N LMHom O) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to x \cdot_{O} (F \circ G) (y) = x \cdot_{O} F (G (y))$
48	38 44 47	3eqtr4d	$⊢ ((F \in (N LMHom O) \land G \in (M LMHom N)) \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to (F \circ G) (x \cdot_{M} y) = x \cdot_{O} (F \circ G) (y)$
49	1 2 3 4 5 6 8 10 14 18 48	islmhmd	$⊢ (F \in (N LMHom O) \land G \in (M LMHom N)) \to F \circ G \in (M LMHom O)$

Metamath Proof Explorer

Theorem lmhmco

Proof