Theorem sraip

Description: The inner product operation of a subring algebra. (Contributed by Thierry Arnoux, 16-Jun-2019)

	Ref	Expression
Hypotheses	srapart.a	⊢ ( 𝜑 → 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) )
	srapart.s	⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
Assertion	sraip	⊢ ( 𝜑 → ( .r ‘ 𝑊 ) = ( ·𝑖 ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		srapart.a	⊢ ( 𝜑 → 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) )
2		srapart.s	⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
3		ovex	⊢ ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) ∈ V
4		fvex	⊢ ( .r ‘ 𝑊 ) ∈ V
5		ipid	⊢ ·𝑖 = Slot ( ·𝑖 ‘ ndx )
6	5	setsid	⊢ ( ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) ∈ V ∧ ( .r ‘ 𝑊 ) ∈ V ) → ( .r ‘ 𝑊 ) = ( ·𝑖 ‘ ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) ) )
7	3 4 6	mp2an	⊢ ( .r ‘ 𝑊 ) = ( ·𝑖 ‘ ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
8	1	adantl	⊢ ( ( 𝑊 ∈ V ∧ 𝜑 ) → 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) )
9		sraval	⊢ ( ( 𝑊 ∈ V ∧ 𝑆 ⊆ ( Base ‘ 𝑊 ) ) → ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) = ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
10	2 9	sylan2	⊢ ( ( 𝑊 ∈ V ∧ 𝜑 ) → ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) = ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
11	8 10	eqtrd	⊢ ( ( 𝑊 ∈ V ∧ 𝜑 ) → 𝐴 = ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
12	11	fveq2d	⊢ ( ( 𝑊 ∈ V ∧ 𝜑 ) → ( ·𝑖 ‘ 𝐴 ) = ( ·𝑖 ‘ ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) ) )
13	7 12	eqtr4id	⊢ ( ( 𝑊 ∈ V ∧ 𝜑 ) → ( .r ‘ 𝑊 ) = ( ·𝑖 ‘ 𝐴 ) )
14	5	str0	⊢ ∅ = ( ·𝑖 ‘ ∅ )
15		fvprc	⊢ ( ¬ 𝑊 ∈ V → ( .r ‘ 𝑊 ) = ∅ )
16	15	adantr	⊢ ( ( ¬ 𝑊 ∈ V ∧ 𝜑 ) → ( .r ‘ 𝑊 ) = ∅ )
17		fv2prc	⊢ ( ¬ 𝑊 ∈ V → ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) = ∅ )
18	1 17	sylan9eqr	⊢ ( ( ¬ 𝑊 ∈ V ∧ 𝜑 ) → 𝐴 = ∅ )
19	18	fveq2d	⊢ ( ( ¬ 𝑊 ∈ V ∧ 𝜑 ) → ( ·𝑖 ‘ 𝐴 ) = ( ·𝑖 ‘ ∅ ) )
20	14 16 19	3eqtr4a	⊢ ( ( ¬ 𝑊 ∈ V ∧ 𝜑 ) → ( .r ‘ 𝑊 ) = ( ·𝑖 ‘ 𝐴 ) )
21	13 20	pm2.61ian	⊢ ( 𝜑 → ( .r ‘ 𝑊 ) = ( ·𝑖 ‘ 𝐴 ) )