Step | Hyp | Ref
| Expression |
1 | | lnoval.1 |
. . . . 5
β’ π = (BaseSetβπ) |
2 | | lnoval.2 |
. . . . 5
β’ π = (BaseSetβπ) |
3 | | lnoval.3 |
. . . . 5
β’ πΊ = ( +π£
βπ) |
4 | | lnoval.4 |
. . . . 5
β’ π» = ( +π£
βπ) |
5 | | lnoval.5 |
. . . . 5
β’ π
= (
Β·π OLD βπ) |
6 | | lnoval.6 |
. . . . 5
β’ π = (
Β·π OLD βπ) |
7 | | lnoval.7 |
. . . . 5
β’ πΏ = (π LnOp π) |
8 | 1, 2, 3, 4, 5, 6, 7 | islno 29737 |
. . . 4
β’ ((π β NrmCVec β§ π β NrmCVec) β (π β πΏ β (π:πβΆπ β§ βπ’ β β βπ€ β π βπ‘ β π (πβ((π’π
π€)πΊπ‘)) = ((π’π(πβπ€))π»(πβπ‘))))) |
9 | 8 | biimp3a 1470 |
. . 3
β’ ((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β (π:πβΆπ β§ βπ’ β β βπ€ β π βπ‘ β π (πβ((π’π
π€)πΊπ‘)) = ((π’π(πβπ€))π»(πβπ‘)))) |
10 | 9 | simprd 497 |
. 2
β’ ((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β βπ’ β β βπ€ β π βπ‘ β π (πβ((π’π
π€)πΊπ‘)) = ((π’π(πβπ€))π»(πβπ‘))) |
11 | | oveq1 7365 |
. . . . 5
β’ (π’ = π΄ β (π’π
π€) = (π΄π
π€)) |
12 | 11 | fvoveq1d 7380 |
. . . 4
β’ (π’ = π΄ β (πβ((π’π
π€)πΊπ‘)) = (πβ((π΄π
π€)πΊπ‘))) |
13 | | oveq1 7365 |
. . . . 5
β’ (π’ = π΄ β (π’π(πβπ€)) = (π΄π(πβπ€))) |
14 | 13 | oveq1d 7373 |
. . . 4
β’ (π’ = π΄ β ((π’π(πβπ€))π»(πβπ‘)) = ((π΄π(πβπ€))π»(πβπ‘))) |
15 | 12, 14 | eqeq12d 2749 |
. . 3
β’ (π’ = π΄ β ((πβ((π’π
π€)πΊπ‘)) = ((π’π(πβπ€))π»(πβπ‘)) β (πβ((π΄π
π€)πΊπ‘)) = ((π΄π(πβπ€))π»(πβπ‘)))) |
16 | | oveq2 7366 |
. . . . 5
β’ (π€ = π΅ β (π΄π
π€) = (π΄π
π΅)) |
17 | 16 | fvoveq1d 7380 |
. . . 4
β’ (π€ = π΅ β (πβ((π΄π
π€)πΊπ‘)) = (πβ((π΄π
π΅)πΊπ‘))) |
18 | | fveq2 6843 |
. . . . . 6
β’ (π€ = π΅ β (πβπ€) = (πβπ΅)) |
19 | 18 | oveq2d 7374 |
. . . . 5
β’ (π€ = π΅ β (π΄π(πβπ€)) = (π΄π(πβπ΅))) |
20 | 19 | oveq1d 7373 |
. . . 4
β’ (π€ = π΅ β ((π΄π(πβπ€))π»(πβπ‘)) = ((π΄π(πβπ΅))π»(πβπ‘))) |
21 | 17, 20 | eqeq12d 2749 |
. . 3
β’ (π€ = π΅ β ((πβ((π΄π
π€)πΊπ‘)) = ((π΄π(πβπ€))π»(πβπ‘)) β (πβ((π΄π
π΅)πΊπ‘)) = ((π΄π(πβπ΅))π»(πβπ‘)))) |
22 | | oveq2 7366 |
. . . . 5
β’ (π‘ = πΆ β ((π΄π
π΅)πΊπ‘) = ((π΄π
π΅)πΊπΆ)) |
23 | 22 | fveq2d 6847 |
. . . 4
β’ (π‘ = πΆ β (πβ((π΄π
π΅)πΊπ‘)) = (πβ((π΄π
π΅)πΊπΆ))) |
24 | | fveq2 6843 |
. . . . 5
β’ (π‘ = πΆ β (πβπ‘) = (πβπΆ)) |
25 | 24 | oveq2d 7374 |
. . . 4
β’ (π‘ = πΆ β ((π΄π(πβπ΅))π»(πβπ‘)) = ((π΄π(πβπ΅))π»(πβπΆ))) |
26 | 23, 25 | eqeq12d 2749 |
. . 3
β’ (π‘ = πΆ β ((πβ((π΄π
π΅)πΊπ‘)) = ((π΄π(πβπ΅))π»(πβπ‘)) β (πβ((π΄π
π΅)πΊπΆ)) = ((π΄π(πβπ΅))π»(πβπΆ)))) |
27 | 15, 21, 26 | rspc3v 3592 |
. 2
β’ ((π΄ β β β§ π΅ β π β§ πΆ β π) β (βπ’ β β βπ€ β π βπ‘ β π (πβ((π’π
π€)πΊπ‘)) = ((π’π(πβπ€))π»(πβπ‘)) β (πβ((π΄π
π΅)πΊπΆ)) = ((π΄π(πβπ΅))π»(πβπΆ)))) |
28 | 10, 27 | mpan9 508 |
1
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (π΄ β β β§ π΅ β π β§ πΆ β π)) β (πβ((π΄π
π΅)πΊπΆ)) = ((π΄π(πβπ΅))π»(πβπΆ))) |