Metamath Proof Explorer

Theorem sraip

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

Ref Expression
Hypotheses srapart.a ⊢ φ → A = subringAlg ⁡ W ⁡ S
srapart.s ⊢ φ → S ⊆ Base W
Assertion sraip ⊢ φ → ⋅ W = ⋅ 𝑖 ⁡ A

Proof

Step Hyp Ref Expression
1 srapart.a ⊢ φ → A = subringAlg ⁡ W ⁡ S
2 srapart.s ⊢ φ → S ⊆ Base W
3 ovex ⊢ W sSet Scalar ⁡ ndx W ↾ 𝑠 S sSet ⋅ ndx ⋅ W ∈ V
4 fvex ⊢ ⋅ W ∈ V
5 ipid ⊢ ⋅ 𝑖 = Slot ⋅ 𝑖 ⁡ ndx
6 5 setsid ⊢ W sSet Scalar ⁡ ndx W ↾ 𝑠 S sSet ⋅ ndx ⋅ W ∈ V ∧ ⋅ W ∈ V → ⋅ W = ⋅ 𝑖 ⁡ W sSet Scalar ⁡ ndx W ↾ 𝑠 S sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W
7 3 4 6 mp2an ⊢ ⋅ W = ⋅ 𝑖 ⁡ W sSet Scalar ⁡ ndx W ↾ 𝑠 S sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W
8 1 adantl ⊢ W ∈ V ∧ φ → A = subringAlg ⁡ W ⁡ S
9 sraval ⊢ W ∈ V ∧ S ⊆ Base W → subringAlg ⁡ W ⁡ S = W sSet Scalar ⁡ ndx W ↾ 𝑠 S sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W
10 2 9 sylan2 ⊢ W ∈ V ∧ φ → subringAlg ⁡ W ⁡ S = W sSet Scalar ⁡ ndx W ↾ 𝑠 S sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W
11 8 10 eqtrd ⊢ W ∈ V ∧ φ → A = W sSet Scalar ⁡ ndx W ↾ 𝑠 S sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W
12 11 fveq2d ⊢ W ∈ V ∧ φ → ⋅ 𝑖 ⁡ A = ⋅ 𝑖 ⁡ W sSet Scalar ⁡ ndx W ↾ 𝑠 S sSet ⋅ ndx ⋅ W sSet ⋅ 𝑖 ⁡ ndx ⋅ W
13 7 12 eqtr4id ⊢ W ∈ V ∧ φ → ⋅ W = ⋅ 𝑖 ⁡ A
14 5 str0 ⊢ ∅ = ⋅ 𝑖 ⁡ ∅
15 fvprc ⊢ ¬ W ∈ V → ⋅ W = ∅
16 15 adantr ⊢ ¬ W ∈ V ∧ φ → ⋅ W = ∅
17 fv2prc ⊢ ¬ W ∈ V → subringAlg ⁡ W ⁡ S = ∅
18 1 17 sylan9eqr ⊢ ¬ W ∈ V ∧ φ → A = ∅
19 18 fveq2d ⊢ ¬ W ∈ V ∧ φ → ⋅ 𝑖 ⁡ A = ⋅ 𝑖 ⁡ ∅
20 14 16 19 3eqtr4a ⊢ ¬ W ∈ V ∧ φ → ⋅ W = ⋅ 𝑖 ⁡ A
21 13 20 pm2.61ian ⊢ φ → ⋅ W = ⋅ 𝑖 ⁡ A