This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lmodfopnelem1

Description: Lemma 1 for lmodfopne . (Contributed by AV, 2-Oct-2021)

Ref Expression
Hypotheses lmodfopne.t ⊢ · = ( ·sf ‘ 𝑊 )
lmodfopne.a ⊢ + = ( +𝑓 ‘ 𝑊 )
lmodfopne.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lmodfopne.s ⊢ 𝑆 = ( Scalar ‘ 𝑊 )
lmodfopne.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
Assertion lmodfopnelem1 ( ( 𝑊 ∈ LMod ∧ + = · ) → 𝑉 = 𝐾 )

Proof

Step Hyp Ref Expression
1 lmodfopne.t ⊢ · = ( ·sf ‘ 𝑊 )
2 lmodfopne.a ⊢ + = ( +𝑓 ‘ 𝑊 )
3 lmodfopne.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
4 lmodfopne.s ⊢ 𝑆 = ( Scalar ‘ 𝑊 )
5 lmodfopne.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
6 3 4 5 1 lmodscaf ⊢ ( 𝑊 ∈ LMod → · : ( 𝐾 × 𝑉 ) ⟶ 𝑉 )
7 6 ffnd ⊢ ( 𝑊 ∈ LMod → · Fn ( 𝐾 × 𝑉 ) )
8 3 2 plusffn ⊢ + Fn ( 𝑉 × 𝑉 )
9 fneq1 ⊢ ( + = · → ( + Fn ( 𝑉 × 𝑉 ) ↔ · Fn ( 𝑉 × 𝑉 ) ) )
10 fndmu ⊢ ( ( · Fn ( 𝑉 × 𝑉 ) ∧ · Fn ( 𝐾 × 𝑉 ) ) → ( 𝑉 × 𝑉 ) = ( 𝐾 × 𝑉 ) )
11 10 ex ⊢ ( · Fn ( 𝑉 × 𝑉 ) → ( · Fn ( 𝐾 × 𝑉 ) → ( 𝑉 × 𝑉 ) = ( 𝐾 × 𝑉 ) ) )
12 9 11 biimtrdi ⊢ ( + = · → ( + Fn ( 𝑉 × 𝑉 ) → ( · Fn ( 𝐾 × 𝑉 ) → ( 𝑉 × 𝑉 ) = ( 𝐾 × 𝑉 ) ) ) )
13 12 com13 ⊢ ( · Fn ( 𝐾 × 𝑉 ) → ( + Fn ( 𝑉 × 𝑉 ) → ( + = · → ( 𝑉 × 𝑉 ) = ( 𝐾 × 𝑉 ) ) ) )
14 13 impcom ⊢ ( ( + Fn ( 𝑉 × 𝑉 ) ∧ · Fn ( 𝐾 × 𝑉 ) ) → ( + = · → ( 𝑉 × 𝑉 ) = ( 𝐾 × 𝑉 ) ) )
15 3 lmodbn0 ⊢ ( 𝑊 ∈ LMod → 𝑉 ≠ ∅ )
16 xp11 ⊢ ( ( 𝑉 ≠ ∅ ∧ 𝑉 ≠ ∅ ) → ( ( 𝑉 × 𝑉 ) = ( 𝐾 × 𝑉 ) ↔ ( 𝑉 = 𝐾 ∧ 𝑉 = 𝑉 ) ) )
17 15 15 16 syl2anc ⊢ ( 𝑊 ∈ LMod → ( ( 𝑉 × 𝑉 ) = ( 𝐾 × 𝑉 ) ↔ ( 𝑉 = 𝐾 ∧ 𝑉 = 𝑉 ) ) )
18 17 simprbda ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑉 × 𝑉 ) = ( 𝐾 × 𝑉 ) ) → 𝑉 = 𝐾 )
19 18 expcom ⊢ ( ( 𝑉 × 𝑉 ) = ( 𝐾 × 𝑉 ) → ( 𝑊 ∈ LMod → 𝑉 = 𝐾 ) )
20 14 19 syl6 ⊢ ( ( + Fn ( 𝑉 × 𝑉 ) ∧ · Fn ( 𝐾 × 𝑉 ) ) → ( + = · → ( 𝑊 ∈ LMod → 𝑉 = 𝐾 ) ) )
21 20 com23 ⊢ ( ( + Fn ( 𝑉 × 𝑉 ) ∧ · Fn ( 𝐾 × 𝑉 ) ) → ( 𝑊 ∈ LMod → ( + = · → 𝑉 = 𝐾 ) ) )
22 21 ex ⊢ ( + Fn ( 𝑉 × 𝑉 ) → ( · Fn ( 𝐾 × 𝑉 ) → ( 𝑊 ∈ LMod → ( + = · → 𝑉 = 𝐾 ) ) ) )
23 22 com23 ⊢ ( + Fn ( 𝑉 × 𝑉 ) → ( 𝑊 ∈ LMod → ( · Fn ( 𝐾 × 𝑉 ) → ( + = · → 𝑉 = 𝐾 ) ) ) )
24 8 23 ax-mp ⊢ ( 𝑊 ∈ LMod → ( · Fn ( 𝐾 × 𝑉 ) → ( + = · → 𝑉 = 𝐾 ) ) )
25 7 24 mpd ⊢ ( 𝑊 ∈ LMod → ( + = · → 𝑉 = 𝐾 ) )
26 25 imp ⊢ ( ( 𝑊 ∈ LMod ∧ + = · ) → 𝑉 = 𝐾 )