lmodpropd

Description: If two structures have the same components (properties), one is a left module iff the other one is. (Contributed by Mario Carneiro, 8-Feb-2015) (Revised by Mario Carneiro, 27-Jun-2015)

	Ref	Expression
Hypotheses	lmodpropd.1	$⊢ φ \to B = {Base}_{K}$
	lmodpropd.2	$⊢ φ \to B = {Base}_{L}$
	lmodpropd.3	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{K} y = x +_{L} y$
	lmodpropd.4	$⊢ φ \to F = Scalar (K)$
	lmodpropd.5	$⊢ φ \to F = Scalar (L)$
	lmodpropd.6	$⊢ P = {Base}_{F}$
	lmodpropd.7	$⊢ (φ \land (x \in P \land y \in B)) \to x \cdot_{K} y = x \cdot_{L} y$
Assertion	lmodpropd	$⊢ φ \to (K \in LMod \leftrightarrow L \in LMod)$

Proof

Step	Hyp	Ref	Expression
1		lmodpropd.1	$⊢ φ \to B = {Base}_{K}$
2		lmodpropd.2	$⊢ φ \to B = {Base}_{L}$
3		lmodpropd.3	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{K} y = x +_{L} y$
4		lmodpropd.4	$⊢ φ \to F = Scalar (K)$
5		lmodpropd.5	$⊢ φ \to F = Scalar (L)$
6		lmodpropd.6	$⊢ P = {Base}_{F}$
7		lmodpropd.7	$⊢ (φ \land (x \in P \land y \in B)) \to x \cdot_{K} y = x \cdot_{L} y$
8		eqid	$⊢ Scalar (K) = Scalar (K)$
9		eqid	$⊢ Scalar (L) = Scalar (L)$
10	4	fveq2d	$⊢ φ \to {Base}_{F} = {Base}_{Scalar (K)}$
11	6 10	eqtrid	$⊢ φ \to P = {Base}_{Scalar (K)}$
12	5	fveq2d	$⊢ φ \to {Base}_{F} = {Base}_{Scalar (L)}$
13	6 12	eqtrid	$⊢ φ \to P = {Base}_{Scalar (L)}$
14	4 5	eqtr3d	$⊢ φ \to Scalar (K) = Scalar (L)$
15	14	adantr	$⊢ (φ \land (x \in P \land y \in P)) \to Scalar (K) = Scalar (L)$
16	15	fveq2d	$⊢ (φ \land (x \in P \land y \in P)) \to +_{Scalar (K)} = +_{Scalar (L)}$
17	16	oveqd	$⊢ (φ \land (x \in P \land y \in P)) \to x +_{Scalar (K)} y = x +_{Scalar (L)} y$
18	15	fveq2d	$⊢ (φ \land (x \in P \land y \in P)) \to \cdot_{Scalar (K)} = \cdot_{Scalar (L)}$
19	18	oveqd	$⊢ (φ \land (x \in P \land y \in P)) \to x \cdot_{Scalar (K)} y = x \cdot_{Scalar (L)} y$
20	1 2 8 9 11 13 3 17 19 7	lmodprop2d	$⊢ φ \to (K \in LMod \leftrightarrow L \in LMod)$

Metamath Proof Explorer

Theorem lmodpropd

Proof