Step | Hyp | Ref
| Expression |
1 | | lmodfopne.v |
. . . . 5
β’ π = (Baseβπ) |
2 | | lmodfopne.s |
. . . . 5
β’ π = (Scalarβπ) |
3 | | lmodfopne.k |
. . . . 5
β’ πΎ = (Baseβπ) |
4 | | lmodfopne.t |
. . . . 5
β’ Β· = (
Β·sf βπ) |
5 | 1, 2, 3, 4 | lmodscaf 20639 |
. . . 4
β’ (π β LMod β Β·
:(πΎ Γ π)βΆπ) |
6 | 5 | ffnd 6718 |
. . 3
β’ (π β LMod β Β· Fn
(πΎ Γ π)) |
7 | | lmodfopne.a |
. . . . 5
β’ + =
(+πβπ) |
8 | 1, 7 | plusffn 18575 |
. . . 4
β’ + Fn (π Γ π) |
9 | | fneq1 6640 |
. . . . . . . . . . 11
β’ ( + = Β· β
( + Fn
(π Γ π) β Β· Fn (π Γ π))) |
10 | | fndmu 6656 |
. . . . . . . . . . . 12
β’ (( Β· Fn
(π Γ π) β§ Β· Fn (πΎ Γ π)) β (π Γ π) = (πΎ Γ π)) |
11 | 10 | ex 412 |
. . . . . . . . . . 11
β’ ( Β· Fn
(π Γ π) β ( Β· Fn (πΎ Γ π) β (π Γ π) = (πΎ Γ π))) |
12 | 9, 11 | syl6bi 253 |
. . . . . . . . . 10
β’ ( + = Β· β
( + Fn
(π Γ π) β ( Β· Fn (πΎ Γ π) β (π Γ π) = (πΎ Γ π)))) |
13 | 12 | com13 88 |
. . . . . . . . 9
β’ ( Β· Fn
(πΎ Γ π) β ( + Fn (π Γ π) β ( + = Β· β (π Γ π) = (πΎ Γ π)))) |
14 | 13 | impcom 407 |
. . . . . . . 8
β’ (( + Fn (π Γ π) β§ Β· Fn (πΎ Γ π)) β ( + = Β· β (π Γ π) = (πΎ Γ π))) |
15 | 1 | lmodbn0 20626 |
. . . . . . . . . . 11
β’ (π β LMod β π β β
) |
16 | | xp11 6174 |
. . . . . . . . . . 11
β’ ((π β β
β§ π β β
) β ((π Γ π) = (πΎ Γ π) β (π = πΎ β§ π = π))) |
17 | 15, 15, 16 | syl2anc 583 |
. . . . . . . . . 10
β’ (π β LMod β ((π Γ π) = (πΎ Γ π) β (π = πΎ β§ π = π))) |
18 | 17 | simprbda 498 |
. . . . . . . . 9
β’ ((π β LMod β§ (π Γ π) = (πΎ Γ π)) β π = πΎ) |
19 | 18 | expcom 413 |
. . . . . . . 8
β’ ((π Γ π) = (πΎ Γ π) β (π β LMod β π = πΎ)) |
20 | 14, 19 | syl6 35 |
. . . . . . 7
β’ (( + Fn (π Γ π) β§ Β· Fn (πΎ Γ π)) β ( + = Β· β (π β LMod β π = πΎ))) |
21 | 20 | com23 86 |
. . . . . 6
β’ (( + Fn (π Γ π) β§ Β· Fn (πΎ Γ π)) β (π β LMod β ( + = Β· β π = πΎ))) |
22 | 21 | ex 412 |
. . . . 5
β’ ( + Fn (π Γ π) β ( Β· Fn (πΎ Γ π) β (π β LMod β ( + = Β· β π = πΎ)))) |
23 | 22 | com23 86 |
. . . 4
β’ ( + Fn (π Γ π) β (π β LMod β ( Β· Fn (πΎ Γ π) β ( + = Β· β π = πΎ)))) |
24 | 8, 23 | ax-mp 5 |
. . 3
β’ (π β LMod β ( Β· Fn
(πΎ Γ π) β ( + = Β· β π = πΎ))) |
25 | 6, 24 | mpd 15 |
. 2
β’ (π β LMod β ( + = Β· β
π = πΎ)) |
26 | 25 | imp 406 |
1
β’ ((π β LMod β§ + = Β· )
β π = πΎ) |