Theorem lvecprop2d

Description: If two structures have the same components (properties), one is a left vector space iff the other one is. This version of lvecpropd also breaks up the components of the scalar ring. (Contributed by Mario Carneiro, 27-Jun-2015)

	Ref	Expression
Hypotheses	lvecprop2d.b1	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
	lvecprop2d.b2	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
	lvecprop2d.f	⊢ 𝐹 = ( Scalar ‘ 𝐾 )
	lvecprop2d.g	⊢ 𝐺 = ( Scalar ‘ 𝐿 )
	lvecprop2d.p1	⊢ ( 𝜑 → 𝑃 = ( Base ‘ 𝐹 ) )
	lvecprop2d.p2	⊢ ( 𝜑 → 𝑃 = ( Base ‘ 𝐺 ) )
	lvecprop2d.1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
	lvecprop2d.2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) → ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) )
	lvecprop2d.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) → ( 𝑥 ( .r ‘ 𝐹 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐺 ) 𝑦 ) )
	lvecprop2d.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝐿 ) 𝑦 ) )
Assertion	lvecprop2d	⊢ ( 𝜑 → ( 𝐾 ∈ LVec ↔ 𝐿 ∈ LVec ) )

Proof

Step	Hyp	Ref	Expression
1		lvecprop2d.b1	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
2		lvecprop2d.b2	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
3		lvecprop2d.f	⊢ 𝐹 = ( Scalar ‘ 𝐾 )
4		lvecprop2d.g	⊢ 𝐺 = ( Scalar ‘ 𝐿 )
5		lvecprop2d.p1	⊢ ( 𝜑 → 𝑃 = ( Base ‘ 𝐹 ) )
6		lvecprop2d.p2	⊢ ( 𝜑 → 𝑃 = ( Base ‘ 𝐺 ) )
7		lvecprop2d.1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
8		lvecprop2d.2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) → ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) )
9		lvecprop2d.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃 ) ) → ( 𝑥 ( .r ‘ 𝐹 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐺 ) 𝑦 ) )
10		lvecprop2d.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝐿 ) 𝑦 ) )
11	1 2 3 4 5 6 7 8 9 10	lmodprop2d	⊢ ( 𝜑 → ( 𝐾 ∈ LMod ↔ 𝐿 ∈ LMod ) )
12	5 6 8 9	drngpropd	⊢ ( 𝜑 → ( 𝐹 ∈ DivRing ↔ 𝐺 ∈ DivRing ) )
13	11 12	anbi12d	⊢ ( 𝜑 → ( ( 𝐾 ∈ LMod ∧ 𝐹 ∈ DivRing ) ↔ ( 𝐿 ∈ LMod ∧ 𝐺 ∈ DivRing ) ) )
14	3	islvec	⊢ ( 𝐾 ∈ LVec ↔ ( 𝐾 ∈ LMod ∧ 𝐹 ∈ DivRing ) )
15	4	islvec	⊢ ( 𝐿 ∈ LVec ↔ ( 𝐿 ∈ LMod ∧ 𝐺 ∈ DivRing ) )
16	13 14 15	3bitr4g	⊢ ( 𝜑 → ( 𝐾 ∈ LVec ↔ 𝐿 ∈ LVec ) )