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=BaseU
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=BaseU
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