Metamath Proof Explorer

Theorem mapd0

Description: Projectivity map of the zero subspace. Part of property (f) in Baer p. 40. TODO: does proof need to be this long for this simple fact? (Contributed by NM, 15-Mar-2015)

Ref Expression
Hypotheses mapd0.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
mapd0.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
mapd0.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
mapd0.o ⊢ 𝑂 = ( 0g ‘ 𝑈 )
mapd0.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
mapd0.z ⊢ 0 = ( 0g ‘ 𝐶 )
mapd0.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
Assertion mapd0 ( 𝜑 → ( 𝑀 ‘ { 𝑂 } ) = { 0 } )

Proof

Step Hyp Ref Expression
1 mapd0.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 mapd0.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
3 mapd0.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 mapd0.o ⊢ 𝑂 = ( 0g ‘ 𝑈 )
5 mapd0.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
6 mapd0.z ⊢ 0 = ( 0g ‘ 𝐶 )
7 mapd0.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
9 eqid ⊢ ( LFnl ‘ 𝑈 ) = ( LFnl ‘ 𝑈 )
10 eqid ⊢ ( LKer ‘ 𝑈 ) = ( LKer ‘ 𝑈 )
11 eqid ⊢ ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
12 1 3 7 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
13 4 8 lsssn0 ⊢ ( 𝑈 ∈ LMod → { 𝑂 } ∈ ( LSubSp ‘ 𝑈 ) )
14 12 13 syl ⊢ ( 𝜑 → { 𝑂 } ∈ ( LSubSp ‘ 𝑈 ) )
15 1 3 8 9 10 11 2 7 14 mapdval ⊢ ( 𝜑 → ( 𝑀 ‘ { 𝑂 } ) = { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ⊆ { 𝑂 } ) } )
16 simprrr ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( LFnl ‘ 𝑈 ) ∧ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ⊆ { 𝑂 } ) ) ) → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ⊆ { 𝑂 } )
17 12 adantr ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( LFnl ‘ 𝑈 ) ∧ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ⊆ { 𝑂 } ) ) ) → 𝑈 ∈ LMod )
18 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( LFnl ‘ 𝑈 ) ∧ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ⊆ { 𝑂 } ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
19 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
20 simprl ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( LFnl ‘ 𝑈 ) ∧ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ⊆ { 𝑂 } ) ) ) → 𝑔 ∈ ( LFnl ‘ 𝑈 ) )
21 19 9 10 17 20 lkrssv ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( LFnl ‘ 𝑈 ) ∧ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ⊆ { 𝑂 } ) ) ) → ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ⊆ ( Base ‘ 𝑈 ) )
22 1 3 19 8 11 dochlss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ⊆ ( Base ‘ 𝑈 ) ) → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ∈ ( LSubSp ‘ 𝑈 ) )
23 18 21 22 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( LFnl ‘ 𝑈 ) ∧ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ⊆ { 𝑂 } ) ) ) → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ∈ ( LSubSp ‘ 𝑈 ) )
24 4 8 lssle0 ⊢ ( ( 𝑈 ∈ LMod ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ∈ ( LSubSp ‘ 𝑈 ) ) → ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ⊆ { 𝑂 } ↔ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) = { 𝑂 } ) )
25 17 23 24 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( LFnl ‘ 𝑈 ) ∧ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ⊆ { 𝑂 } ) ) ) → ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ⊆ { 𝑂 } ↔ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) = { 𝑂 } ) )
26 16 25 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( LFnl ‘ 𝑈 ) ∧ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ⊆ { 𝑂 } ) ) ) → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) = { 𝑂 } )
27 26 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( LFnl ‘ 𝑈 ) ∧ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ⊆ { 𝑂 } ) ) ) → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ) = ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑂 } ) )
28 simprrl ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( LFnl ‘ 𝑈 ) ∧ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ⊆ { 𝑂 } ) ) ) → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) )
29 1 3 11 19 4 doch0 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑂 } ) = ( Base ‘ 𝑈 ) )
30 7 29 syl ⊢ ( 𝜑 → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑂 } ) = ( Base ‘ 𝑈 ) )
31 30 adantr ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( LFnl ‘ 𝑈 ) ∧ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ⊆ { 𝑂 } ) ) ) → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑂 } ) = ( Base ‘ 𝑈 ) )
32 27 28 31 3eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( LFnl ‘ 𝑈 ) ∧ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ⊆ { 𝑂 } ) ) ) → ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) = ( Base ‘ 𝑈 ) )
33 eqid ⊢ ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 )
34 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑈 ) ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) )
35 33 34 19 9 10 lkr0f ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑔 ∈ ( LFnl ‘ 𝑈 ) ) → ( ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) = ( Base ‘ 𝑈 ) ↔ 𝑔 = ( ( Base ‘ 𝑈 ) × { ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } ) ) )
36 17 20 35 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( LFnl ‘ 𝑈 ) ∧ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ⊆ { 𝑂 } ) ) ) → ( ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) = ( Base ‘ 𝑈 ) ↔ 𝑔 = ( ( Base ‘ 𝑈 ) × { ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } ) ) )
37 32 36 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( LFnl ‘ 𝑈 ) ∧ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ⊆ { 𝑂 } ) ) ) → 𝑔 = ( ( Base ‘ 𝑈 ) × { ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } ) )
38 1 3 19 33 34 5 6 7 lcd0v ⊢ ( 𝜑 → 0 = ( ( Base ‘ 𝑈 ) × { ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } ) )
39 38 adantr ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( LFnl ‘ 𝑈 ) ∧ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ⊆ { 𝑂 } ) ) ) → 0 = ( ( Base ‘ 𝑈 ) × { ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } ) )
40 37 39 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( LFnl ‘ 𝑈 ) ∧ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ⊆ { 𝑂 } ) ) ) → 𝑔 = 0 )
41 40 ex ⊢ ( 𝜑 → ( ( 𝑔 ∈ ( LFnl ‘ 𝑈 ) ∧ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ⊆ { 𝑂 } ) ) → 𝑔 = 0 ) )
42 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
43 1 5 42 6 7 lcd0vcl ⊢ ( 𝜑 → 0 ∈ ( Base ‘ 𝐶 ) )
44 1 5 42 3 9 7 43 lcdvbaselfl ⊢ ( 𝜑 → 0 ∈ ( LFnl ‘ 𝑈 ) )
45 33 34 19 9 10 lkr0f ⊢ ( ( 𝑈 ∈ LMod ∧ 0 ∈ ( LFnl ‘ 𝑈 ) ) → ( ( ( LKer ‘ 𝑈 ) ‘ 0 ) = ( Base ‘ 𝑈 ) ↔ 0 = ( ( Base ‘ 𝑈 ) × { ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } ) ) )
46 12 44 45 syl2anc ⊢ ( 𝜑 → ( ( ( LKer ‘ 𝑈 ) ‘ 0 ) = ( Base ‘ 𝑈 ) ↔ 0 = ( ( Base ‘ 𝑈 ) × { ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } ) ) )
47 38 46 mpbird ⊢ ( 𝜑 → ( ( LKer ‘ 𝑈 ) ‘ 0 ) = ( Base ‘ 𝑈 ) )
48 47 fveq2d ⊢ ( 𝜑 → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 0 ) ) = ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( Base ‘ 𝑈 ) ) )
49 48 fveq2d ⊢ ( 𝜑 → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 0 ) ) ) = ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( Base ‘ 𝑈 ) ) ) )
50 1 3 11 19 7 dochoc1 ⊢ ( 𝜑 → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( Base ‘ 𝑈 ) ) ) = ( Base ‘ 𝑈 ) )
51 49 50 eqtrd ⊢ ( 𝜑 → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 0 ) ) ) = ( Base ‘ 𝑈 ) )
52 51 47 eqtr4d ⊢ ( 𝜑 → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 0 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 0 ) )
53 1 3 11 19 4 doch1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( Base ‘ 𝑈 ) ) = { 𝑂 } )
54 7 53 syl ⊢ ( 𝜑 → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( Base ‘ 𝑈 ) ) = { 𝑂 } )
55 48 54 eqtrd ⊢ ( 𝜑 → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 0 ) ) = { 𝑂 } )
56 eqimss ⊢ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 0 ) ) = { 𝑂 } → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 0 ) ) ⊆ { 𝑂 } )
57 55 56 syl ⊢ ( 𝜑 → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 0 ) ) ⊆ { 𝑂 } )
58 44 52 57 jca32 ⊢ ( 𝜑 → ( 0 ∈ ( LFnl ‘ 𝑈 ) ∧ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 0 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 0 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 0 ) ) ⊆ { 𝑂 } ) ) )
59 eleq1 ⊢ ( 𝑔 = 0 → ( 𝑔 ∈ ( LFnl ‘ 𝑈 ) ↔ 0 ∈ ( LFnl ‘ 𝑈 ) ) )
60 2fveq3 ⊢ ( 𝑔 = 0 → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) = ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 0 ) ) )
61 60 fveq2d ⊢ ( 𝑔 = 0 → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ) = ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 0 ) ) ) )
62 fveq2 ⊢ ( 𝑔 = 0 → ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) = ( ( LKer ‘ 𝑈 ) ‘ 0 ) )
63 61 62 eqeq12d ⊢ ( 𝑔 = 0 → ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ↔ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 0 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 0 ) ) )
64 60 sseq1d ⊢ ( 𝑔 = 0 → ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ⊆ { 𝑂 } ↔ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 0 ) ) ⊆ { 𝑂 } ) )
65 63 64 anbi12d ⊢ ( 𝑔 = 0 → ( ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ⊆ { 𝑂 } ) ↔ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 0 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 0 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 0 ) ) ⊆ { 𝑂 } ) ) )
66 59 65 anbi12d ⊢ ( 𝑔 = 0 → ( ( 𝑔 ∈ ( LFnl ‘ 𝑈 ) ∧ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ⊆ { 𝑂 } ) ) ↔ ( 0 ∈ ( LFnl ‘ 𝑈 ) ∧ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 0 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 0 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 0 ) ) ⊆ { 𝑂 } ) ) ) )
67 58 66 syl5ibrcom ⊢ ( 𝜑 → ( 𝑔 = 0 → ( 𝑔 ∈ ( LFnl ‘ 𝑈 ) ∧ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ⊆ { 𝑂 } ) ) ) )
68 41 67 impbid ⊢ ( 𝜑 → ( ( 𝑔 ∈ ( LFnl ‘ 𝑈 ) ∧ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ⊆ { 𝑂 } ) ) ↔ 𝑔 = 0 ) )
69 2fveq3 ⊢ ( 𝑓 = 𝑔 → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) = ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) )
70 69 fveq2d ⊢ ( 𝑓 = 𝑔 → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ) )
71 fveq2 ⊢ ( 𝑓 = 𝑔 → ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) )
72 70 71 eqeq12d ⊢ ( 𝑓 = 𝑔 → ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ↔ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) )
73 69 sseq1d ⊢ ( 𝑓 = 𝑔 → ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ⊆ { 𝑂 } ↔ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ⊆ { 𝑂 } ) )
74 72 73 anbi12d ⊢ ( 𝑓 = 𝑔 → ( ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ⊆ { 𝑂 } ) ↔ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ⊆ { 𝑂 } ) ) )
75 74 elrab ⊢ ( 𝑔 ∈ { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ⊆ { 𝑂 } ) } ↔ ( 𝑔 ∈ ( LFnl ‘ 𝑈 ) ∧ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ⊆ { 𝑂 } ) ) )
76 velsn ⊢ ( 𝑔 ∈ { 0 } ↔ 𝑔 = 0 )
77 68 75 76 3bitr4g ⊢ ( 𝜑 → ( 𝑔 ∈ { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ⊆ { 𝑂 } ) } ↔ 𝑔 ∈ { 0 } ) )
78 77 eqrdv ⊢ ( 𝜑 → { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ⊆ { 𝑂 } ) } = { 0 } )
79 15 78 eqtrd ⊢ ( 𝜑 → ( 𝑀 ‘ { 𝑂 } ) = { 0 } )