Metamath Proof Explorer

Theorem dochkrshp4

Description: Properties of the closure of the kernel of a functional. (Contributed by NM, 1-Jan-2015)

Ref Expression
Hypotheses dochkrshp3.h ⊢ H = LHyp ⁡ K
dochkrshp3.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
dochkrshp3.u ⊢ U = DVecH ⁡ K ⁡ W
dochkrshp3.v ⊢ V = Base U
dochkrshp3.f ⊢ F = LFnl ⁡ U
dochkrshp3.l ⊢ L = LKer ⁡ U
dochkrshp3.k ⊢ φ → K ∈ HL ∧ W ∈ H
dochkrshp3.g ⊢ φ → G ∈ F
Assertion dochkrshp4 ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ≠ V ∨ L ⁡ G = V

Proof

Step Hyp Ref Expression
1 dochkrshp3.h ⊢ H = LHyp ⁡ K
2 dochkrshp3.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
3 dochkrshp3.u ⊢ U = DVecH ⁡ K ⁡ W
4 dochkrshp3.v ⊢ V = Base U
5 dochkrshp3.f ⊢ F = LFnl ⁡ U
6 dochkrshp3.l ⊢ L = LKer ⁡ U
7 dochkrshp3.k ⊢ φ → K ∈ HL ∧ W ∈ H
8 dochkrshp3.g ⊢ φ → G ∈ F
9 df-ne ⊢ L ⁡ G ≠ V ↔ ¬ L ⁡ G = V
10 1 2 3 4 5 6 7 8 dochkrshp3 ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ≠ V ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G ∧ L ⁡ G ≠ V
11 10 biimprd ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G ∧ L ⁡ G ≠ V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ≠ V
12 11 expdimp ⊢ φ ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G → L ⁡ G ≠ V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ≠ V
13 9 12 biimtrrid ⊢ φ ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G → ¬ L ⁡ G = V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ≠ V
14 13 orrd ⊢ φ ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G → L ⁡ G = V ∨ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ≠ V
15 14 orcomd ⊢ φ ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ≠ V ∨ L ⁡ G = V
16 15 ex ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ≠ V ∨ L ⁡ G = V
17 simpl ⊢ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G ∧ L ⁡ G ≠ V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G
18 10 17 biimtrdi ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ≠ V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G
19 1 3 2 4 7 dochoc1 ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ V = V
20 2fveq3 ⊢ L ⁡ G = V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = ⊥ ˙ ⁡ ⊥ ˙ ⁡ V
21 id ⊢ L ⁡ G = V → L ⁡ G = V
22 20 21 eqeq12d ⊢ L ⁡ G = V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ V = V
23 19 22 syl5ibrcom ⊢ φ → L ⁡ G = V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G
24 18 23 jaod ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ≠ V ∨ L ⁡ G = V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G
25 16 24 impbid ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G ≠ V ∨ L ⁡ G = V