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 ∧ + = · ) → 𝑉 = 𝐾 )