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 oveq1 ⊢ m = 1 S → m · ˙ X = 1 S · ˙ X
7 6 eqeq2d ⊢ m = 1 S → X = m · ˙ X ↔ X = 1 S · ˙ X
8 eqid ⊢ 1 S = 1 S
9 3 5 8 lmod1cl ⊢ V ∈ LMod → 1 S ∈ K
10 9 adantr ⊢ V ∈ LMod ∧ X ∈ B → 1 S ∈ K
11 eldifi ⊢ X ∈ Base V ∖ 0 V → X ∈ Base V
12 11 2 eleq2s ⊢ X ∈ B → X ∈ Base V
13 eqid ⊢ Base V = Base V
14 13 3 4 8 lmodvs1 ⊢ V ∈ LMod ∧ X ∈ Base V → 1 S · ˙ X = X
15 12 14 sylan2 ⊢ V ∈ LMod ∧ X ∈ B → 1 S · ˙ X = X
16 15 eqcomd ⊢ V ∈ LMod ∧ X ∈ B → X = 1 S · ˙ X
17 7 10 16 rspcedvdw ⊢ V ∈ LMod ∧ X ∈ B → ∃ m ∈ K X = m · ˙ X
18 17 ex ⊢ V ∈ LMod → X ∈ B → ∃ m ∈ K X = m · ˙ X
19 18 pm4.71d ⊢ V ∈ LMod → X ∈ B ↔ X ∈ B ∧ ∃ m ∈ K X = m · ˙ X
20 pm4.24 ⊢ X ∈ B ↔ X ∈ B ∧ X ∈ B
21 20 anbi1i ⊢ X ∈ B ∧ ∃ m ∈ K X = m · ˙ X ↔ X ∈ B ∧ X ∈ B ∧ ∃ m ∈ K X = m · ˙ X
22 1 prjsprel ⊢ X ∼ ˙ X ↔ X ∈ B ∧ X ∈ B ∧ ∃ m ∈ K X = m · ˙ X
23 21 22 bitr4i ⊢ X ∈ B ∧ ∃ m ∈ K X = m · ˙ X ↔ X ∼ ˙ X
24 19 23 bitrdi ⊢ V ∈ LMod → X ∈ B ↔ X ∼ ˙ X