lmhmpropd

Description: Module homomorphism depends only on the module attributes of structures. (Contributed by Mario Carneiro, 8-Oct-2015)

	Ref	Expression
Hypotheses	lmhmpropd.a	$⊢ φ \to B = {Base}_{J}$
	lmhmpropd.b	$⊢ φ \to C = {Base}_{K}$
	lmhmpropd.c	$⊢ φ \to B = {Base}_{L}$
	lmhmpropd.d	$⊢ φ \to C = {Base}_{M}$
	lmhmpropd.1	$⊢ φ \to F = Scalar (J)$
	lmhmpropd.2	$⊢ φ \to G = Scalar (K)$
	lmhmpropd.3	$⊢ φ \to F = Scalar (L)$
	lmhmpropd.4	$⊢ φ \to G = Scalar (M)$
	lmhmpropd.p	$⊢ P = {Base}_{F}$
	lmhmpropd.q	$⊢ Q = {Base}_{G}$
	lmhmpropd.e	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{J} y = x +_{L} y$
	lmhmpropd.f	$⊢ (φ \land (x \in C \land y \in C)) \to x +_{K} y = x +_{M} y$
	lmhmpropd.g	$⊢ (φ \land (x \in P \land y \in B)) \to x \cdot_{J} y = x \cdot_{L} y$
	lmhmpropd.h	$⊢ (φ \land (x \in Q \land y \in C)) \to x \cdot_{K} y = x \cdot_{M} y$
Assertion	lmhmpropd	$⊢ φ \to J LMHom K = L LMHom M$

Proof

Step	Hyp	Ref	Expression
1		lmhmpropd.a	$⊢ φ \to B = {Base}_{J}$
2		lmhmpropd.b	$⊢ φ \to C = {Base}_{K}$
3		lmhmpropd.c	$⊢ φ \to B = {Base}_{L}$
4		lmhmpropd.d	$⊢ φ \to C = {Base}_{M}$
5		lmhmpropd.1	$⊢ φ \to F = Scalar (J)$
6		lmhmpropd.2	$⊢ φ \to G = Scalar (K)$
7		lmhmpropd.3	$⊢ φ \to F = Scalar (L)$
8		lmhmpropd.4	$⊢ φ \to G = Scalar (M)$
9		lmhmpropd.p	$⊢ P = {Base}_{F}$
10		lmhmpropd.q	$⊢ Q = {Base}_{G}$
11		lmhmpropd.e	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{J} y = x +_{L} y$
12		lmhmpropd.f	$⊢ (φ \land (x \in C \land y \in C)) \to x +_{K} y = x +_{M} y$
13		lmhmpropd.g	$⊢ (φ \land (x \in P \land y \in B)) \to x \cdot_{J} y = x \cdot_{L} y$
14		lmhmpropd.h	$⊢ (φ \land (x \in Q \land y \in C)) \to x \cdot_{K} y = x \cdot_{M} y$
15	1 3 11 5 7 9 13	lmodpropd	$⊢ φ \to (J \in LMod \leftrightarrow L \in LMod)$
16	2 4 12 6 8 10 14	lmodpropd	$⊢ φ \to (K \in LMod \leftrightarrow M \in LMod)$
17	15 16	anbi12d	$⊢ φ \to ((J \in LMod \land K \in LMod) \leftrightarrow (L \in LMod \land M \in LMod))$
18	13	oveqrspc2v	$⊢ (φ \land (z \in P \land w \in B)) \to z \cdot_{J} w = z \cdot_{L} w$
19	18	adantlr	$⊢ ((φ \land (f \in (J GrpHom K) \land G = F)) \land (z \in P \land w \in B)) \to z \cdot_{J} w = z \cdot_{L} w$
20	19	fveq2d	$⊢ ((φ \land (f \in (J GrpHom K) \land G = F)) \land (z \in P \land w \in B)) \to f (z \cdot_{J} w) = f (z \cdot_{L} w)$
21		simpll	$⊢ ((φ \land (f \in (J GrpHom K) \land G = F)) \land (z \in P \land w \in B)) \to φ$
22		simprl	$⊢ ((φ \land (f \in (J GrpHom K) \land G = F)) \land (z \in P \land w \in B)) \to z \in P$
23		simplrr	$⊢ ((φ \land (f \in (J GrpHom K) \land G = F)) \land (z \in P \land w \in B)) \to G = F$
24	23	fveq2d	$⊢ ((φ \land (f \in (J GrpHom K) \land G = F)) \land (z \in P \land w \in B)) \to {Base}_{G} = {Base}_{F}$
25	24 10 9	3eqtr4g	$⊢ ((φ \land (f \in (J GrpHom K) \land G = F)) \land (z \in P \land w \in B)) \to Q = P$
26	22 25	eleqtrrd	$⊢ ((φ \land (f \in (J GrpHom K) \land G = F)) \land (z \in P \land w \in B)) \to z \in Q$
27		simplrl	$⊢ ((φ \land (f \in (J GrpHom K) \land G = F)) \land (z \in P \land w \in B)) \to f \in (J GrpHom K)$
28		eqid	$⊢ {Base}_{J} = {Base}_{J}$
29		eqid	$⊢ {Base}_{K} = {Base}_{K}$
30	28 29	ghmf	$⊢ f \in (J GrpHom K) \to f : {Base}_{J} ⟶ {Base}_{K}$
31	27 30	syl	$⊢ ((φ \land (f \in (J GrpHom K) \land G = F)) \land (z \in P \land w \in B)) \to f : {Base}_{J} ⟶ {Base}_{K}$
32		simprr	$⊢ ((φ \land (f \in (J GrpHom K) \land G = F)) \land (z \in P \land w \in B)) \to w \in B$
33	21 1	syl	$⊢ ((φ \land (f \in (J GrpHom K) \land G = F)) \land (z \in P \land w \in B)) \to B = {Base}_{J}$
34	32 33	eleqtrd	$⊢ ((φ \land (f \in (J GrpHom K) \land G = F)) \land (z \in P \land w \in B)) \to w \in {Base}_{J}$
35	31 34	ffvelrnd	$⊢ ((φ \land (f \in (J GrpHom K) \land G = F)) \land (z \in P \land w \in B)) \to f (w) \in {Base}_{K}$
36	21 2	syl	$⊢ ((φ \land (f \in (J GrpHom K) \land G = F)) \land (z \in P \land w \in B)) \to C = {Base}_{K}$
37	35 36	eleqtrrd	$⊢ ((φ \land (f \in (J GrpHom K) \land G = F)) \land (z \in P \land w \in B)) \to f (w) \in C$
38	14	oveqrspc2v	$⊢ (φ \land (z \in Q \land f (w) \in C)) \to z \cdot_{K} f (w) = z \cdot_{M} f (w)$
39	21 26 37 38	syl12anc	$⊢ ((φ \land (f \in (J GrpHom K) \land G = F)) \land (z \in P \land w \in B)) \to z \cdot_{K} f (w) = z \cdot_{M} f (w)$
40	20 39	eqeq12d	$⊢ ((φ \land (f \in (J GrpHom K) \land G = F)) \land (z \in P \land w \in B)) \to (f (z \cdot_{J} w) = z \cdot_{K} f (w) \leftrightarrow f (z \cdot_{L} w) = z \cdot_{M} f (w))$
41	40	2ralbidva	$⊢ (φ \land (f \in (J GrpHom K) \land G = F)) \to (\forall z \in P \forall w \in B f (z \cdot_{J} w) = z \cdot_{K} f (w) \leftrightarrow \forall z \in P \forall w \in B f (z \cdot_{L} w) = z \cdot_{M} f (w))$
42	41	pm5.32da	$⊢ φ \to (((f \in (J GrpHom K) \land G = F) \land \forall z \in P \forall w \in B f (z \cdot_{J} w) = z \cdot_{K} f (w)) \leftrightarrow ((f \in (J GrpHom K) \land G = F) \land \forall z \in P \forall w \in B f (z \cdot_{L} w) = z \cdot_{M} f (w)))$
43		df-3an	$⊢ (f \in (J GrpHom K) \land G = F \land \forall z \in P \forall w \in B f (z \cdot_{J} w) = z \cdot_{K} f (w)) \leftrightarrow ((f \in (J GrpHom K) \land G = F) \land \forall z \in P \forall w \in B f (z \cdot_{J} w) = z \cdot_{K} f (w))$
44		df-3an	$⊢ (f \in (J GrpHom K) \land G = F \land \forall z \in P \forall w \in B f (z \cdot_{L} w) = z \cdot_{M} f (w)) \leftrightarrow ((f \in (J GrpHom K) \land G = F) \land \forall z \in P \forall w \in B f (z \cdot_{L} w) = z \cdot_{M} f (w))$
45	42 43 44	3bitr4g	$⊢ φ \to ((f \in (J GrpHom K) \land G = F \land \forall z \in P \forall w \in B f (z \cdot_{J} w) = z \cdot_{K} f (w)) \leftrightarrow (f \in (J GrpHom K) \land G = F \land \forall z \in P \forall w \in B f (z \cdot_{L} w) = z \cdot_{M} f (w)))$
46	6 5	eqeq12d	$⊢ φ \to (G = F \leftrightarrow Scalar (K) = Scalar (J))$
47	5	fveq2d	$⊢ φ \to {Base}_{F} = {Base}_{Scalar (J)}$
48	9 47	syl5eq	$⊢ φ \to P = {Base}_{Scalar (J)}$
49	1	raleqdv	$⊢ φ \to (\forall w \in B f (z \cdot_{J} w) = z \cdot_{K} f (w) \leftrightarrow \forall w \in {Base}_{J} f (z \cdot_{J} w) = z \cdot_{K} f (w))$
50	48 49	raleqbidv	$⊢ φ \to (\forall z \in P \forall w \in B f (z \cdot_{J} w) = z \cdot_{K} f (w) \leftrightarrow \forall z \in {Base}_{Scalar (J)} \forall w \in {Base}_{J} f (z \cdot_{J} w) = z \cdot_{K} f (w))$
51	46 50	3anbi23d	$⊢ φ \to ((f \in (J GrpHom K) \land G = F \land \forall z \in P \forall w \in B f (z \cdot_{J} w) = z \cdot_{K} f (w)) \leftrightarrow (f \in (J GrpHom K) \land Scalar (K) = Scalar (J) \land \forall z \in {Base}_{Scalar (J)} \forall w \in {Base}_{J} f (z \cdot_{J} w) = z \cdot_{K} f (w)))$
52	1 2 3 4 11 12	ghmpropd	$⊢ φ \to J GrpHom K = L GrpHom M$
53	52	eleq2d	$⊢ φ \to (f \in (J GrpHom K) \leftrightarrow f \in (L GrpHom M))$
54	8 7	eqeq12d	$⊢ φ \to (G = F \leftrightarrow Scalar (M) = Scalar (L))$
55	7	fveq2d	$⊢ φ \to {Base}_{F} = {Base}_{Scalar (L)}$
56	9 55	syl5eq	$⊢ φ \to P = {Base}_{Scalar (L)}$
57	3	raleqdv	$⊢ φ \to (\forall w \in B f (z \cdot_{L} w) = z \cdot_{M} f (w) \leftrightarrow \forall w \in {Base}_{L} f (z \cdot_{L} w) = z \cdot_{M} f (w))$
58	56 57	raleqbidv	$⊢ φ \to (\forall z \in P \forall w \in B f (z \cdot_{L} w) = z \cdot_{M} f (w) \leftrightarrow \forall z \in {Base}_{Scalar (L)} \forall w \in {Base}_{L} f (z \cdot_{L} w) = z \cdot_{M} f (w))$
59	53 54 58	3anbi123d	$⊢ φ \to ((f \in (J GrpHom K) \land G = F \land \forall z \in P \forall w \in B f (z \cdot_{L} w) = z \cdot_{M} f (w)) \leftrightarrow (f \in (L GrpHom M) \land Scalar (M) = Scalar (L) \land \forall z \in {Base}_{Scalar (L)} \forall w \in {Base}_{L} f (z \cdot_{L} w) = z \cdot_{M} f (w)))$
60	45 51 59	3bitr3d	$⊢ φ \to ((f \in (J GrpHom K) \land Scalar (K) = Scalar (J) \land \forall z \in {Base}_{Scalar (J)} \forall w \in {Base}_{J} f (z \cdot_{J} w) = z \cdot_{K} f (w)) \leftrightarrow (f \in (L GrpHom M) \land Scalar (M) = Scalar (L) \land \forall z \in {Base}_{Scalar (L)} \forall w \in {Base}_{L} f (z \cdot_{L} w) = z \cdot_{M} f (w)))$
61	17 60	anbi12d	$⊢ φ \to (((J \in LMod \land K \in LMod) \land (f \in (J GrpHom K) \land Scalar (K) = Scalar (J) \land \forall z \in {Base}_{Scalar (J)} \forall w \in {Base}_{J} f (z \cdot_{J} w) = z \cdot_{K} f (w))) \leftrightarrow ((L \in LMod \land M \in LMod) \land (f \in (L GrpHom M) \land Scalar (M) = Scalar (L) \land \forall z \in {Base}_{Scalar (L)} \forall w \in {Base}_{L} f (z \cdot_{L} w) = z \cdot_{M} f (w))))$
62		eqid	$⊢ Scalar (J) = Scalar (J)$
63		eqid	$⊢ Scalar (K) = Scalar (K)$
64		eqid	$⊢ {Base}_{Scalar (J)} = {Base}_{Scalar (J)}$
65		eqid	$⊢ \cdot_{J} = \cdot_{J}$
66		eqid	$⊢ \cdot_{K} = \cdot_{K}$
67	62 63 64 28 65 66	islmhm	$⊢ f \in (J LMHom K) \leftrightarrow ((J \in LMod \land K \in LMod) \land (f \in (J GrpHom K) \land Scalar (K) = Scalar (J) \land \forall z \in {Base}_{Scalar (J)} \forall w \in {Base}_{J} f (z \cdot_{J} w) = z \cdot_{K} f (w)))$
68		eqid	$⊢ Scalar (L) = Scalar (L)$
69		eqid	$⊢ Scalar (M) = Scalar (M)$
70		eqid	$⊢ {Base}_{Scalar (L)} = {Base}_{Scalar (L)}$
71		eqid	$⊢ {Base}_{L} = {Base}_{L}$
72		eqid	$⊢ \cdot_{L} = \cdot_{L}$
73		eqid	$⊢ \cdot_{M} = \cdot_{M}$
74	68 69 70 71 72 73	islmhm	$⊢ f \in (L LMHom M) \leftrightarrow ((L \in LMod \land M \in LMod) \land (f \in (L GrpHom M) \land Scalar (M) = Scalar (L) \land \forall z \in {Base}_{Scalar (L)} \forall w \in {Base}_{L} f (z \cdot_{L} w) = z \cdot_{M} f (w)))$
75	61 67 74	3bitr4g	$⊢ φ \to (f \in (J LMHom K) \leftrightarrow f \in (L LMHom M))$
76	75	eqrdv	$⊢ φ \to J LMHom K = L LMHom M$

Metamath Proof Explorer

Theorem lmhmpropd

Proof