Theorem lvecpropd

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

	Ref	Expression
Hypotheses	lvecpropd.1	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
	lvecpropd.2	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
	lvecpropd.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
	lvecpropd.4	⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝐾 ) )
	lvecpropd.5	⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝐿 ) )
	lvecpropd.6	⊢ 𝑃 = ( Base ‘ 𝐹 )
	lvecpropd.7	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝐿 ) 𝑦 ) )
Assertion	lvecpropd	⊢ ( 𝜑 → ( 𝐾 ∈ LVec ↔ 𝐿 ∈ LVec ) )

Proof

Step	Hyp	Ref	Expression
1		lvecpropd.1	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
2		lvecpropd.2	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
3		lvecpropd.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
4		lvecpropd.4	⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝐾 ) )
5		lvecpropd.5	⊢ ( 𝜑 → 𝐹 = ( Scalar ‘ 𝐿 ) )
6		lvecpropd.6	⊢ 𝑃 = ( Base ‘ 𝐹 )
7		lvecpropd.7	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝐿 ) 𝑦 ) )
8	1 2 3 4 5 6 7	lmodpropd	⊢ ( 𝜑 → ( 𝐾 ∈ LMod ↔ 𝐿 ∈ LMod ) )
9	4 5	eqtr3d	⊢ ( 𝜑 → ( Scalar ‘ 𝐾 ) = ( Scalar ‘ 𝐿 ) )
10	9	eleq1d	⊢ ( 𝜑 → ( ( Scalar ‘ 𝐾 ) ∈ DivRing ↔ ( Scalar ‘ 𝐿 ) ∈ DivRing ) )
11	8 10	anbi12d	⊢ ( 𝜑 → ( ( 𝐾 ∈ LMod ∧ ( Scalar ‘ 𝐾 ) ∈ DivRing ) ↔ ( 𝐿 ∈ LMod ∧ ( Scalar ‘ 𝐿 ) ∈ DivRing ) ) )
12		eqid	⊢ ( Scalar ‘ 𝐾 ) = ( Scalar ‘ 𝐾 )
13	12	islvec	⊢ ( 𝐾 ∈ LVec ↔ ( 𝐾 ∈ LMod ∧ ( Scalar ‘ 𝐾 ) ∈ DivRing ) )
14		eqid	⊢ ( Scalar ‘ 𝐿 ) = ( Scalar ‘ 𝐿 )
15	14	islvec	⊢ ( 𝐿 ∈ LVec ↔ ( 𝐿 ∈ LMod ∧ ( Scalar ‘ 𝐿 ) ∈ DivRing ) )
16	11 13 15	3bitr4g	⊢ ( 𝜑 → ( 𝐾 ∈ LVec ↔ 𝐿 ∈ LVec ) )