Theorem 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	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
	lmodpropd.2	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
	lmodpropd.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
	lmodpropd.4	⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝐾 ) )
	lmodpropd.5	⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝐿 ) )
	lmodpropd.6	⊢ 𝑃 = ( Base ‘ 𝐹 )
	lmodpropd.7	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝐿 ) 𝑦 ) )
Assertion	lmodpropd	⊢ ( 𝜑 → ( 𝐾 ∈ LMod ↔ 𝐿 ∈ LMod ) )

Proof

Step	Hyp	Ref	Expression
1		lmodpropd.1	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
2		lmodpropd.2	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
3		lmodpropd.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
4		lmodpropd.4	⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝐾 ) )
5		lmodpropd.5	⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝐿 ) )
6		lmodpropd.6	⊢ 𝑃 = ( Base ‘ 𝐹 )
7		lmodpropd.7	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝐿 ) 𝑦 ) )
8		eqid	⊢ ( Scalar ‘ 𝐾 ) = ( Scalar ‘ 𝐾 )
9		eqid	⊢ ( Scalar ‘ 𝐿 ) = ( Scalar ‘ 𝐿 )
10	4	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝐹 ) = ( Base ‘ ( Scalar ‘ 𝐾 ) ) )
11	6 10	eqtrid	⊢ ( 𝜑 → 𝑃 = ( Base ‘ ( Scalar ‘ 𝐾 ) ) )
12	5	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝐹 ) = ( Base ‘ ( Scalar ‘ 𝐿 ) ) )
13	6 12	eqtrid	⊢ ( 𝜑 → 𝑃 = ( Base ‘ ( Scalar ‘ 𝐿 ) ) )
14	4 5	eqtr3d	⊢ ( 𝜑 → ( Scalar ‘ 𝐾 ) = ( Scalar ‘ 𝐿 ) )
15	14	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) → ( Scalar ‘ 𝐾 ) = ( Scalar ‘ 𝐿 ) )
16	15	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) → ( +g ‘ ( Scalar ‘ 𝐾 ) ) = ( +g ‘ ( Scalar ‘ 𝐿 ) ) )
17	16	oveqd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) → ( 𝑥 ( +g ‘ ( Scalar ‘ 𝐾 ) ) 𝑦 ) = ( 𝑥 ( +g ‘ ( Scalar ‘ 𝐿 ) ) 𝑦 ) )
18	15	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) → ( .r ‘ ( Scalar ‘ 𝐾 ) ) = ( .r ‘ ( Scalar ‘ 𝐿 ) ) )
19	18	oveqd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) → ( 𝑥 ( .r ‘ ( Scalar ‘ 𝐾 ) ) 𝑦 ) = ( 𝑥 ( .r ‘ ( Scalar ‘ 𝐿 ) ) 𝑦 ) )
20	1 2 8 9 11 13 3 17 19 7	lmodprop2d	⊢ ( 𝜑 → ( 𝐾 ∈ LMod ↔ 𝐿 ∈ LMod ) )