| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | hilablo 31180 | . . 3
⊢ 
+ℎ ∈ AbelOp | 
| 2 |  | ablogrpo 30567 | . . 3
⊢ (
+ℎ ∈ AbelOp → +ℎ ∈
GrpOp) | 
| 3 | 1, 2 | ax-mp 5 | . 2
⊢ 
+ℎ ∈ GrpOp | 
| 4 |  | hhssabl.1 | . . . 4
⊢ 𝐻 ∈
Sℋ | 
| 5 | 4 | elexi 3502 | . . 3
⊢ 𝐻 ∈ V | 
| 6 |  | eqid 2736 | . . . . . . . 8
⊢ ran
+ℎ = ran +ℎ | 
| 7 | 6 | grpofo 30519 | . . . . . . 7
⊢ (
+ℎ ∈ GrpOp → +ℎ :(ran
+ℎ × ran +ℎ )–onto→ran +ℎ ) | 
| 8 |  | fof 6819 | . . . . . . 7
⊢ (
+ℎ :(ran +ℎ × ran
+ℎ )–onto→ran
+ℎ → +ℎ :(ran +ℎ
× ran +ℎ )⟶ran +ℎ
) | 
| 9 | 3, 7, 8 | mp2b 10 | . . . . . 6
⊢ 
+ℎ :(ran +ℎ × ran
+ℎ )⟶ran +ℎ | 
| 10 | 4 | shssii 31233 | . . . . . . . 8
⊢ 𝐻 ⊆
ℋ | 
| 11 |  | df-hba 30989 | . . . . . . . . 9
⊢  ℋ
= (BaseSet‘〈〈 +ℎ ,
·ℎ 〉,
normℎ〉) | 
| 12 |  | eqid 2736 | . . . . . . . . . 10
⊢
〈〈 +ℎ , ·ℎ
〉, normℎ〉 = 〈〈 +ℎ ,
·ℎ 〉,
normℎ〉 | 
| 13 | 12 | hhva 31186 | . . . . . . . . 9
⊢ 
+ℎ = ( +𝑣 ‘〈〈
+ℎ , ·ℎ 〉,
normℎ〉) | 
| 14 | 11, 13 | bafval 30624 | . . . . . . . 8
⊢  ℋ
= ran +ℎ | 
| 15 | 10, 14 | sseqtri 4031 | . . . . . . 7
⊢ 𝐻 ⊆ ran
+ℎ | 
| 16 |  | xpss12 5699 | . . . . . . 7
⊢ ((𝐻 ⊆ ran
+ℎ ∧ 𝐻 ⊆ ran +ℎ ) →
(𝐻 × 𝐻) ⊆ (ran
+ℎ × ran +ℎ )) | 
| 17 | 15, 15, 16 | mp2an 692 | . . . . . 6
⊢ (𝐻 × 𝐻) ⊆ (ran +ℎ ×
ran +ℎ ) | 
| 18 |  | fssres 6773 | . . . . . 6
⊢ ((
+ℎ :(ran +ℎ × ran
+ℎ )⟶ran +ℎ ∧ (𝐻 × 𝐻) ⊆ (ran +ℎ ×
ran +ℎ )) → ( +ℎ ↾ (𝐻 × 𝐻)):(𝐻 × 𝐻)⟶ran +ℎ
) | 
| 19 | 9, 17, 18 | mp2an 692 | . . . . 5
⊢ (
+ℎ ↾ (𝐻 × 𝐻)):(𝐻 × 𝐻)⟶ran
+ℎ | 
| 20 |  | ffn 6735 | . . . . 5
⊢ ((
+ℎ ↾ (𝐻 × 𝐻)):(𝐻 × 𝐻)⟶ran +ℎ → (
+ℎ ↾ (𝐻 × 𝐻)) Fn (𝐻 × 𝐻)) | 
| 21 | 19, 20 | ax-mp 5 | . . . 4
⊢ (
+ℎ ↾ (𝐻 × 𝐻)) Fn (𝐻 × 𝐻) | 
| 22 |  | ovres 7600 | . . . . . 6
⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → (𝑥( +ℎ ↾ (𝐻 × 𝐻))𝑦) = (𝑥 +ℎ 𝑦)) | 
| 23 |  | shaddcl 31237 | . . . . . . 7
⊢ ((𝐻 ∈
Sℋ ∧ 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → (𝑥 +ℎ 𝑦) ∈ 𝐻) | 
| 24 | 4, 23 | mp3an1 1449 | . . . . . 6
⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → (𝑥 +ℎ 𝑦) ∈ 𝐻) | 
| 25 | 22, 24 | eqeltrd 2840 | . . . . 5
⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → (𝑥( +ℎ ↾ (𝐻 × 𝐻))𝑦) ∈ 𝐻) | 
| 26 | 25 | rgen2 3198 | . . . 4
⊢
∀𝑥 ∈
𝐻 ∀𝑦 ∈ 𝐻 (𝑥( +ℎ ↾ (𝐻 × 𝐻))𝑦) ∈ 𝐻 | 
| 27 |  | ffnov 7560 | . . . 4
⊢ ((
+ℎ ↾ (𝐻 × 𝐻)):(𝐻 × 𝐻)⟶𝐻 ↔ (( +ℎ ↾
(𝐻 × 𝐻)) Fn (𝐻 × 𝐻) ∧ ∀𝑥 ∈ 𝐻 ∀𝑦 ∈ 𝐻 (𝑥( +ℎ ↾ (𝐻 × 𝐻))𝑦) ∈ 𝐻)) | 
| 28 | 21, 26, 27 | mpbir2an 711 | . . 3
⊢ (
+ℎ ↾ (𝐻 × 𝐻)):(𝐻 × 𝐻)⟶𝐻 | 
| 29 | 22 | oveq1d 7447 | . . . . 5
⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → ((𝑥( +ℎ ↾ (𝐻 × 𝐻))𝑦) +ℎ 𝑧) = ((𝑥 +ℎ 𝑦) +ℎ 𝑧)) | 
| 30 | 29 | 3adant3 1132 | . . . 4
⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → ((𝑥( +ℎ ↾ (𝐻 × 𝐻))𝑦) +ℎ 𝑧) = ((𝑥 +ℎ 𝑦) +ℎ 𝑧)) | 
| 31 |  | ovres 7600 | . . . . 5
⊢ (((𝑥( +ℎ ↾
(𝐻 × 𝐻))𝑦) ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → ((𝑥( +ℎ ↾ (𝐻 × 𝐻))𝑦)( +ℎ ↾ (𝐻 × 𝐻))𝑧) = ((𝑥( +ℎ ↾ (𝐻 × 𝐻))𝑦) +ℎ 𝑧)) | 
| 32 | 25, 31 | stoic3 1775 | . . . 4
⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → ((𝑥( +ℎ ↾ (𝐻 × 𝐻))𝑦)( +ℎ ↾ (𝐻 × 𝐻))𝑧) = ((𝑥( +ℎ ↾ (𝐻 × 𝐻))𝑦) +ℎ 𝑧)) | 
| 33 |  | ovres 7600 | . . . . . . 7
⊢ ((𝑦 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦( +ℎ ↾ (𝐻 × 𝐻))𝑧) = (𝑦 +ℎ 𝑧)) | 
| 34 | 33 | oveq2d 7448 | . . . . . 6
⊢ ((𝑦 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑥 +ℎ (𝑦( +ℎ ↾ (𝐻 × 𝐻))𝑧)) = (𝑥 +ℎ (𝑦 +ℎ 𝑧))) | 
| 35 | 34 | 3adant1 1130 | . . . . 5
⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑥 +ℎ (𝑦( +ℎ ↾ (𝐻 × 𝐻))𝑧)) = (𝑥 +ℎ (𝑦 +ℎ 𝑧))) | 
| 36 | 28 | fovcl 7562 | . . . . . . 7
⊢ ((𝑦 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦( +ℎ ↾ (𝐻 × 𝐻))𝑧) ∈ 𝐻) | 
| 37 |  | ovres 7600 | . . . . . . 7
⊢ ((𝑥 ∈ 𝐻 ∧ (𝑦( +ℎ ↾ (𝐻 × 𝐻))𝑧) ∈ 𝐻) → (𝑥( +ℎ ↾ (𝐻 × 𝐻))(𝑦( +ℎ ↾ (𝐻 × 𝐻))𝑧)) = (𝑥 +ℎ (𝑦( +ℎ ↾ (𝐻 × 𝐻))𝑧))) | 
| 38 | 36, 37 | sylan2 593 | . . . . . 6
⊢ ((𝑥 ∈ 𝐻 ∧ (𝑦 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻)) → (𝑥( +ℎ ↾ (𝐻 × 𝐻))(𝑦( +ℎ ↾ (𝐻 × 𝐻))𝑧)) = (𝑥 +ℎ (𝑦( +ℎ ↾ (𝐻 × 𝐻))𝑧))) | 
| 39 | 38 | 3impb 1114 | . . . . 5
⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑥( +ℎ ↾ (𝐻 × 𝐻))(𝑦( +ℎ ↾ (𝐻 × 𝐻))𝑧)) = (𝑥 +ℎ (𝑦( +ℎ ↾ (𝐻 × 𝐻))𝑧))) | 
| 40 | 15 | sseli 3978 | . . . . . 6
⊢ (𝑥 ∈ 𝐻 → 𝑥 ∈ ran +ℎ
) | 
| 41 | 15 | sseli 3978 | . . . . . 6
⊢ (𝑦 ∈ 𝐻 → 𝑦 ∈ ran +ℎ
) | 
| 42 | 15 | sseli 3978 | . . . . . 6
⊢ (𝑧 ∈ 𝐻 → 𝑧 ∈ ran +ℎ
) | 
| 43 | 6 | grpoass 30523 | . . . . . . 7
⊢ ((
+ℎ ∈ GrpOp ∧ (𝑥 ∈ ran +ℎ ∧ 𝑦 ∈ ran +ℎ
∧ 𝑧 ∈ ran
+ℎ )) → ((𝑥 +ℎ 𝑦) +ℎ 𝑧) = (𝑥 +ℎ (𝑦 +ℎ 𝑧))) | 
| 44 | 3, 43 | mpan 690 | . . . . . 6
⊢ ((𝑥 ∈ ran +ℎ
∧ 𝑦 ∈ ran
+ℎ ∧ 𝑧 ∈ ran +ℎ ) →
((𝑥 +ℎ
𝑦) +ℎ
𝑧) = (𝑥 +ℎ (𝑦 +ℎ 𝑧))) | 
| 45 | 40, 41, 42, 44 | syl3an 1160 | . . . . 5
⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → ((𝑥 +ℎ 𝑦) +ℎ 𝑧) = (𝑥 +ℎ (𝑦 +ℎ 𝑧))) | 
| 46 | 35, 39, 45 | 3eqtr4d 2786 | . . . 4
⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑥( +ℎ ↾ (𝐻 × 𝐻))(𝑦( +ℎ ↾ (𝐻 × 𝐻))𝑧)) = ((𝑥 +ℎ 𝑦) +ℎ 𝑧)) | 
| 47 | 30, 32, 46 | 3eqtr4d 2786 | . . 3
⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → ((𝑥( +ℎ ↾ (𝐻 × 𝐻))𝑦)( +ℎ ↾ (𝐻 × 𝐻))𝑧) = (𝑥( +ℎ ↾ (𝐻 × 𝐻))(𝑦( +ℎ ↾ (𝐻 × 𝐻))𝑧))) | 
| 48 |  | hilid 31181 | . . . 4
⊢
(GId‘ +ℎ ) =
0ℎ | 
| 49 |  | sh0 31236 | . . . . 5
⊢ (𝐻 ∈
Sℋ → 0ℎ ∈ 𝐻) | 
| 50 | 4, 49 | ax-mp 5 | . . . 4
⊢
0ℎ ∈ 𝐻 | 
| 51 | 48, 50 | eqeltri 2836 | . . 3
⊢
(GId‘ +ℎ ) ∈ 𝐻 | 
| 52 |  | ovres 7600 | . . . . 5
⊢
(((GId‘ +ℎ ) ∈ 𝐻 ∧ 𝑥 ∈ 𝐻) → ((GId‘ +ℎ
)( +ℎ ↾ (𝐻 × 𝐻))𝑥) = ((GId‘ +ℎ )
+ℎ 𝑥)) | 
| 53 | 51, 52 | mpan 690 | . . . 4
⊢ (𝑥 ∈ 𝐻 → ((GId‘ +ℎ )(
+ℎ ↾ (𝐻 × 𝐻))𝑥) = ((GId‘ +ℎ )
+ℎ 𝑥)) | 
| 54 |  | eqid 2736 | . . . . . 6
⊢
(GId‘ +ℎ ) = (GId‘ +ℎ
) | 
| 55 | 6, 54 | grpolid 30536 | . . . . 5
⊢ ((
+ℎ ∈ GrpOp ∧ 𝑥 ∈ ran +ℎ ) →
((GId‘ +ℎ ) +ℎ 𝑥) = 𝑥) | 
| 56 | 3, 40, 55 | sylancr 587 | . . . 4
⊢ (𝑥 ∈ 𝐻 → ((GId‘ +ℎ )
+ℎ 𝑥) =
𝑥) | 
| 57 | 53, 56 | eqtrd 2776 | . . 3
⊢ (𝑥 ∈ 𝐻 → ((GId‘ +ℎ )(
+ℎ ↾ (𝐻 × 𝐻))𝑥) = 𝑥) | 
| 58 | 12 | hhnv 31185 | . . . . . . 7
⊢
〈〈 +ℎ , ·ℎ
〉, normℎ〉 ∈ NrmCVec | 
| 59 | 12 | hhsm 31189 | . . . . . . . 8
⊢ 
·ℎ = ( ·𝑠OLD
‘〈〈 +ℎ , ·ℎ
〉, normℎ〉) | 
| 60 |  | eqid 2736 | . . . . . . . 8
⊢ (
·ℎ ∘ ◡(2nd ↾ ({-1} × V))) =
( ·ℎ ∘ ◡(2nd ↾ ({-1} ×
V))) | 
| 61 | 13, 59, 60 | nvinvfval 30660 | . . . . . . 7
⊢
(〈〈 +ℎ , ·ℎ
〉, normℎ〉 ∈ NrmCVec → (
·ℎ ∘ ◡(2nd ↾ ({-1} × V))) =
(inv‘ +ℎ )) | 
| 62 | 58, 61 | ax-mp 5 | . . . . . 6
⊢ (
·ℎ ∘ ◡(2nd ↾ ({-1} × V))) =
(inv‘ +ℎ ) | 
| 63 | 62 | eqcomi 2745 | . . . . 5
⊢
(inv‘ +ℎ ) = (
·ℎ ∘ ◡(2nd ↾ ({-1} ×
V))) | 
| 64 | 63 | fveq1i 6906 | . . . 4
⊢
((inv‘ +ℎ )‘𝑥) = (( ·ℎ
∘ ◡(2nd ↾ ({-1}
× V)))‘𝑥) | 
| 65 |  | ax-hfvmul 31025 | . . . . . . 7
⊢ 
·ℎ :(ℂ × ℋ)⟶
ℋ | 
| 66 |  | ffn 6735 | . . . . . . 7
⊢ (
·ℎ :(ℂ × ℋ)⟶ ℋ
→ ·ℎ Fn (ℂ ×
ℋ)) | 
| 67 | 65, 66 | ax-mp 5 | . . . . . 6
⊢ 
·ℎ Fn (ℂ ×
ℋ) | 
| 68 |  | neg1cn 12381 | . . . . . 6
⊢ -1 ∈
ℂ | 
| 69 | 60 | curry1val 8131 | . . . . . 6
⊢ ((
·ℎ Fn (ℂ × ℋ) ∧ -1 ∈
ℂ) → (( ·ℎ ∘ ◡(2nd ↾ ({-1} ×
V)))‘𝑥) = (-1
·ℎ 𝑥)) | 
| 70 | 67, 68, 69 | mp2an 692 | . . . . 5
⊢ ((
·ℎ ∘ ◡(2nd ↾ ({-1} ×
V)))‘𝑥) = (-1
·ℎ 𝑥) | 
| 71 |  | shmulcl 31238 | . . . . . 6
⊢ ((𝐻 ∈
Sℋ ∧ -1 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (-1
·ℎ 𝑥) ∈ 𝐻) | 
| 72 | 4, 68, 71 | mp3an12 1452 | . . . . 5
⊢ (𝑥 ∈ 𝐻 → (-1
·ℎ 𝑥) ∈ 𝐻) | 
| 73 | 70, 72 | eqeltrid 2844 | . . . 4
⊢ (𝑥 ∈ 𝐻 → ((
·ℎ ∘ ◡(2nd ↾ ({-1} ×
V)))‘𝑥) ∈ 𝐻) | 
| 74 | 64, 73 | eqeltrid 2844 | . . 3
⊢ (𝑥 ∈ 𝐻 → ((inv‘ +ℎ
)‘𝑥) ∈ 𝐻) | 
| 75 |  | ovres 7600 | . . . . 5
⊢
((((inv‘ +ℎ )‘𝑥) ∈ 𝐻 ∧ 𝑥 ∈ 𝐻) → (((inv‘ +ℎ
)‘𝑥)(
+ℎ ↾ (𝐻 × 𝐻))𝑥) = (((inv‘ +ℎ
)‘𝑥)
+ℎ 𝑥)) | 
| 76 | 74, 75 | mpancom 688 | . . . 4
⊢ (𝑥 ∈ 𝐻 → (((inv‘ +ℎ
)‘𝑥)(
+ℎ ↾ (𝐻 × 𝐻))𝑥) = (((inv‘ +ℎ
)‘𝑥)
+ℎ 𝑥)) | 
| 77 |  | eqid 2736 | . . . . . 6
⊢
(inv‘ +ℎ ) = (inv‘ +ℎ
) | 
| 78 | 6, 54, 77 | grpolinv 30546 | . . . . 5
⊢ ((
+ℎ ∈ GrpOp ∧ 𝑥 ∈ ran +ℎ ) →
(((inv‘ +ℎ )‘𝑥) +ℎ 𝑥) = (GId‘ +ℎ
)) | 
| 79 | 3, 40, 78 | sylancr 587 | . . . 4
⊢ (𝑥 ∈ 𝐻 → (((inv‘ +ℎ
)‘𝑥)
+ℎ 𝑥) =
(GId‘ +ℎ )) | 
| 80 | 76, 79 | eqtrd 2776 | . . 3
⊢ (𝑥 ∈ 𝐻 → (((inv‘ +ℎ
)‘𝑥)(
+ℎ ↾ (𝐻 × 𝐻))𝑥) = (GId‘ +ℎ
)) | 
| 81 | 5, 28, 47, 51, 57, 74, 80 | isgrpoi 30518 | . 2
⊢ (
+ℎ ↾ (𝐻 × 𝐻)) ∈ GrpOp | 
| 82 |  | resss 6018 | . 2
⊢ (
+ℎ ↾ (𝐻 × 𝐻)) ⊆
+ℎ | 
| 83 | 3, 81, 82 | 3pm3.2i 1339 | 1
⊢ (
+ℎ ∈ GrpOp ∧ ( +ℎ ↾ (𝐻 × 𝐻)) ∈ GrpOp ∧ ( +ℎ
↾ (𝐻 × 𝐻)) ⊆ +ℎ
) |