pwsdiaglmhm

Description: Diagonal homomorphism into a structure power. (Contributed by Stefan O'Rear, 24-Jan-2015)

	Ref	Expression
Hypotheses	pwsdiaglmhm.y	$⊢ Y = R ↑_{𝑠} I$
	pwsdiaglmhm.b	$⊢ B = {Base}_{R}$
	pwsdiaglmhm.f	$⊢ F = (x \in B ⟼ I \times \{x\})$
Assertion	pwsdiaglmhm	$⊢ (R \in LMod \land I \in W) \to F \in (R LMHom Y)$

Proof

Step	Hyp	Ref	Expression
1		pwsdiaglmhm.y	$⊢ Y = R ↑_{𝑠} I$
2		pwsdiaglmhm.b	$⊢ B = {Base}_{R}$
3		pwsdiaglmhm.f	$⊢ F = (x \in B ⟼ I \times \{x\})$
4		eqid	$⊢ \cdot_{R} = \cdot_{R}$
5		eqid	$⊢ \cdot_{Y} = \cdot_{Y}$
6		eqid	$⊢ Scalar (R) = Scalar (R)$
7		eqid	$⊢ Scalar (Y) = Scalar (Y)$
8		eqid	$⊢ {Base}_{Scalar (R)} = {Base}_{Scalar (R)}$
9		simpl	$⊢ (R \in LMod \land I \in W) \to R \in LMod$
10	1	pwslmod	$⊢ (R \in LMod \land I \in W) \to Y \in LMod$
11	1 6	pwssca	$⊢ (R \in LMod \land I \in W) \to Scalar (R) = Scalar (Y)$
12	11	eqcomd	$⊢ (R \in LMod \land I \in W) \to Scalar (Y) = Scalar (R)$
13		lmodgrp	$⊢ R \in LMod \to R \in Grp$
14	1 2 3	pwsdiagghm	$⊢ (R \in Grp \land I \in W) \to F \in (R GrpHom Y)$
15	13 14	sylan	$⊢ (R \in LMod \land I \in W) \to F \in (R GrpHom Y)$
16		simplr	$⊢ ((R \in LMod \land I \in W) \land (a \in {Base}_{Scalar (R)} \land b \in B)) \to I \in W$
17	2 6 4 8	lmodvscl	$⊢ (R \in LMod \land a \in {Base}_{Scalar (R)} \land b \in B) \to a \cdot_{R} b \in B$
18	17	3expb	$⊢ (R \in LMod \land (a \in {Base}_{Scalar (R)} \land b \in B)) \to a \cdot_{R} b \in B$
19	18	adantlr	$⊢ ((R \in LMod \land I \in W) \land (a \in {Base}_{Scalar (R)} \land b \in B)) \to a \cdot_{R} b \in B$
20	3	fvdiagfn	$⊢ (I \in W \land a \cdot_{R} b \in B) \to F (a \cdot_{R} b) = I \times \{a \cdot_{R} b\}$
21	16 19 20	syl2anc	$⊢ ((R \in LMod \land I \in W) \land (a \in {Base}_{Scalar (R)} \land b \in B)) \to F (a \cdot_{R} b) = I \times \{a \cdot_{R} b\}$
22	3	fvdiagfn	$⊢ (I \in W \land b \in B) \to F (b) = I \times \{b\}$
23	22	ad2ant2l	$⊢ ((R \in LMod \land I \in W) \land (a \in {Base}_{Scalar (R)} \land b \in B)) \to F (b) = I \times \{b\}$
24	23	oveq2d	$⊢ ((R \in LMod \land I \in W) \land (a \in {Base}_{Scalar (R)} \land b \in B)) \to a \cdot_{Y} F (b) = a \cdot_{Y} (I \times \{b\})$
25		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
26		simpll	$⊢ ((R \in LMod \land I \in W) \land (a \in {Base}_{Scalar (R)} \land b \in B)) \to R \in LMod$
27		simprl	$⊢ ((R \in LMod \land I \in W) \land (a \in {Base}_{Scalar (R)} \land b \in B)) \to a \in {Base}_{Scalar (R)}$
28	1 2 25	pwsdiagel	$⊢ ((R \in LMod \land I \in W) \land b \in B) \to I \times \{b\} \in {Base}_{Y}$
29	28	adantrl	$⊢ ((R \in LMod \land I \in W) \land (a \in {Base}_{Scalar (R)} \land b \in B)) \to I \times \{b\} \in {Base}_{Y}$
30	1 25 4 5 6 8 26 16 27 29	pwsvscafval	$⊢ ((R \in LMod \land I \in W) \land (a \in {Base}_{Scalar (R)} \land b \in B)) \to a \cdot_{Y} (I \times \{b\}) = (I \times \{a\}) {\cdot_{R}}_{f} (I \times \{b\})$
31		id	$⊢ I \in W \to I \in W$
32		vex	$⊢ a \in V$
33	32	a1i	$⊢ I \in W \to a \in V$
34		vex	$⊢ b \in V$
35	34	a1i	$⊢ I \in W \to b \in V$
36	31 33 35	ofc12	$⊢ I \in W \to (I \times \{a\}) {\cdot_{R}}_{f} (I \times \{b\}) = I \times \{a \cdot_{R} b\}$
37	36	ad2antlr	$⊢ ((R \in LMod \land I \in W) \land (a \in {Base}_{Scalar (R)} \land b \in B)) \to (I \times \{a\}) {\cdot_{R}}_{f} (I \times \{b\}) = I \times \{a \cdot_{R} b\}$
38	24 30 37	3eqtrd	$⊢ ((R \in LMod \land I \in W) \land (a \in {Base}_{Scalar (R)} \land b \in B)) \to a \cdot_{Y} F (b) = I \times \{a \cdot_{R} b\}$
39	21 38	eqtr4d	$⊢ ((R \in LMod \land I \in W) \land (a \in {Base}_{Scalar (R)} \land b \in B)) \to F (a \cdot_{R} b) = a \cdot_{Y} F (b)$
40	2 4 5 6 7 8 9 10 12 15 39	islmhmd	$⊢ (R \in LMod \land I \in W) \to F \in (R LMHom Y)$

Metamath Proof Explorer

Theorem pwsdiaglmhm

Proof