lmhmimasvsca

Description: Value of the scalar product of the surjective image of a module. (Contributed by Thierry Arnoux, 2-Apr-2025)

	Ref	Expression
Hypotheses	lmhmimasvsca.w	$⊢ W = F “_{𝑠} V$
	lmhmimasvsca.b	$⊢ B = {Base}_{V}$
	lmhmimasvsca.c	$⊢ C = {Base}_{W}$
	lmhmimasvsca.x	$⊢ φ \to X \in K$
	lmhmimasvsca.y	$⊢ φ \to Y \in B$
	lmhmimasvsca.1	$⊢ φ \to F : B \underset{onto}{⟶} C$
	lmhmimasvsca.f	$⊢ φ \to F \in (V LMHom W)$
	lmhmimasvsca.2	$⊢ \underset{˙}{\cdot} = \cdot_{V}$
	lmhmimasvsca.3	$⊢ \underset{˙}{\times} = \cdot_{W}$
	lmhmimasvsca.k	$⊢ K = {Base}_{Scalar (V)}$
Assertion	lmhmimasvsca	$⊢ φ \to X \underset{˙}{\times} F (Y) = F (X \underset{˙}{\cdot} Y)$

Proof

Step	Hyp	Ref	Expression
1		lmhmimasvsca.w	$⊢ W = F “_{𝑠} V$
2		lmhmimasvsca.b	$⊢ B = {Base}_{V}$
3		lmhmimasvsca.c	$⊢ C = {Base}_{W}$
4		lmhmimasvsca.x	$⊢ φ \to X \in K$
5		lmhmimasvsca.y	$⊢ φ \to Y \in B$
6		lmhmimasvsca.1	$⊢ φ \to F : B \underset{onto}{⟶} C$
7		lmhmimasvsca.f	$⊢ φ \to F \in (V LMHom W)$
8		lmhmimasvsca.2	$⊢ \underset{˙}{\cdot} = \cdot_{V}$
9		lmhmimasvsca.3	$⊢ \underset{˙}{\times} = \cdot_{W}$
10		lmhmimasvsca.k	$⊢ K = {Base}_{Scalar (V)}$
11	1	a1i	$⊢ φ \to W = F “_{𝑠} V$
12	2	a1i	$⊢ φ \to B = {Base}_{V}$
13		lmhmlmod1	$⊢ F \in (V LMHom W) \to V \in LMod$
14	7 13	syl	$⊢ φ \to V \in LMod$
15		eqid	$⊢ Scalar (V) = Scalar (V)$
16		simpr	$⊢ ((φ \land (p \in K \land a \in B \land q \in B)) \land F (a) = F (q)) \to F (a) = F (q)$
17	16	oveq2d	$⊢ ((φ \land (p \in K \land a \in B \land q \in B)) \land F (a) = F (q)) \to p \underset{˙}{\times} F (a) = p \underset{˙}{\times} F (q)$
18	7	ad2antrr	$⊢ ((φ \land (p \in K \land a \in B \land q \in B)) \land F (a) = F (q)) \to F \in (V LMHom W)$
19		simplr1	$⊢ ((φ \land (p \in K \land a \in B \land q \in B)) \land F (a) = F (q)) \to p \in K$
20		simplr2	$⊢ ((φ \land (p \in K \land a \in B \land q \in B)) \land F (a) = F (q)) \to a \in B$
21	15 10 2 8 9	lmhmlin	$⊢ (F \in (V LMHom W) \land p \in K \land a \in B) \to F (p \underset{˙}{\cdot} a) = p \underset{˙}{\times} F (a)$
22	18 19 20 21	syl3anc	$⊢ ((φ \land (p \in K \land a \in B \land q \in B)) \land F (a) = F (q)) \to F (p \underset{˙}{\cdot} a) = p \underset{˙}{\times} F (a)$
23		simplr3	$⊢ ((φ \land (p \in K \land a \in B \land q \in B)) \land F (a) = F (q)) \to q \in B$
24	15 10 2 8 9	lmhmlin	$⊢ (F \in (V LMHom W) \land p \in K \land q \in B) \to F (p \underset{˙}{\cdot} q) = p \underset{˙}{\times} F (q)$
25	18 19 23 24	syl3anc	$⊢ ((φ \land (p \in K \land a \in B \land q \in B)) \land F (a) = F (q)) \to F (p \underset{˙}{\cdot} q) = p \underset{˙}{\times} F (q)$
26	17 22 25	3eqtr4d	$⊢ ((φ \land (p \in K \land a \in B \land q \in B)) \land F (a) = F (q)) \to F (p \underset{˙}{\cdot} a) = F (p \underset{˙}{\cdot} q)$
27	26	ex	$⊢ (φ \land (p \in K \land a \in B \land q \in B)) \to (F (a) = F (q) \to F (p \underset{˙}{\cdot} a) = F (p \underset{˙}{\cdot} q))$
28	11 12 6 14 15 10 8 9 27	imasvscaval	$⊢ (φ \land X \in K \land Y \in B) \to X \underset{˙}{\times} F (Y) = F (X \underset{˙}{\cdot} Y)$
29	4 5 28	mpd3an23	$⊢ φ \to X \underset{˙}{\times} F (Y) = F (X \underset{˙}{\cdot} Y)$

Metamath Proof Explorer

Theorem lmhmimasvsca

Proof