Metamath Proof Explorer

Theorem prjsperref

Description: The relation in PrjSp is reflexive. (Contributed by Steven Nguyen, 30-Apr-2023)

Ref Expression
Hypotheses prjsprel.1 ⊢ ∼ ˙ = x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ K x = l · ˙ y
prjspertr.b ⊢ B = Base V ∖ 0 V
prjspertr.s ⊢ S = Scalar ⁡ V
prjspertr.x ⊢ · ˙ = ⋅ V
prjspertr.k ⊢ K = Base S
Assertion prjsperref ⊢ V ∈ LMod → X ∈ B ↔ X ∼ ˙ X

Proof

Step Hyp Ref Expression
1 prjsprel.1 ⊢ ∼ ˙ = x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ K x = l · ˙ y
2 prjspertr.b ⊢ B = Base V ∖ 0 V
3 prjspertr.s ⊢ S = Scalar ⁡ V
4 prjspertr.x ⊢ · ˙ = ⋅ V
5 prjspertr.k ⊢ K = Base S
6 eqid ⊢ 1 S = 1 S
7 3 5 6 lmod1cl ⊢ V ∈ LMod → 1 S ∈ K
8 7 adantr ⊢ V ∈ LMod ∧ X ∈ B → 1 S ∈ K
9 oveq1 ⊢ m = 1 S → m · ˙ X = 1 S · ˙ X
10 9 eqeq2d ⊢ m = 1 S → X = m · ˙ X ↔ X = 1 S · ˙ X
11 10 adantl ⊢ V ∈ LMod ∧ X ∈ B ∧ m = 1 S → X = m · ˙ X ↔ X = 1 S · ˙ X
12 eldifi ⊢ X ∈ Base V ∖ 0 V → X ∈ Base V
13 12 2 eleq2s ⊢ X ∈ B → X ∈ Base V
14 eqid ⊢ Base V = Base V
15 14 3 4 6 lmodvs1 ⊢ V ∈ LMod ∧ X ∈ Base V → 1 S · ˙ X = X
16 13 15 sylan2 ⊢ V ∈ LMod ∧ X ∈ B → 1 S · ˙ X = X
17 16 eqcomd ⊢ V ∈ LMod ∧ X ∈ B → X = 1 S · ˙ X
18 8 11 17 rspcedvd ⊢ V ∈ LMod ∧ X ∈ B → ∃ m ∈ K X = m · ˙ X
19 18 ex ⊢ V ∈ LMod → X ∈ B → ∃ m ∈ K X = m · ˙ X
20 19 pm4.71d ⊢ V ∈ LMod → X ∈ B ↔ X ∈ B ∧ ∃ m ∈ K X = m · ˙ X
21 pm4.24 ⊢ X ∈ B ↔ X ∈ B ∧ X ∈ B
22 21 anbi1i ⊢ X ∈ B ∧ ∃ m ∈ K X = m · ˙ X ↔ X ∈ B ∧ X ∈ B ∧ ∃ m ∈ K X = m · ˙ X
23 1 prjsprel ⊢ X ∼ ˙ X ↔ X ∈ B ∧ X ∈ B ∧ ∃ m ∈ K X = m · ˙ X
24 22 23 bitr4i ⊢ X ∈ B ∧ ∃ m ∈ K X = m · ˙ X ↔ X ∼ ˙ X
25 20 24 bitrdi ⊢ V ∈ LMod → X ∈ B ↔ X ∼ ˙ X