Step |
Hyp |
Ref |
Expression |
1 |
|
hgmaprn.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
2 |
|
hgmaprn.u |
⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) |
3 |
|
hgmaprn.r |
⊢ 𝑅 = ( Scalar ‘ 𝑈 ) |
4 |
|
hgmaprn.b |
⊢ 𝐵 = ( Base ‘ 𝑅 ) |
5 |
|
hgmaprn.g |
⊢ 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 ) |
6 |
|
hgmaprn.k |
⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
7 |
1 2 3 4 5 6
|
hgmapfnN |
⊢ ( 𝜑 → 𝐺 Fn 𝐵 ) |
8 |
|
eqid |
⊢ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) |
9 |
|
eqid |
⊢ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) |
10 |
|
eqid |
⊢ ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) = ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) |
11 |
6
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
12 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ 𝐵 ) |
13 |
1 2 3 4 8 9 10 5 11 12
|
hgmapdcl |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 𝐺 ‘ 𝑧 ) ∈ ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) |
14 |
13
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ( 𝐺 ‘ 𝑧 ) ∈ ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) |
15 |
|
fnfvrnss |
⊢ ( ( 𝐺 Fn 𝐵 ∧ ∀ 𝑧 ∈ 𝐵 ( 𝐺 ‘ 𝑧 ) ∈ ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) → ran 𝐺 ⊆ ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) |
16 |
7 14 15
|
syl2anc |
⊢ ( 𝜑 → ran 𝐺 ⊆ ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) |
17 |
|
eqid |
⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 ) |
18 |
|
eqid |
⊢ ( ·𝑠 ‘ 𝑈 ) = ( ·𝑠 ‘ 𝑈 ) |
19 |
|
eqid |
⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 ) |
20 |
|
eqid |
⊢ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) |
21 |
|
eqid |
⊢ ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) |
22 |
|
eqid |
⊢ ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) |
23 |
|
eqid |
⊢ ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) |
24 |
6
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
25 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) → 𝑧 ∈ ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) |
26 |
1 2 17 3 4 18 19 8 20 9 10 21 22 23 5 24 25
|
hgmaprnlem5N |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) → 𝑧 ∈ ran 𝐺 ) |
27 |
16 26
|
eqelssd |
⊢ ( 𝜑 → ran 𝐺 = ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) |
28 |
1 2 3 4 8 9 10 6
|
lcdsbase |
⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) = 𝐵 ) |
29 |
27 28
|
eqtrd |
⊢ ( 𝜑 → ran 𝐺 = 𝐵 ) |