Metamath Proof Explorer

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 syl5eq ⊢ ( 𝜑 → 𝑃 = ( Base ‘ ( Scalar ‘ 𝐾 ) ) )
12 5 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝐹 ) = ( Base ‘ ( Scalar ‘ 𝐿 ) ) )
13 6 12 syl5eq ⊢ ( 𝜑 → 𝑃 = ( 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 ) )