Metamath Proof Explorer

Theorem mapdordlem1a

Description: Lemma for mapdord . (Contributed by NM, 27-Jan-2015)

Ref Expression
Hypotheses mapdordlem1a.h ⊢ H = LHyp ⁡ K
mapdordlem1a.o ⊢ O = ocH ⁡ K ⁡ W
mapdordlem1a.u ⊢ U = DVecH ⁡ K ⁡ W
mapdordlem1a.v ⊢ V = Base U
mapdordlem1a.y ⊢ Y = LSHyp ⁡ U
mapdordlem1a.f ⊢ F = LFnl ⁡ U
mapdordlem1a.l ⊢ L = LKer ⁡ U
mapdordlem1a.t ⊢ T = g ∈ F | O ⁡ O ⁡ L ⁡ g ∈ Y
mapdordlem1a.c ⊢ C = g ∈ F | O ⁡ O ⁡ L ⁡ g = L ⁡ g
mapdordlem1a.k ⊢ φ → K ∈ HL ∧ W ∈ H
Assertion mapdordlem1a ⊢ φ → J ∈ T ↔ J ∈ C ∧ O ⁡ O ⁡ L ⁡ J ∈ Y

Proof

Step Hyp Ref Expression
1 mapdordlem1a.h ⊢ H = LHyp ⁡ K
2 mapdordlem1a.o ⊢ O = ocH ⁡ K ⁡ W
3 mapdordlem1a.u ⊢ U = DVecH ⁡ K ⁡ W
4 mapdordlem1a.v ⊢ V = Base U
5 mapdordlem1a.y ⊢ Y = LSHyp ⁡ U
6 mapdordlem1a.f ⊢ F = LFnl ⁡ U
7 mapdordlem1a.l ⊢ L = LKer ⁡ U
8 mapdordlem1a.t ⊢ T = g ∈ F | O ⁡ O ⁡ L ⁡ g ∈ Y
9 mapdordlem1a.c ⊢ C = g ∈ F | O ⁡ O ⁡ L ⁡ g = L ⁡ g
10 mapdordlem1a.k ⊢ φ → K ∈ HL ∧ W ∈ H
11 simprr ⊢ φ ∧ J ∈ F ∧ O ⁡ O ⁡ L ⁡ J ∈ Y → O ⁡ O ⁡ L ⁡ J ∈ Y
12 10 adantr ⊢ φ ∧ J ∈ F ∧ O ⁡ O ⁡ L ⁡ J ∈ Y → K ∈ HL ∧ W ∈ H
13 simprl ⊢ φ ∧ J ∈ F ∧ O ⁡ O ⁡ L ⁡ J ∈ Y → J ∈ F
14 1 2 3 6 5 7 12 13 dochlkr ⊢ φ ∧ J ∈ F ∧ O ⁡ O ⁡ L ⁡ J ∈ Y → O ⁡ O ⁡ L ⁡ J ∈ Y ↔ O ⁡ O ⁡ L ⁡ J = L ⁡ J ∧ L ⁡ J ∈ Y
15 11 14 mpbid ⊢ φ ∧ J ∈ F ∧ O ⁡ O ⁡ L ⁡ J ∈ Y → O ⁡ O ⁡ L ⁡ J = L ⁡ J ∧ L ⁡ J ∈ Y
16 15 simpld ⊢ φ ∧ J ∈ F ∧ O ⁡ O ⁡ L ⁡ J ∈ Y → O ⁡ O ⁡ L ⁡ J = L ⁡ J
17 16 ex ⊢ φ → J ∈ F ∧ O ⁡ O ⁡ L ⁡ J ∈ Y → O ⁡ O ⁡ L ⁡ J = L ⁡ J
18 17 pm4.71rd ⊢ φ → J ∈ F ∧ O ⁡ O ⁡ L ⁡ J ∈ Y ↔ O ⁡ O ⁡ L ⁡ J = L ⁡ J ∧ J ∈ F ∧ O ⁡ O ⁡ L ⁡ J ∈ Y
19 2fveq3 ⊢ g = J → O ⁡ L ⁡ g = O ⁡ L ⁡ J
20 19 fveq2d ⊢ g = J → O ⁡ O ⁡ L ⁡ g = O ⁡ O ⁡ L ⁡ J
21 20 eleq1d ⊢ g = J → O ⁡ O ⁡ L ⁡ g ∈ Y ↔ O ⁡ O ⁡ L ⁡ J ∈ Y
22 21 8 elrab2 ⊢ J ∈ T ↔ J ∈ F ∧ O ⁡ O ⁡ L ⁡ J ∈ Y
23 9 lcfl1lem ⊢ J ∈ C ↔ J ∈ F ∧ O ⁡ O ⁡ L ⁡ J = L ⁡ J
24 23 anbi1i ⊢ J ∈ C ∧ O ⁡ O ⁡ L ⁡ J ∈ Y ↔ J ∈ F ∧ O ⁡ O ⁡ L ⁡ J = L ⁡ J ∧ O ⁡ O ⁡ L ⁡ J ∈ Y
25 anass ⊢ J ∈ F ∧ O ⁡ O ⁡ L ⁡ J = L ⁡ J ∧ O ⁡ O ⁡ L ⁡ J ∈ Y ↔ J ∈ F ∧ O ⁡ O ⁡ L ⁡ J = L ⁡ J ∧ O ⁡ O ⁡ L ⁡ J ∈ Y
26 an12 ⊢ J ∈ F ∧ O ⁡ O ⁡ L ⁡ J = L ⁡ J ∧ O ⁡ O ⁡ L ⁡ J ∈ Y ↔ O ⁡ O ⁡ L ⁡ J = L ⁡ J ∧ J ∈ F ∧ O ⁡ O ⁡ L ⁡ J ∈ Y
27 24 25 26 3bitri ⊢ J ∈ C ∧ O ⁡ O ⁡ L ⁡ J ∈ Y ↔ O ⁡ O ⁡ L ⁡ J = L ⁡ J ∧ J ∈ F ∧ O ⁡ O ⁡ L ⁡ J ∈ Y
28 18 22 27 3bitr4g ⊢ φ → J ∈ T ↔ J ∈ C ∧ O ⁡ O ⁡ L ⁡ J ∈ Y